Gagliardo-Nirenberg-Sobolev on a bounded domain

EllipticPdes.Embedding.exists_eLpNorm_sobolevConj_le raises the exponent from p to the Sobolev conjugate on a ball inside a ball, the inner ball being where the cutoff feeding the whole-space inequality is one. On a bounded domain with C¹ boundary no ball shrinks: EllipticPdes.Extension.exists_extension_bound puts the class on the whole space with a bound by its seminorms over the domain, the whole-space inequality applies there, and the conclusion restricts back to the domain.

This is the single rung the proof of the Sobolev embedding at order k iterates.

Main declarations

• EllipticPdes.Embedding.isFiniteMeasure_restrict_of_isBounded: a bounded domain has finite measure.
• EllipticPdes.Embedding.exists_eLpNorm_sobolevConj_le_domain: the rung on the domain, with a constant taken before the class.
• EllipticPdes.Embedding.exists_eLpNorm_sobolevConj_le_domain_of_le: the same rung fed by data at a higher exponent.

References

James Guo, Partial Differential Equations (Course Lecture Notes), Theorem III.4.3 and Theorem IV.2.3; L. C. Evans, Partial Differential Equations (2nd ed.), §5.6.1 Theorem 2.

theorem EllipticPdes.Embedding.isFiniteMeasure_restrict_of_isBounded {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩb : Bornology.IsBounded Ω) : MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict Ω)

Finite measure of a bounded domain. Lowering an exponent on it uses this.

theorem EllipticPdes.Embedding.exists_eLpNorm_sobolevConj_le_domain {d : ℕ} (hd : 0 < d) {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩopen : IsOpen Ω) (hΩb : Bornology.IsBounded Ω) (hC1 : Extension.HasC1Boundary Ω) {p p' : NNReal} (hp : 1 ≤ p) (hpp' : (↑p')⁻¹ = (↑p)⁻¹ - (↑d)⁻¹) : ∃ (K : NNReal), ∀ (u : EuclideanSpace ℝ (Fin d) → ℝ) (g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ), MeasureTheory.MemLp u (↑p) (MeasureTheory.volume.restrict Ω) → (∀ (k : Fin d), MeasureTheory.MemLp (g k) (↑p) (MeasureTheory.volume.restrict Ω)) → HasWeakGradOn Ω u g → MeasureTheory.MemLp u (↑p') (MeasureTheory.volume.restrict Ω) ∧ MeasureTheory.eLpNorm u (↑p') (MeasureTheory.volume.restrict Ω) ≤ ↑K * (MeasureTheory.eLpNorm u (↑p) (MeasureTheory.volume.restrict Ω) + ∑ k : Fin d, MeasureTheory.eLpNorm (g k) (↑p) (MeasureTheory.volume.restrict Ω))

Gagliardo-Nirenberg-Sobolev on a bounded domain with C¹ boundary. A class on Ω with an Lᵖ weak gradient lies in L^{p'}(Ω) at the Sobolev conjugate 1/p' = 1/p - 1/d, with one constant, depending on the domain, the dimension and the exponents alone, bounding it by the class and its gradient over the domain.

theorem EllipticPdes.Embedding.exists_eLpNorm_sobolevConj_le_domain_of_le {d : ℕ} (hd : 0 < d) {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩopen : IsOpen Ω) (hΩb : Bornology.IsBounded Ω) (hC1 : Extension.HasC1Boundary Ω) {p q p' : NNReal} (hp : 1 ≤ p) (hpq : p ≤ q) (hpp' : (↑p')⁻¹ = (↑p)⁻¹ - (↑d)⁻¹) : ∃ (K : NNReal), ∀ (u : EuclideanSpace ℝ (Fin d) → ℝ) (g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ), MeasureTheory.MemLp u (↑q) (MeasureTheory.volume.restrict Ω) → (∀ (k : Fin d), MeasureTheory.MemLp (g k) (↑q) (MeasureTheory.volume.restrict Ω)) → HasWeakGradOn Ω u g → MeasureTheory.MemLp u (↑p') (MeasureTheory.volume.restrict Ω) ∧ MeasureTheory.eLpNorm u (↑p') (MeasureTheory.volume.restrict Ω) ≤ ↑K * (MeasureTheory.eLpNorm u (↑q) (MeasureTheory.volume.restrict Ω) + ∑ k : Fin d, MeasureTheory.eLpNorm (g k) (↑q) (MeasureTheory.volume.restrict Ω))

Rung fed by a higher exponent. A bounded domain has finite measure, so Lq data with p ≤ q is Lᵖ data, at the price of a factor |Ω|^{1/p - 1/q} the constant absorbs. This is the form the ladder consumes at every rung above the first.