The Gagliardo–Nirenberg–Sobolev inequality for integrable functions

Mathlib's Gagliardo–Nirenberg–Sobolev inequality MeasureTheory.eLpNorm_le_eLpNorm_fderiv_one bounds ‖u‖_p, for p = n / (n - 1), by C ‖Du‖₁ for a compactly supported C¹ function u on a space of dimension n ≥ 2, where C = MeasureTheory.eLpNormLESNormFDerivOneConst μ p. This file removes the compact support hypothesis: the same inequality, with the same constant, holds for every integrable C¹ function, with ‖Du‖₁ finite or infinite.

The constant is positive (TauCeti.eLpNormLESNormFDerivOneConst_pos), as one sees by applying the inequality to a bump function; this is what makes the inequality meaningful when ‖Du‖₁ is infinite. When ‖Du‖₁ is finite, the compactly supported functions χ(x / R) u(x), for a bump function χ equal to one near zero, converge to u in L¹ and their derivatives converge to Du in L¹ (TauCeti.tendsto_eLpNorm_iteratedFDeriv_cutoff_sub). Mathlib's inequality holds for each of them, and Fatou's lemma along an almost everywhere convergent subsequence passes it to u.

Main results

• TauCeti.eLpNormLESNormFDerivOneConst_pos: the constant of the Gagliardo–Nirenberg–Sobolev inequality is positive.
• TauCeti.eLpNorm_le_eLpNorm_fderiv_one_of_integrable: the Gagliardo–Nirenberg–Sobolev inequality for integrable C¹ functions.

References

• L. C. Evans, Partial Differential Equations, §5.6.1, Theorem 1.

theorem TauCeti.eLpNormLESNormFDerivOneConst_pos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {p : NNReal} (hp : (↑(Module.finrank ℝ E)).HolderConjugate p) : 0 < MeasureTheory.eLpNormLESNormFDerivOneConst μ ↑p

The constant MeasureTheory.eLpNormLESNormFDerivOneConst μ p of the Gagliardo–Nirenberg– Sobolev inequality MeasureTheory.eLpNorm_le_eLpNorm_fderiv_one is positive.

theorem TauCeti.eLpNorm_le_eLpNorm_fderiv_one_of_integrable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {u : E → F} (hu : ContDiff ℝ 1 u) (hi : MeasureTheory.Integrable u μ) {p : NNReal} (hp : (↑(Module.finrank ℝ E)).HolderConjugate p) : MeasureTheory.eLpNorm u (↑p) μ ≤ ↑(MeasureTheory.eLpNormLESNormFDerivOneConst μ ↑p) * MeasureTheory.eLpNorm (fderiv ℝ u) 1 μ

The Gagliardo–Nirenberg–Sobolev inequality for integrable functions. Let E have dimension n ≥ 2 and let p = n / (n - 1). Every integrable C¹ function u satisfies ‖u‖_p ≤ C ‖Du‖₁, with ‖Du‖₁ finite or infinite, where C is the constant MeasureTheory.eLpNormLESNormFDerivOneConst μ p of the compactly supported case MeasureTheory.eLpNorm_le_eLpNorm_fderiv_one.