The sharp BV Sobolev bound

In a real Euclidean space of dimension n ≥ 2, put ωₙ = volume (ball 0 1) and p = n / (n - 1). Every integrable real-valued function satisfies

‖u‖ₚ ≤ (n ωₙ^(1/n))⁻¹ |Du|(E).

The bound allows infinite variation. Finite variation gives membership in Lᵖ, not just a bound on a seminorm. The exponent is expressed by NNReal.HolderConjugate n p, as in the nonsharp BV Sobolev inequality.

For a nonnegative function, integral Minkowski bounds its norm by the integral of the superlevel-set norms. The sharp perimeter inequality bounds these norms, and scalar coarea integrates the perimeters. Lipschitz composition with absolute value extends the result to signed functions. The geometric inputs are MeasureTheory.NullMeasurableSet.ofReal_mul_volume_real_rpow_mul_le_perimeter and TauCeti.totalVariationOn_eq_lintegral_perimeter; the absolute-value step uses TauCeti.totalVariationOn_comp_lipschitz_le. No regularity or bounded support is required of u. This file proves the bound and membership, not the classification of equality cases.

References

• L. C. Evans and R. F. Gariepy, Measure Theory and Fine Properties of Functions, revised edition, §5.6.1 (Sobolev inequalities for BV functions).
• F. Maggi, Sets of Finite Perimeter and Geometric Variational Problems, Theorem 12.37 (the sharp BV Sobolev inequality).

theorem TauCeti.eLpNorm_le_inv_mul_totalVariationOn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {u : E → ℝ} {p : NNReal} (hu : MeasureTheory.Integrable u MeasureTheory.volume) (hp : (↑(Module.finrank ℝ E)).HolderConjugate p) : MeasureTheory.eLpNorm u (↑p) MeasureTheory.volume ≤ (ENNReal.ofReal (↑(Module.finrank ℝ E) * MeasureTheory.volume.real (Metric.ball 0 1) ^ (↑(Module.finrank ℝ E))⁻¹))⁻¹ * totalVariationOn MeasureTheory.volume ⊤ u

The sharp BV Sobolev bound. In dimension n ≥ 2, every integrable real-valued function satisfies ‖u‖ₚ ≤ (n ωₙ^(1/n))⁻¹ |Du|(E) for p = n / (n - 1). The total variation may be infinite.

theorem TauCeti.MemBV.memLp_of_holderConjugate {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {u : E → ℝ} {p : NNReal} (hu : MemBV MeasureTheory.volume ⊤ u) (hp : (↑(Module.finrank ℝ E)).HolderConjugate p) : MeasureTheory.MemLp u (↑p) MeasureTheory.volume

A whole-space BV function belongs to the critical Lebesgue space L^(n/(n-1)).