Sobolev embedding of H₀¹(Ω)

The Gagliardo-Nirenberg-Sobolev inequality ‖u‖_{L^{2⋆}} ≤ C ‖∇u‖_{L²}, with 2⋆ the Sobolev conjugate 1/2⋆ = 1/2 - 1/d, is Mathlib's MeasureTheory.eLpNorm_le_eLpNorm_fderiv_of_eq for a smooth compactly supported function. This file passes it from the test functions to their closure H₀¹(Ω) and bundles the result as a continuous linear map.

Lower semicontinuity in place of continuity

EllipticPdes.Poincare.poincare_H01 extends the Poincaré inequality to H₀¹(Ω) by observing that the estimate is a closed condition on a continuous function of the graph. That argument is unavailable here: the two sides of the Sobolev estimate live at different exponents, and the L^q seminorm of the function coordinate is not a continuous function of the H¹ graph.

What survives is lower semicontinuity. Convergence in H¹ gives convergence of the function coordinate in L²(Ω), hence convergence in measure, and MeasureTheory.eLpNorm_le_of_tendstoInMeasure passes an eventual bound at the exponent q to the limit through Fatou's lemma. The bound along the sequence is not constant, so it is the limit of the right-hand sides that is used, one strict upper bound at a time.

The transfer takes the test-function estimate as a hypothesis at an arbitrary exponent and an arbitrary constant, in the manner of EllipticPdes.Poincare.poincare_H01, so each Gagliardo-Nirenberg-Sobolev variant proved for test functions reaches H₀¹(Ω) by supplying it. Two are supplied: the critical exponent on any Ω, and every exponent below it on a bounded Ω.

Main declarations

• EllipticPdes.Embedding.eLpNorm_testGraph_le: the estimate on a test function at the critical exponent, read off the graph coordinates.
• EllipticPdes.Embedding.eLpNorm_testGraph_le_of_isBounded: the same at every exponent below the critical one, on a bounded domain.
• EllipticPdes.Embedding.eLpNorm_le_of_mem_H01_of_forall_testFn: the transfer principle, from an estimate on test functions to the same estimate on H₀¹(Ω).
• EllipticPdes.Embedding.eLpNorm_le_of_mem_H01 and EllipticPdes.Embedding.eLpNorm_le_of_mem_H01_of_isBounded: the two estimates on H₀¹(Ω).
• EllipticPdes.Embedding.sobolevEmbL: the embedding H₀¹(Ω) →L[ℝ] L^q(Ω) built from such an estimate, with EllipticPdes.Embedding.coeFn_sobolevEmbL identifying it with the function coordinate and EllipticPdes.Embedding.norm_sobolevEmbL_le bounding it by the gradient alone.

References

L. C. Evans, Partial Differential Equations (2nd ed.), §5.6.1, Theorem 1; H. Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations, Corollary 9.9.

noncomputable def EllipticPdes.Embedding.sobolevConst (d : ℕ) : NNReal

Mathlib's Gagliardo-Nirenberg-Sobolev constant at p = 2 on ℝ^d. It depends on the dimension and the exponent alone, not on the function or the domain.

Equations

• EllipticPdes.Embedding.sobolevConst d = MeasureTheory.SNormLESNormFDerivOfEqConst ℝ MeasureTheory.volume ↑2

noncomputable def EllipticPdes.Embedding.sobolevConstOfLe {d : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin d))) (q : NNReal) : NNReal

Mathlib's Gagliardo-Nirenberg-Sobolev constant at p = 2 for an exponent q below the critical one, on a domain of finite measure.

Equations

• EllipticPdes.Embedding.sobolevConstOfLe Ω q = MeasureTheory.eLpNormLESNormFDerivOfLeConst ℝ MeasureTheory.volume Ω 2 q

The estimate on a test function

theorem EllipticPdes.Embedding.eLpNorm_restrict_eq_of_tsupport_subset {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩm : MeasurableSet Ω) {f : EuclideanSpace ℝ (Fin d) → ℝ} (hf : tsupport f ⊆ Ω) (p : ENNReal) : MeasureTheory.eLpNorm f p (MeasureTheory.volume.restrict Ω) = MeasureTheory.eLpNorm f p MeasureTheory.volume

A function supported in Ω has the same Lᵖ seminorm over Ω as over the whole space.

theorem EllipticPdes.Embedding.eLpNorm_fderiv_le_sum {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩm : MeasurableSet Ω) {φ : EuclideanSpace ℝ (Fin d) → ℝ} (h : Sobolev.IsTestFn Ω φ) : MeasureTheory.eLpNorm (fderiv ℝ φ) 2 MeasureTheory.volume ≤ ∑ i : Fin d, ‖h.testGraph.ofLp i.succ‖ₑ

