Sobolev embedding of H₀¹(Ω) in dimension two

In dimension two the critical exponent of H¹ is infinite and the Gagliardo-Nirenberg-Sobolev inequality at p = 2 is unavailable, since it asks p < d. On a bounded domain the embedding into L⁴ still follows from the inequality at p = 3/2 < 2, whose conjugate exponent is 6, together with Hölder's inequality ‖∇u‖_{L^{3/2}(Ω)} ≤ |Ω|^{1/6} ‖∇u‖_{L²(Ω)}. This is the remark on n = 2 in the proof of Gilbarg and Trudinger's Theorem 8.1, where any exponent above 2 serves.

Main declarations

• EllipticPdes.Embedding.sobolevConstTwo: the constant.
• EllipticPdes.Embedding.eLpNorm_testGraph_le_two: the estimate on a test function.
• EllipticPdes.Embedding.eLpNorm_le_of_mem_H01_two: the estimate on H₀¹(Ω).

References

D. Gilbarg and N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, §8.1 Theorem 8.1 (p. 180), the remark on n = 2.

noncomputable def EllipticPdes.Embedding.sobolevConstTwo (Ω : Set (EuclideanSpace ℝ (Fin 2))) : NNReal

The constant of the two-dimensional embedding into L⁴: Mathlib's constant at p = 3/2, q = 4, times the Hölder factor |Ω|^{1/6}.

Equations

• EllipticPdes.Embedding.sobolevConstTwo Ω = MeasureTheory.eLpNormLESNormFDerivOfLeConst ℝ MeasureTheory.volume Ω (3 / 2) 4 * (MeasureTheory.volume Ω).toNNReal ^ (1 / 6)

theorem EllipticPdes.Embedding.eLpNorm_restrict_eq_of_tsupport_subset' {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩm : MeasurableSet Ω) {F : Type u_1} [NormedAddCommGroup F] {f : EuclideanSpace ℝ (Fin d) → F} (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, for functions into any normed group.

theorem EllipticPdes.Embedding.eLpNorm_testGraph_le_two {Ω : Set (EuclideanSpace ℝ (Fin 2))} (hΩm : MeasurableSet Ω) (hΩb : Bornology.IsBounded Ω) {φ : EuclideanSpace ℝ (Fin 2) → ℝ} (h : Sobolev.IsTestFn Ω φ) : MeasureTheory.eLpNorm (↑↑(h.testGraph.ofLp 0)) 4 (MeasureTheory.volume.restrict Ω) ≤ ↑(sobolevConstTwo Ω) * ∑ i : Fin 2, ‖h.testGraph.ofLp i.succ‖ₑ

Two-dimensional Sobolev inequality on a test function: the L⁴(Ω) seminorm of the function coordinate is bounded by the sum of the L²(Ω) norms of the gradient coordinates.

theorem EllipticPdes.Embedding.eLpNorm_le_of_mem_H01_two {Ω : Set (EuclideanSpace ℝ (Fin 2))} (hΩm : MeasurableSet Ω) (hΩb : Bornology.IsBounded Ω) {U : Sobolev.H1amb Ω} (hU : U ∈ Sobolev.H01 Ω) : MeasureTheory.eLpNorm (↑↑(U.ofLp 0)) 4 (MeasureTheory.volume.restrict Ω) ≤ ↑(sobolevConstTwo Ω) * ∑ i : Fin 2, ‖U.ofLp i.succ‖ₑ

Sobolev estimate on H₀¹(Ω) in dimension two, into L⁴(Ω).