Gagliardo-Nirenberg-Sobolev inequality

In this file we prove the Gagliardo-Nirenberg-Sobolev inequality. This states that for compactly supported C¹-functions between finite dimensional vector spaces, we can bound the L^p-norm of u by the L^q norm of the derivative of u. The bound is up to a constant that is independent of the function u. Let n be the dimension of the domain.

The main step in the proof, which we dubbed the "grid-lines lemma" below, is a complicated inductive argument that involves manipulating an n+1-fold iterated integral and a product of n+2 factors. In each step, one pushes one of the integral inside (all but one of) the factors of the product using Hölder's inequality. The precise formulation of the induction hypothesis (MeasureTheory.GridLines.T_insert_le_T_lmarginal_singleton) is tricky, and none of the 5 sources we referenced stated it.

In the formalization we use the operation MeasureTheory.lmarginal to work with the iterated integrals, and use MeasureTheory.lmarginal_insert' to conveniently push one of the integrals inside. The Hölder's inequality step is done using ENNReal.lintegral_mul_prod_norm_pow_le.

The conclusions of the main results below are an estimation up to a constant multiple. We don't really care about this constant, other than that it only depends on some pieces of data, typically E, μ, p and sometimes also the codomain of u or the support of u. We state these constants as separate definitions.

Main results

• MeasureTheory.eLpNorm_le_eLpNorm_fderiv_of_eq: The bound holds for 1 ≤ p, 0 < n and q⁻¹ = p⁻¹ - n⁻¹
• MeasureTheory.eLpNorm_le_eLpNorm_fderiv_of_le: The bound holds when 1 ≤ p < n, 0 ≤ q and p⁻¹ - n⁻¹ ≤ q⁻¹. Note that in this case the constant depends on the support of u.

Potentially also useful:

• MeasureTheory.eLpNorm_le_eLpNorm_fderiv_one: this is the inequality for q = 1. In this version, the codomain can be an arbitrary Banach space.
• MeasureTheory.eLpNorm_le_eLpNorm_fderiv_of_eq_inner: in this version, the codomain is assumed to be a Hilbert space, without restrictions on its dimension.

The grid-lines lemma

def MeasureTheory.GridLines.T {ι : Type u_1} {A : ι → Type u_2} [(i : ι) → MeasurableSpace (A i)] (μ : (i : ι) → Measure (A i)) [DecidableEq ι] (p : ℝ) (f : ((i : ι) → A i) → ENNReal) (s : Finset ι) : ((i : ι) → A i) → ENNReal

The "grid-lines operation" (not a standard name) which is central in the inductive proof of the Sobolev inequality.

For a finite dependent product Π i : ι, A i of sigma-finite measure spaces, a finite set s of indices from ι, and a (later assumed nonnegative) real number p, this operation acts on a function f from Π i, A i into the extended nonnegative reals. The operation is to partially integrate, in the s co-ordinates, the function whose value at x : Π i, A i is obtained by multiplying a certain power of f with the product, for each co-ordinate i in s, of a certain power of the integral of f along the "grid line" in the i direction through x.

We are most interested in this operation when the set s is the universe in ι, but as a proxy for "induction on dimension" we define it for a general set s of co-ordinates: the s-grid-lines operation on a function f which is constant along the co-ordinates in sᶜ is morally (that is, up to type-theoretic nonsense) the same thing as the universe-grid-lines operation on the associated function on the "lower-dimensional" space Π i : s, A i.

Equations

• MeasureTheory.GridLines.T μ p f s = ∫⋯∫⁻_s, f ^ (1 - (↑s.card - 1) * p) * ∏ i ∈ s, (∫⋯∫⁻_{i}, f ∂μ) ^ p ∂μ

@[simp]

theorem MeasureTheory.GridLines.T_univ {ι : Type u_1} {A : ι → Type u_2} [(i : ι) → MeasurableSpace (A i)] (μ : (i : ι) → Measure (A i)) [DecidableEq ι] {p : ℝ} [Fintype ι] [∀ (i : ι), SigmaFinite (μ i)] (f : ((i : ι) → A i) → ENNReal) (x : (i : ι) → A i) : T μ p f Finset.univ x = ∫⁻ (x : (i : ι) → A i), f x ^ (1 - (↑(Fintype.card ι) - 1) * p) * ∏ i : ι, (∫⁻ (t : A i), f (Function.update x i t) ∂μ i) ^ p ∂Measure.pi μ