The L² seminorm of the derivative of a test function is bounded by the sum of the L²(Ω) norms of its graph's gradient coordinates.

theorem EllipticPdes.Embedding.eLpNorm_testGraph_zero {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (q : ENNReal) {φ : EuclideanSpace ℝ (Fin d) → ℝ} (h : Sobolev.IsTestFn Ω φ) : MeasureTheory.eLpNorm (↑↑(h.testGraph.ofLp 0)) q (MeasureTheory.volume.restrict Ω) = MeasureTheory.eLpNorm φ q (MeasureTheory.volume.restrict Ω)

The function coordinate of a test graph is the test function.

theorem EllipticPdes.Embedding.eLpNorm_testGraph_le {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {p' : NNReal} (hΩm : MeasurableSet Ω) (hd : 0 < d) (hp' : (↑p')⁻¹ = (↑2)⁻¹ - (↑d)⁻¹) {φ : EuclideanSpace ℝ (Fin d) → ℝ} (h : Sobolev.IsTestFn Ω φ) : MeasureTheory.eLpNorm (↑↑(h.testGraph.ofLp 0)) (↑p') (MeasureTheory.volume.restrict Ω) ≤ ↑(sobolevConst d) * ∑ i : Fin d, ‖h.testGraph.ofLp i.succ‖ₑ

Gagliardo-Nirenberg-Sobolev inequality on a test function, read off the graph coordinates: the L^{2⋆}(Ω) seminorm of the function coordinate is bounded by the sum of the L²(Ω) norms of the gradient coordinates.

theorem EllipticPdes.Embedding.eLpNorm_testGraph_le_of_isBounded {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩm : MeasurableSet Ω) (hΩb : Bornology.IsBounded Ω) (hd : 2 < d) {q : NNReal} (hq : (↑2)⁻¹ - (↑d)⁻¹ ≤ (↑q)⁻¹) {φ : EuclideanSpace ℝ (Fin d) → ℝ} (h : Sobolev.IsTestFn Ω φ) : MeasureTheory.eLpNorm (↑↑(h.testGraph.ofLp 0)) (↑q) (MeasureTheory.volume.restrict Ω) ≤ ↑(sobolevConstOfLe Ω q) * ∑ i : Fin d, ‖h.testGraph.ofLp i.succ‖ₑ

Gagliardo-Nirenberg-Sobolev inequality on a test function at a subcritical exponent. On a bounded domain the estimate is available at every q with 1/q ≥ 1/2 - 1/d, the critical exponent included, since the domain has finite measure. The dimension must exceed 2, which is what the critical exponent asks for.

The transfer to H₀¹(Ω)

theorem EllipticPdes.Embedding.norm_apply_le {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (U : Sobolev.H1amb Ω) (j : Fin (d + 1)) : ‖U.ofLp j‖ ≤ ‖U‖

Each coordinate of the graph is bounded by the ambient H¹ norm.

theorem EllipticPdes.Embedding.eLpNorm_le_of_mem_H01_of_forall_testFn {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {q : ENNReal} {C : NNReal} (hbase : ∀ {φ : EuclideanSpace ℝ (Fin d) → ℝ} (h : Sobolev.IsTestFn Ω φ), MeasureTheory.eLpNorm (↑↑(h.testGraph.ofLp 0)) q (MeasureTheory.volume.restrict Ω) ≤ ↑C * ∑ i : Fin d, ‖h.testGraph.ofLp i.succ‖ₑ) {U : Sobolev.H1amb Ω} (hU : U ∈ Sobolev.H01 Ω) : MeasureTheory.eLpNorm (↑↑(U.ofLp 0)) q (MeasureTheory.volume.restrict Ω) ≤ ↑C * ∑ i : Fin d, ‖U.ofLp i.succ‖ₑ

Transfer principle. An estimate of the function coordinate by the gradient coordinates, valid on every test graph, is valid on all of H₀¹(Ω).

The two sides live at different exponents, so the estimate is not a closed condition on a continuous function of the graph, as it is for the Poincaré inequality (EllipticPdes.Poincare.poincare_H01). It is still lower semicontinuous: the test graphs converging to U in H¹ have function coordinates converging in L²(Ω), hence in measure, and Fatou's lemma passes the bound to the limit.

theorem EllipticPdes.Embedding.eLpNorm_le_of_mem_H01 {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {p' : NNReal} (hΩm : MeasurableSet Ω) (hd : 0 < d) (hp' : (↑p')⁻¹ = (↑2)⁻¹ - (↑d)⁻¹) {U : Sobolev.H1amb Ω} (hU : U ∈ Sobolev.H01 Ω) : MeasureTheory.eLpNorm (↑↑(U.ofLp 0)) (↑p') (MeasureTheory.volume.restrict Ω) ≤ ↑(sobolevConst d) * ∑ i : Fin d, ‖U.ofLp i.succ‖ₑ

Sobolev estimate on H₀¹(Ω) at the critical exponent.

theorem EllipticPdes.Embedding.eLpNorm_le_of_mem_H01_of_isBounded {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩm : MeasurableSet Ω) (hΩb : Bornology.IsBounded Ω) (hd : 2 < d) {q : NNReal} (hq : (↑2)⁻¹ - (↑d)⁻¹ ≤ (↑q)⁻¹) {U : Sobolev.H1amb Ω} (hU : U ∈ Sobolev.H01 Ω) : MeasureTheory.eLpNorm (↑↑(U.ofLp 0)) (↑q) (MeasureTheory.volume.restrict Ω) ≤ ↑(sobolevConstOfLe Ω q) * ∑ i : Fin d, ‖U.ofLp i.succ‖ₑ

Sobolev estimate on H₀¹(Ω) at every exponent up to the critical one, on a bounded domain.

theorem EllipticPdes.Embedding.memLp_of_mem_H01 {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {q : ENNReal} {C : NNReal} {U : Sobolev.H1amb Ω} (hbound : MeasureTheory.eLpNorm (↑↑(U.ofLp 0)) q (MeasureTheory.volume.restrict Ω) ≤ ↑C * ∑ i : Fin d, ‖U.ofLp i.succ‖ₑ) : MeasureTheory.MemLp (↑↑(U.ofLp 0)) q (MeasureTheory.volume.restrict Ω)

An element of H₀¹(Ω) is L^q(Ω) at any exponent the estimate reaches.

The embedding as a continuous linear map

theorem EllipticPdes.Embedding.sum_enorm_succ_le {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (U : ↥(Sobolev.H01 Ω)) : ∑ i : Fin d, ‖(↑U).ofLp i.succ‖ₑ ≤ ENNReal.ofReal (↑d * ‖U‖)

The sum of the gradient coordinates of an element of H₀¹(Ω), bounded through the ambient norm one coordinate at a time.

noncomputable def EllipticPdes.Embedding.sobolevEmbL {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {q : ENNReal} [Fact (1 ≤ q)] {C : NNReal} (hbound : ∀ U ∈ Sobolev.H01 Ω, MeasureTheory.eLpNorm (↑↑(U.ofLp 0)) q (MeasureTheory.volume.restrict Ω) ≤ ↑C * ∑ i : Fin d, ‖U.ofLp i.succ‖ₑ) : ↥(Sobolev.H01 Ω) →L[ℝ] ↥(MeasureTheory.Lp ℝ q (MeasureTheory.volume.restrict Ω))

Sobolev embedding H₀¹(Ω) →L[ℝ] L^q(Ω), built from an estimate of the function coordinate by the gradient coordinates. The map sends an element of H₀¹(Ω) to its function coordinate, read at the exponent q.

The operator-norm bound supplied here is C * d, from the coordinate bound ‖U i‖ ≤ ‖U‖ applied d times. norm_sobolevEmbL_le states the sharper bound, by the gradient coordinates themselves.

Equations

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

@[simp]

theorem EllipticPdes.Embedding.coeFn_sobolevEmbL {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {q : ENNReal} [Fact (1 ≤ q)] {C : NNReal} (hbound : ∀ U ∈ Sobolev.H01 Ω, MeasureTheory.eLpNorm (↑↑(U.ofLp 0)) q (MeasureTheory.volume.restrict Ω) ≤ ↑C * ∑ i : Fin d, ‖U.ofLp i.succ‖ₑ) (U : ↥(Sobolev.H01 Ω)) : ↑↑((sobolevEmbL hbound) U) =ᵐ[MeasureTheory.volume.restrict Ω] ↑↑((↑U).ofLp 0)

theorem EllipticPdes.Embedding.norm_sobolevEmbL_le {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {q : ENNReal} [Fact (1 ≤ q)] {C : NNReal} (hbound : ∀ U ∈ Sobolev.H01 Ω, MeasureTheory.eLpNorm (↑↑(U.ofLp 0)) q (MeasureTheory.volume.restrict Ω) ≤ ↑C * ∑ i : Fin d, ‖U.ofLp i.succ‖ₑ) (U : ↥(Sobolev.H01 Ω)) : ‖(sobolevEmbL hbound) U‖ ≤ ↑C * ∑ i : Fin d, ‖(↑U).ofLp i.succ‖

The embedding is bounded by the gradient coordinates alone, with no Poincaré inequality and no bound on the domain.