The coarea formula for total variation #
For a function u on an open set Ω of a finite-dimensional real inner product space, the
coarea formula |Du|(Ω) = ∫_ℝ P({u > t}; Ω) dt expresses the total variation of u as the
integral over all levels of the perimeters of its superlevel sets. Here |Du|(Ω) is the
variational supremum TauCeti.totalVariationOn and P(·; Ω) is TauCeti.perimeter, both
against an additive Haar measure; the level integral is an extended Lebesgue integral.
The formula holds for every function locally integrable on Ω
(TauCeti.totalVariationOn_eq_lintegral_perimeter). The proof has three steps.
- The layer-cake formula for the distributional pairing,
∫ u div φ = ∫_ℝ (∫_{u > t} div φ) dt, follows from writingu x = ∫_ℝ (1_{t < u x} - 1_{t < 0}) dt, Fubini's theorem and∫ div φ = 0. Testing each superlevel set against the same vector field gives the coarea inequality|Du|(Ω) ≤ ∫_ℝ P({u > t}; Ω) dt. - For
ulocally Lipschitz onΩ, in particularC¹, the reverse inequality holds and∫_ℝ P({u > t}; Ω) dt = ∫_Ω ‖Du‖. The indicator of{u > t}is the pointwise limit ofψ ((n + 1) (u - t))for the smooth transition functionψ. Lower semicontinuity boundsP({u > t}; Ω)by the variations of these locally Lipschitz functions, and Fatou's lemma and Tonelli's theorem integrate the bound overt. - For a general locally integrable
u, the reverse inequality is first proved on open setsΩ'with compact closure inΩ. There the mollifications ofusatisfy it by the previous step and the convolution estimateContDiffBump.totalVariationOn_normed_convolution_le. Since∫_ℝ μ (({w > t} ∆ {u > t}) ∩ K) dt = ∫_K |w - u|, along a subsequence their superlevel sets converge locally in measure to those ofuat almost every level. Lower semicontinuity of the perimeter and Fatou's lemma then pass the inequality tou. An exhaustion ofΩ, inner continuity of the perimeter in the open set and monotone convergence finish the proof.
Fatou's lemma and monotone convergence need the level perimeter t ↦ P({u > t}; Ω) to be
measurable (TauCeti.measurable_perimeter_setOf_lt). It is lower semicontinuous at every level
t with μ ({u = t} ∩ Ω) = 0, so at all but countably many levels.
If u moreover has locally finite variation on Ω, the formula holds at the level of measures:
the variation measure |Du| (TauCeti.variationMeasure) is the superposition
|Du| = ∫_ℝ |D1_{u > t}| dt of the perimeter measures of the superlevel sets, so that
|Du|(B) = ∫_ℝ |D1_{u > t}|(B) dt for every Borel set B ⊆ Ω
(TauCeti.variationMeasure_eq_bind). Applying the coarea formula on each set V j of an
exhaustion of Ω by relatively compact open sets shows that almost every superlevel set has
locally finite perimeter in Ω. The two measures then agree on open subsets of Ω by the coarea
formula there, and are finite on each V j, so they agree on all Borel sets. Since the definition
of the variation measure involves a choice depending on local finiteness, the measurability of
t ↦ |D1_{u > t}| is proved separately, by a π-λ argument on each V j.
Main declarations #
TauCeti.integral_divergenceCLM_mul_eq_integral_integral_indicator: the layer-cake formula for the pairing ofuwithdiv φ, in any finite-dimensional real normed space.TauCeti.totalVariationOn_le_lintegral_perimeter: the coarea inequality.LocallyLipschitzOn.lintegral_perimeter_eq_setLIntegral_enorm_fderiv: for locally Lipschitzu,∫_ℝ P({u > t}; Ω) dt = ∫_Ω ‖Du‖.TauCeti.measurable_perimeter_setOf_lt: the perimeter of{u > t}is measurable int.TauCeti.totalVariationOn_eq_lintegral_perimeter: the coarea formula|Du|(Ω) = ∫_ℝ P({u > t}; Ω) dtfor locally integrableu.TauCeti.ae_perimeter_setOf_lt_lt_top: if|Du|(Ω) < ∞, then{u > t}has finite perimeter inΩfor almost everyt.TauCeti.ae_exists_perimeter_setOf_lt_ne_top: ifuhas locally finite variation onΩ, then{u > t}has locally finite perimeter inΩfor almost everyt.TauCeti.measurable_variationMeasure_indicator_setOf_lt: the perimeter measure|D1_{u > t}|onΩis measurable int.TauCeti.variationMeasure_eq_bind,TauCeti.variationMeasure_apply_eq_lintegralandTauCeti.lintegral_variationMeasure_eq_lintegral_lintegral: the coarea formula|Du| = ∫_ℝ |D1_{u > t}| dtfor the variation measure, on Borel sets and for integrals.
References #
- L. C. Evans, R. F. Gariepy, Measure Theory and Fine Properties of Functions, §5.5, Theorem 5.9.
The layer-cake formula and the coarea inequality #
The layer-cake formula for the distributional pairing. For u locally integrable on Ω
and a test vector field φ on Ω, the pairing of u with div φ is the integral over all
levels t of the pairings of the superlevel sets {u > t}:
∫ u div φ = ∫_ℝ (∫_{u > t} div φ) dt.
The coarea inequality. For u locally integrable on Ω, against an additive Haar
measure, the total variation of u is at most the integral of the perimeters of its superlevel
sets: |Du|(Ω) ≤ ∫_ℝ P({u > t}; Ω) dt.
The coarea formula for locally Lipschitz functions #
The coarea formula for locally Lipschitz functions. If u is locally Lipschitz on Ω,
in particular if it is C¹ there, then against an additive Haar measure the perimeters of its
superlevel sets integrate to the integral of the norm of its derivative:
∫_ℝ P({u > t}; Ω) dt = ∫_Ω ‖Du‖.
Measurability in the level #
Measurability in the level. For u almost everywhere measurable on Ω, the perimeter of
the superlevel set {u > t} in Ω is a measurable function of the level t.
The coarea formula for locally integrable functions #
The coarea formula for total variation. For u locally integrable on Ω, against an
additive Haar measure, the total variation of u is the integral of the perimeters of its
superlevel sets: |Du|(Ω) = ∫_ℝ P({u > t}; Ω) dt, finite or infinite.
If u has finite total variation on Ω, then its superlevel sets {u > t} have finite
perimeter in Ω for almost every level t.
The coarea formula for the variation measure #
The perimeter measure |D1_s| of a null-measurable set s with locally finite perimeter in
Ω gives every open U ⊆ Ω the perimeter P(s; U).
Measurability in the level of the perimeter measures. For u almost everywhere measurable
on Ω, the variation measure |D1_{u > t}| of the indicator of the superlevel set {u > t} is a
measurable function of the level t.
If u has locally finite variation on Ω, then for almost every level t the superlevel set
{u > t} has locally finite perimeter in Ω: every compact K ⊆ Ω has an open neighbourhood U
with P({u > t}; U) < ∞.
The coarea formula for the variation measure. If u is locally integrable on Ω with
locally finite variation there, its variation measure is the superposition of the perimeter
measures of its superlevel sets: |Du| = ∫_ℝ |D1_{u > t}| dt as measures on Ω.
The coarea formula on Borel sets. If u is locally integrable on Ω with locally finite
variation there, then |Du|(B) = ∫_ℝ |D1_{u > t}|(B) dt for every measurable B ⊆ Ω.
The coarea formula for integrals against the variation measure. If u is locally integrable
on Ω with locally finite variation there, then ∫ f d|Du| = ∫_ℝ ∫ f d|D1_{u > t}| dt for every
nonnegative f almost everywhere measurable for |Du|.