The Sobolev inequality for functions of bounded variation

Let E be a real inner product space of finite dimension n ≥ 2 with an additive Haar measure μ, and let p = n / (n - 1). This file proves the Gagliardo–Nirenberg–Sobolev inequality for functions of bounded variation: every integrable u : E → ℝ satisfies

‖u‖_p ≤ C |Du|(E),

where |Du|(E) is the variational total variation TauCeti.totalVariationOn μ ⊤ u, finite or infinite, and C = MeasureTheory.eLpNormLESNormFDerivOneConst μ p is the constant of Mathlib's inequality MeasureTheory.eLpNorm_le_eLpNorm_fderiv_one for compactly supported C¹ functions. No compact support and no differentiability are assumed. Applied to indicators, it gives the nonsharp isoperimetric inequality μ(s) ^ (1 - 1/n) ≤ C P(s; E) for every null-measurable set of finite measure; finiteness of the perimeter is not assumed either.

The proof mollifies u. The mollifications ρ_ε ⋆ u are smooth and integrable, so they satisfy the inequality ‖ρ_ε ⋆ u‖_p ≤ C ‖D(ρ_ε ⋆ u)‖₁ for integrable C¹ functions (TauCeti.eLpNorm_le_eLpNorm_fderiv_one_of_integrable). For a smooth function ‖Dv‖₁ is the total variation |Dv|(E), and |D(ρ_ε ⋆ u)|(E) ≤ |Du|(E) by the convolution estimate ContDiffBump.totalVariationOn_normed_convolution_le. The mollifications converge to u in L¹, so Fatou's lemma along an almost everywhere convergent subsequence passes the inequality to u.

Main results

• TauCeti.eLpNorm_le_totalVariationOn: the Sobolev inequality ‖u‖_p ≤ C |Du|(E) for every integrable u.
• TauCeti.measure_rpow_le_perimeter: the isoperimetric inequality μ(s) ^ (1/p) ≤ C P(s; E) for every null-measurable set s of finite measure.

References

• L. Ambrosio, N. Fusco, D. Pallara, Functions of Bounded Variation and Free Discontinuity Problems, Theorem 3.47.
• L. C. Evans, R. F. Gariepy, Measure Theory and Fine Properties of Functions, §5.6.1, Theorem 1.
• F. Maggi, Sets of Finite Perimeter and Geometric Variational Problems, Theorem 12.37.

theorem TauCeti.eLpNorm_le_totalVariationOn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {p : NNReal} {u : E → ℝ} (hu : MeasureTheory.Integrable u μ) (hp : (↑(Module.finrank ℝ E)).HolderConjugate p) : MeasureTheory.eLpNorm u (↑p) μ ≤ ↑(MeasureTheory.eLpNormLESNormFDerivOneConst μ ↑p) * totalVariationOn μ ⊤ u

The Sobolev inequality for functions of bounded variation. Let E have dimension n ≥ 2 and let p = n / (n - 1). Every integrable u : E → ℝ satisfies ‖u‖_p ≤ C |Du|(E), where |Du|(E) is the total variation of u on the whole space, finite or infinite, and C is the constant MeasureTheory.eLpNormLESNormFDerivOneConst μ p of the C¹ Gagliardo–Nirenberg– Sobolev inequality MeasureTheory.eLpNorm_le_eLpNorm_fderiv_one.

theorem TauCeti.measure_rpow_le_perimeter {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {p : NNReal} {s : Set E} (hs : MeasureTheory.NullMeasurableSet s μ) (hμs : μ s ≠ ⊤) (hp : (↑(Module.finrank ℝ E)).HolderConjugate p) : μ s ^ (↑p)⁻¹ ≤ ↑(MeasureTheory.eLpNormLESNormFDerivOneConst μ ↑p) * perimeter μ ⊤ s

The nonsharp isoperimetric inequality. Let E have dimension n ≥ 2 and let p = n / (n - 1). Every null-measurable set s of finite measure satisfies μ(s) ^ (1/p) ≤ C P(s; E), where 1/p = 1 - 1/n, P(s; E) is the perimeter of s in the whole space, finite or infinite, and C is the constant MeasureTheory.eLpNormLESNormFDerivOneConst μ p of the Gagliardo–Nirenberg–Sobolev inequality.