@[simp]

theorem MeasureTheory.GridLines.T_empty {ι : Type u_1} {A : ι → Type u_2} [(i : ι) → MeasurableSpace (A i)] (μ : (i : ι) → Measure (A i)) [DecidableEq ι] {p : ℝ} (f : ((i : ι) → A i) → ENNReal) (x : (i : ι) → A i) : T μ p f ∅ x = f x ^ (1 + p)

theorem MeasureTheory.GridLines.T_insert_le_T_lmarginal_singleton {ι : Type u_1} {A : ι → Type u_2} [(i : ι) → MeasurableSpace (A i)] (μ : (i : ι) → Measure (A i)) [DecidableEq ι] {p : ℝ} [∀ (i : ι), SigmaFinite (μ i)] (hp₀ : 0 ≤ p) (s : Finset ι) (hp : ↑s.card * p ≤ 1) (i : ι) (hi : i ∉ s) {f : ((i : ι) → A i) → ENNReal} (hf : Measurable f) : T μ p f (insert i s) ≤ T μ p (∫⋯∫⁻_{i}, f ∂μ) s

The main inductive step in the grid-lines lemma for the Gagliardo-Nirenberg-Sobolev inequality.

The grid-lines operation GridLines.T on a nonnegative function on a finitary product type is less than or equal to the grid-lines operation of its partial integral in one co-ordinate (the latter intuitively considered as a function on a space "one dimension down").

theorem MeasureTheory.GridLines.T_lmarginal_antitone {ι : Type u_1} {A : ι → Type u_2} [(i : ι) → MeasurableSpace (A i)] (μ : (i : ι) → Measure (A i)) [DecidableEq ι] {p : ℝ} [Fintype ι] [∀ (i : ι), SigmaFinite (μ i)] (hp₀ : 0 ≤ p) (hp : (↑(Fintype.card ι) - 1) * p ≤ 1) {f : ((i : ι) → A i) → ENNReal} (hf : Measurable f) : Antitone fun (s : Finset ι) => T μ p (∫⋯∫⁻_sᶜ, f ∂μ) s

Auxiliary result for the grid-lines lemma. Given a nonnegative function on a finitary product type indexed by ι, and a set s in ι, consider partially integrating over the variables in sᶜ and performing the "grid-lines operation" (see GridLines.T) to the resulting function in the variables s. This theorem states that this operation decreases as the number of grid-lines taken increases.

theorem MeasureTheory.lintegral_mul_prod_lintegral_pow_le {ι : Type u_1} {A : ι → Type u_2} [(i : ι) → MeasurableSpace (A i)] (μ : (i : ι) → Measure (A i)) [DecidableEq ι] [Fintype ι] [∀ (i : ι), SigmaFinite (μ i)] {p : ℝ} (hp₀ : 0 ≤ p) (hp : (↑(Fintype.card ι) - 1) * p ≤ 1) {f : ((i : ι) → A i) → ENNReal} (hf : Measurable f) : ∫⁻ (x : (i : ι) → A i), f x ^ (1 - (↑(Fintype.card ι) - 1) * p) * ∏ i : ι, (∫⁻ (xᵢ : A i), f (Function.update x i xᵢ) ∂μ i) ^ p ∂Measure.pi μ ≤ (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi μ) ^ (1 + p)

The "grid-lines lemma" (not a standard name), stated with a general parameter p as the exponent. Compare with lintegral_prod_lintegral_pow_le.

