Rellich-Kondrachov on the whole graph space

EllipticPdes.Sobolev.embL2_isCompact is the compact embedding of H₀¹(Ω) into L²(Ω) on a bounded measurable domain. Its proof extends each class by zero and applies the Fréchet-Kolmogorov criterion to the extensions, whose translation modulus is bounded by the gradient because a class in H₀¹(Ω) is a limit of test functions. An element of the graph space W12 Ω, the H¹(Ω) of this development, has no such approximation: extended by zero it jumps at the boundary, and the translation modulus is lost.

The extension operator restores it. On a bounded open domain with C¹ boundary, EllipticPdes.Extension.exists_extLinear puts every element of W12 Ω on the whole space, with compact support in a fixed ball, a weak gradient on ℝᵈ, and a bound by the norm of the element. The whole-space translation estimate for a class with a weak gradient, transL2_toLp_sub_le_of_hasWeakGradOn_univ, proved by mollifying the class and passing the smooth estimate to the limit, gives the modulus, and the Fréchet-Kolmogorov criterion gives total boundedness of the extensions. Restricting back to Ω, through the restriction map of the regularity chapter, is continuous, so the image of the unit ball of W12 Ω in L²(Ω) is totally bounded and the embedding is compact.

Main declarations

• EllipticPdes.Sobolev.transL2_toLp_sub_le_of_hasWeakGradOn_univ: the translation modulus of a whole-space class with an L² weak gradient.
• EllipticPdes.Sobolev.embW12: the embedding W12 Ω →L[ℝ] L²(Ω).
• EllipticPdes.Sobolev.embW12_isCompact: that embedding is compact on a bounded open domain with C¹ boundary.

References

L. C. Evans, Partial Differential Equations (2nd ed.), §5.7 Theorem 1 (p. 286); James Guo, Partial Differential Equations (Course Lecture Notes), Theorem IV.2.10.

The translation modulus of a whole-space Sobolev class

theorem EllipticPdes.Sobolev.norm_toLp_sq_eq_integral_sq {d : ℕ} {F : EuclideanSpace ℝ (Fin d) → ℝ} (hF : MeasureTheory.MemLp F 2 MeasureTheory.volume) : ‖MeasureTheory.MemLp.toLp F hF‖ ^ 2 = ∫ (x : EuclideanSpace ℝ (Fin d)), F x ^ 2

The squared L² norm of the L² class of a function is the integral of the square.

theorem EllipticPdes.Sobolev.transL2_toLp_sub_le_of_hasWeakGradOn_univ {d : ℕ} {F : EuclideanSpace ℝ (Fin d) → ℝ} {G : Fin d → EuclideanSpace ℝ (Fin d) → ℝ} (hFcs : HasCompactSupport F) (hFint : MeasureTheory.Integrable F MeasureTheory.volume) (hF : MeasureTheory.MemLp F 2 MeasureTheory.volume) (hG : ∀ (k : Fin d), MeasureTheory.MemLp (G k) 2 MeasureTheory.volume) (hwg : Embedding.HasWeakGradOn Set.univ F G) (h : EuclideanSpace ℝ (Fin d)) : ‖(MeasureTheory.transL2 h) (MeasureTheory.MemLp.toLp F hF) - MeasureTheory.MemLp.toLp F hF‖ ≤ (∑ k : Fin d, (MeasureTheory.eLpNorm (G k) 2 MeasureTheory.volume).toReal) * ‖h‖

Translation modulus of a whole-space class with a weak gradient. A compactly supported class on ℝᵈ with an L² weak gradient moves under translation by at most the length of the translation times the sum of the L² norms of its gradient components. The class is mollified, the smooth estimate integral_sq_sub_translation_le applies to each mollification, whose gradient is the mollified weak gradient and is bounded in L² by the weak gradient itself, and the estimate passes to the L² limit.

The embedding of the graph space

noncomputable def EllipticPdes.Sobolev.embW12 {d : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin d))) : ↥(W12 Ω) →L[ℝ] L2D Ω

The coordinate-0 embedding H¹(Ω) ↪ L²(Ω), U ↦ U 0, on the graph space W12 Ω.

Equations

• EllipticPdes.Sobolev.embW12 Ω = PiLp.proj 2 (fun (x : Fin (d + 1)) => EllipticPdes.Sobolev.L2D Ω) 0 ∘SL (EllipticPdes.Sobolev.W12 Ω).subtypeL

@[simp]

theorem EllipticPdes.Sobolev.embW12_apply {d : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin d))) (U : ↥(W12 Ω)) : (embW12 Ω) U = (↑U).ofLp 0

theorem EllipticPdes.Sobolev.embW12_isCompact {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hd : 0 < d) (hΩopen : IsOpen Ω) (hΩb : Bornology.IsBounded Ω) (hC1 : Extension.HasC1Boundary Ω) : IsCompactOperator ⇑(embW12 Ω)

Rellich-Kondrachov on H¹(Ω) (Evans §5.7 Theorem 1 at p = q = 2, Guo Theorem IV.2.10). On a bounded open domain with C¹ boundary, the embedding of the graph space W12 Ω into L²(Ω) is a compact operator.

theorem EllipticPdes.Sobolev.embW12_isCompact_ball {d : ℕ} (hd : 0 < d) : IsCompactOperator ⇑(embW12 (Metric.ball 0 1))

Rellich-Kondrachov on H¹ of the unit ball, every hypothesis discharged.