For any finite dependent product Π i : ι, A i of sigma-finite measure spaces, for any nonnegative real number p such that (#ι - 1) * p ≤ 1, for any function f from Π i, A i into the extended nonnegative reals, we consider an associated "grid-lines quantity", the integral of an associated function from Π i, A i into the extended nonnegative reals. The value of this function at x : Π i, A i is obtained by multiplying a certain power of f with the product, for each co-ordinate i, of a certain power of the integral of f along the "grid line" in the i direction through x.

This lemma bounds the Lebesgue integral of the grid-lines quantity by a power of the Lebesgue integral of f.

theorem MeasureTheory.lintegral_prod_lintegral_pow_le {ι : Type u_1} {A : ι → Type u_2} [(i : ι) → MeasurableSpace (A i)] (μ : (i : ι) → Measure (A i)) [DecidableEq ι] [Fintype ι] [∀ (i : ι), SigmaFinite (μ i)] {p : ℝ} (hp : (↑(Fintype.card ι)).HolderConjugate p) {f : ((a : ι) → A a) → ENNReal} (hf : Measurable f) : ∫⁻ (x : (i : ι) → A i), ∏ i : ι, (∫⁻ (xᵢ : A i), f (Function.update x i xᵢ) ∂μ i) ^ (1 / (↑(Fintype.card ι) - 1)) ∂Measure.pi μ ≤ (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi μ) ^ p

Special case of the grid-lines lemma lintegral_mul_prod_lintegral_pow_le, taking the extremal exponent p = (#ι - 1)⁻¹.

The Gagliardo-Nirenberg-Sobolev inequality

theorem MeasureTheory.lintegral_pow_le_pow_lintegral_fderiv_aux {ι : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] [Fintype ι] {p : ℝ} (hp : (↑(Fintype.card ι)).HolderConjugate p) {u : (ι → ℝ) → F} (hu : ContDiff ℝ 1 u) (h2u : HasCompactSupport u) : ∫⁻ (x : ι → ℝ), ‖u x‖ₑ ^ p ≤ (∫⁻ (x : ι → ℝ), ‖fderiv ℝ u x‖ₑ) ^ p

The Gagliardo-Nirenberg-Sobolev inequality. Let u be a continuously differentiable compactly-supported function u on ℝⁿ, for n ≥ 2. (More literally we encode ℝⁿ as ι → ℝ where n := #ι is finite and at least 2.) Then the Lebesgue integral of the pointwise expression |u x| ^ (n / (n - 1)) is bounded above by the n / (n - 1)-th power of the Lebesgue integral of the Fréchet derivative of u.

For a basis-free version, see lintegral_pow_le_pow_lintegral_fderiv.

theorem MeasureTheory.lintegralPowLePowLIntegralFDerivConst_def {E : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] (p : ℝ) : lintegralPowLePowLIntegralFDerivConst μ p = let ι := Fin (Module.finrank ℝ E); have this := ⋯; let e := ContinuousLinearEquiv.ofFinrankEq this; have c := μ.addHaarScalarFactor (Measure.map (⇑e.symm) volume); c * ‖↑e.symm‖₊ ^ p * (c ^ p)⁻¹

@[irreducible]

def MeasureTheory.lintegralPowLePowLIntegralFDerivConst {E : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] (p : ℝ) : NNReal

The constant factor occurring in the conclusion of lintegral_pow_le_pow_lintegral_fderiv. It only depends on E, μ and p. It is determined by the ratio of the measures on E and ℝⁿ and the operator norm of a chosen equivalence E ≃ ℝⁿ (raised to suitable powers involving p).

Equations

• One or more equations did not get rendered due to their size.

theorem MeasureTheory.lintegral_pow_le_pow_lintegral_fderiv {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] {u : E → F} (hu : ContDiff ℝ 1 u) (h2u : HasCompactSupport u) {p : ℝ} (hp : (↑(Module.finrank ℝ E)).HolderConjugate p) : ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂μ ≤ ↑(lintegralPowLePowLIntegralFDerivConst μ p) * (∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ∂μ) ^ p

The Gagliardo-Nirenberg-Sobolev inequality. Let u be a continuously differentiable compactly-supported function u on a normed space E of finite dimension n ≥ 2, equipped with Haar measure. Then the Lebesgue integral of the pointwise expression |u x| ^ (n / (n - 1)) is bounded above by a constant times the n / (n - 1)-th power of the Lebesgue integral of the Fréchet derivative of u.

theorem MeasureTheory.eLpNormLESNormFDerivOneConst_def {E : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] (p : ℝ) : eLpNormLESNormFDerivOneConst μ p = lintegralPowLePowLIntegralFDerivConst μ p ^ p⁻¹

@[irreducible]

def MeasureTheory.eLpNormLESNormFDerivOneConst {E : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] (p : ℝ) : NNReal

The constant factor occurring in the conclusion of eLpNorm_le_eLpNorm_fderiv_one. It only depends on E, μ and p.

Equations

• MeasureTheory.eLpNormLESNormFDerivOneConst μ p = MeasureTheory.lintegralPowLePowLIntegralFDerivConst μ p ^ p⁻¹

theorem MeasureTheory.eLpNorm_le_eLpNorm_fderiv_one {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] {u : E → F} (hu : ContDiff ℝ 1 u) (h2u : HasCompactSupport u) {p : NNReal} (hp : (↑(Module.finrank ℝ E)).HolderConjugate p) : eLpNorm u (↑p) μ ≤ ↑(eLpNormLESNormFDerivOneConst μ ↑p) * eLpNorm (fderiv ℝ u) 1 μ

The Gagliardo-Nirenberg-Sobolev inequality. Let u be a continuously differentiable compactly-supported function u on a normed space E of finite dimension n ≥ 2, equipped with Haar measure. Then the Lᵖ norm of u, where p := n / (n - 1), is bounded above by a constant times the L¹ norm of the Fréchet derivative of u.

def MeasureTheory.eLpNormLESNormFDerivOfEqInnerConst {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] (p : ℝ) : NNReal

The constant factor occurring in the conclusion of eLpNorm_le_eLpNorm_fderiv_of_eq_inner. It only depends on E, μ and p.

Equations

• One or more equations did not get rendered due to their size.

theorem MeasureTheory.eLpNorm_le_eLpNorm_fderiv_of_eq_inner {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] {F' : Type u_5} [NormedAddCommGroup F'] [InnerProductSpace ℝ F'] {u : E → F'} (hu : ContDiff ℝ 1 u) (h2u : HasCompactSupport u) {p p' : NNReal} (hp : 1 ≤ p) (hn : 0 < Module.finrank ℝ E) (hp' : (↑p')⁻¹ = ↑p⁻¹ - (↑(Module.finrank ℝ E))⁻¹) : eLpNorm u (↑p') μ ≤ ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑p) * eLpNorm (fderiv ℝ u) (↑p) μ

The Gagliardo-Nirenberg-Sobolev inequality. Let u be a continuously differentiable compactly-supported function u on a normed space E of finite dimension n, equipped with Haar measure, let 1 ≤ p < n and let p'⁻¹ := p⁻¹ - n⁻¹. Then the Lᵖ' norm of u is bounded above by a constant times the Lᵖ norm of the Fréchet derivative of u.

Note: The codomain of u needs to be a Hilbert space.

theorem MeasureTheory.SNormLESNormFDerivOfEqConst_def (F : Type u_6) [NormedAddCommGroup F] [NormedSpace ℝ F] {E : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] [FiniteDimensional ℝ F] (p : ℝ) : SNormLESNormFDerivOfEqConst F μ p = let F' := EuclideanSpace ℝ (Fin (Module.finrank ℝ F)); have e := toEuclidean; ‖↑e.symm‖₊ * eLpNormLESNormFDerivOfEqInnerConst μ p * ‖↑e‖₊

@[irreducible]

def MeasureTheory.SNormLESNormFDerivOfEqConst (F : Type u_6) [NormedAddCommGroup F] [NormedSpace ℝ F] {E : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] [FiniteDimensional ℝ F] (p : ℝ) : NNReal

The constant factor occurring in the conclusion of eLpNorm_le_eLpNorm_fderiv_of_eq. It only depends on E, F, μ and p.

Equations

• One or more equations did not get rendered due to their size.

theorem MeasureTheory.eLpNorm_le_eLpNorm_fderiv_of_eq {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] [FiniteDimensional ℝ F] {u : E → F} (hu : ContDiff ℝ 1 u) (h2u : HasCompactSupport u) {p p' : NNReal} (hp : 1 ≤ p) (hn : 0 < Module.finrank ℝ E) (hp' : (↑p')⁻¹ = ↑p⁻¹ - (↑(Module.finrank ℝ E))⁻¹) : eLpNorm u (↑p') μ ≤ ↑(SNormLESNormFDerivOfEqConst F μ ↑p) * eLpNorm (fderiv ℝ u) (↑p) μ

The Gagliardo-Nirenberg-Sobolev inequality. Let u be a continuously differentiable compactly-supported function u on a normed space E of finite dimension n, equipped with Haar measure, let 1 < p < n and let p'⁻¹ := p⁻¹ - n⁻¹. Then the Lᵖ' norm of u is bounded above by a constant times the Lᵖ norm of the Fréchet derivative of u.

This is the version where the codomain of u is a finite dimensional normed space.

@[irreducible]

def MeasureTheory.eLpNormLESNormFDerivOfLeConst (F : Type u_6) [NormedAddCommGroup F] [NormedSpace ℝ F] {E : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] [FiniteDimensional ℝ F] (s : Set E) (p q : NNReal) : NNReal

The constant factor occurring in the conclusion of eLpNorm_le_eLpNorm_fderiv_of_le. It only depends on F, μ, s, p and q.

Equations

• MeasureTheory.eLpNormLESNormFDerivOfLeConst F μ s p q = have p' := (p⁻¹ - (↑(Module.finrank ℝ E))⁻¹)⁻¹; (μ s).toNNReal ^ (1 / ↑q - 1 / ↑p') * MeasureTheory.SNormLESNormFDerivOfEqConst F μ ↑p

theorem MeasureTheory.eLpNormLESNormFDerivOfLeConst_def (F : Type u_6) [NormedAddCommGroup F] [NormedSpace ℝ F] {E : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] [FiniteDimensional ℝ F] (s : Set E) (p q : NNReal) : eLpNormLESNormFDerivOfLeConst F μ s p q = have p' := (p⁻¹ - (↑(Module.finrank ℝ E))⁻¹)⁻¹; (μ s).toNNReal ^ (1 / ↑q - 1 / ↑p') * SNormLESNormFDerivOfEqConst F μ ↑p

theorem MeasureTheory.eLpNorm_le_eLpNorm_fderiv_of_le {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] [FiniteDimensional ℝ F] {u : E → F} {s : Set E} (hu : ContDiff ℝ 1 u) (h2u : Function.support u ⊆ s) {p q : NNReal} (hp : 1 ≤ p) (h2p : p < ↑(Module.finrank ℝ E)) (hpq : ↑p⁻¹ - (↑(Module.finrank ℝ E))⁻¹ ≤ (↑q)⁻¹) (hs : Bornology.IsBounded s) : eLpNorm u (↑q) μ ≤ ↑(eLpNormLESNormFDerivOfLeConst F μ s p q) * eLpNorm (fderiv ℝ u) (↑p) μ

The Gagliardo-Nirenberg-Sobolev inequality. Let u be a continuously differentiable function u supported in a bounded set s in a normed space E of finite dimension n, equipped with Haar measure, and let 1 < p < n and 0 < q ≤ (p⁻¹ - (finrank ℝ E : ℝ)⁻¹)⁻¹. Then the L^q norm of u is bounded above by a constant times the Lᵖ norm of the Fréchet derivative of u.

Note: The codomain of u needs to be a finite dimensional normed space.

theorem MeasureTheory.eLpNorm_le_eLpNorm_fderiv {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] [FiniteDimensional ℝ F] {u : E → F} {s : Set E} (hu : ContDiff ℝ 1 u) (h2u : Function.support u ⊆ s) {p : NNReal} (hp : 1 ≤ p) (h2p : p < ↑(Module.finrank ℝ E)) (hs : Bornology.IsBounded s) : eLpNorm u (↑p) μ ≤ ↑(eLpNormLESNormFDerivOfLeConst F μ s p p) * eLpNorm (fderiv ℝ u) (↑p) μ

The Gagliardo-Nirenberg-Sobolev inequality. Let u be a continuously differentiable function u supported in a bounded set s in a normed space E of finite dimension n, equipped with Haar measure, and let 1 < p < n. Then the Lᵖ norm of u is bounded above by a constant times the Lᵖ norm of the Fréchet derivative of u.

Note: The codomain of u needs to be a finite dimensional normed space.