Discharging the Rellich-Kondrachov compact embedding

Compactness.lean reduces the Fredholm theory to the single analytic hypothesis IsCompactOperator (embL2 Ω), the Rellich-Kondrachov compact embedding H₀¹(Ω) ↪ L²(Ω). This file proves it for bounded measurable Ω, consuming the Fréchet-Kolmogorov engine built in EllipticPdes.Analysis.*.

The argument sends embL2 Ω U = U 0 ∈ L²(Ω) to its extension by zero in L²(ℝᵈ), where the Fréchet-Kolmogorov criterion totallyBounded_of_lipschitz_translation applies: the family is uniformly bounded, supported in a fixed ball (Ω bounded), and uniformly Lipschitz under translation. The translation modulus comes from the gradient estimate integral_sq_sub_translation_le on the smooth approximants, passed to the limit through transL2_sub_le_of_tendsto'.

theorem EllipticPdes.Sobolev.extCls_ae {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩm : MeasurableSet Ω) {φ : EuclideanSpace ℝ (Fin d) → ℝ} (h : IsTestFn Ω φ) : ↑↑((MeasureTheory.lpExtendByZero MeasureTheory.volume 2 Ω hΩm) h.testCls) =ᵐ[MeasureTheory.volume] φ

Extension of a test class is the function. The extension by zero of the L²(Ω) class of a test function φ equals φ almost everywhere on ℝᵈ, since φ is supported in Ω.

theorem EllipticPdes.Sobolev.partialCls_norm_sq_eq {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {φ : EuclideanSpace ℝ (Fin d) → ℝ} (h : IsTestFn Ω φ) (i : Fin d) : ‖h.partialCls i‖ ^ 2 = ∫ (x : EuclideanSpace ℝ (Fin d)) in Ω, partialD i φ x ^ 2

The squared L²(Ω) norm of a partial-derivative class is the integral of the squared partial over Ω.

theorem EllipticPdes.Sobolev.integral_grad_norm_sq_eq {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {φ : EuclideanSpace ℝ (Fin d) → ℝ} (h : IsTestFn Ω φ) : ∫ (x : EuclideanSpace ℝ (Fin d)), ‖fderiv ℝ φ x‖ ^ 2 = ∑ i : Fin d, ‖h.partialCls i‖ ^ 2

The L²(ℝᵈ) gradient energy of a test function decomposes into the sum of its partial-derivative class norms: ∫ ‖∇φ‖² = ∑ᵢ ‖[∂ᵢφ]‖². Combines the Riesz identity norm_sq_clm_eq_sum_apply_single with the fact that each partial is supported in Ω.

theorem EllipticPdes.Sobolev.mod_sq {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩm : MeasurableSet Ω) {φ : EuclideanSpace ℝ (Fin d) → ℝ} (h : IsTestFn Ω φ) (hvec : EuclideanSpace ℝ (Fin d)) : ‖(MeasureTheory.transL2 hvec) ((MeasureTheory.lpExtendByZero MeasureTheory.volume 2 Ω hΩm) h.testCls) - (MeasureTheory.lpExtendByZero MeasureTheory.volume 2 Ω hΩm) h.testCls‖ ^ 2 ≤ ‖hvec‖ ^ 2 * ∑ i : Fin d, ‖h.partialCls i‖ ^ 2

Per-test-function translation modulus (squared). Through the extension by zero, the squared L²(ℝᵈ) translation increment of a test class is controlled by ‖hvec‖² times the sum of its partial-derivative class norms. This is integral_sq_sub_translation_le transported to the extended class.

theorem EllipticPdes.Sobolev.trans_mod {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩm : MeasurableSet Ω) (U : ↥(H01 Ω)) (hvec : EuclideanSpace ℝ (Fin d)) : ‖(MeasureTheory.transL2 hvec) ((MeasureTheory.lpExtendByZero MeasureTheory.volume 2 Ω hΩm) ((embL2 Ω) U)) - (MeasureTheory.lpExtendByZero MeasureTheory.volume 2 Ω hΩm) ((embL2 Ω) U)‖ ≤ ‖U‖ * ‖hvec‖

Translation modulus of an H₀¹ element. For U ∈ H₀¹(Ω), the extension by zero of embL2 Ω U = U 0 is Lipschitz under translation with modulus ‖U‖. The bound comes from the smooth approximants of U (density of test graphs) through transL2_sub_le_of_tendsto'.

theorem EllipticPdes.Sobolev.embL2_norm_le {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (U : ↥(H01 Ω)) : ‖(embL2 Ω) U‖ ≤ ‖U‖

The embedding embL2 Ω is a contraction: ‖U 0‖ ≤ ‖U‖.

theorem EllipticPdes.Sobolev.embL2_isCompact {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩm : MeasurableSet Ω) (hΩb : Bornology.IsBounded Ω) : IsCompactOperator ⇑(embL2 Ω)

Rellich-Kondrachov compact embedding. For bounded measurable Ω, the embedding embL2 Ω : H₀¹(Ω) →L[ℝ] L²(Ω) is a compact operator. This discharges the single analytic hypothesis of the Fredholm theory in Compactness.lean and Spectrum.lean.

Fredholm and spectral theorems with the Rellich hypothesis discharged

With embL2_isCompact proved, the analytic hypothesis IsCompactOperator (embL2 Ω) threaded through Compactness.lean and Spectrum.lean is no longer assumed: every headline theorem holds for a bounded measurable domain outright.

theorem EllipticPdes.Sobolev.FullEllipticOp.fredholm_alternative_of_bounded {d : ℕ} (Op : FullEllipticOp d) (Ω : Set (EuclideanSpace ℝ (Fin d))) (hΩm : MeasurableSet Ω) (hΩb : Bornology.IsBounded Ω) : (∃ (u : ↥(H01 Ω)), u ≠ 0 ∧ ∀ (v : ↥(H01 Ω)), ((Op.fullBilin Ω) u) v = 0) ∨ ∀ (f : ↥(H01 Ω) →L[ℝ] ℝ), ∃! u : ↥(H01 Ω), ∀ (v : ↥(H01 Ω)), ((Op.fullBilin Ω) u) v = f v

The Fredholm alternative for a bounded measurable domain, with no compactness hypothesis.

theorem EllipticPdes.Sobolev.FullEllipticOp.fredholm_unique_imp_exists_of_bounded {d : ℕ} (Op : FullEllipticOp d) (Ω : Set (EuclideanSpace ℝ (Fin d))) (hΩm : MeasurableSet Ω) (hΩb : Bornology.IsBounded Ω) (huniq : ∀ (u : ↥(H01 Ω)), (∀ (v : ↥(H01 Ω)), ((Op.fullBilin Ω) u) v = 0) → u = 0) (f : ↥(H01 Ω) →L[ℝ] ℝ) : ∃! u : ↥(H01 Ω), ∀ (v : ↥(H01 Ω)), ((Op.fullBilin Ω) u) v = f v

The Fredholm uniqueness-implies-existence corollary for a bounded measurable domain.

Terminal result of the library, the companion of fredholm_alternative_of_bounded. Nothing else consumes it.

theorem EllipticPdes.Sobolev.dirichlet_spectral_of_bounded {d : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin d))) (hΩm : MeasurableSet Ω) (hΩb : Bornology.IsBounded Ω) (CP : ℝ) (hCP : 0 ≤ CP) (hbase : ∀ {φ : EuclideanSpace ℝ (Fin d) → ℝ} (h : IsTestFn Ω φ), ‖h.testGraph.ofLp 0‖ ^ 2 ≤ CP * ∑ i : Fin d, ‖h.testGraph.ofLp i.succ‖ ^ 2) : (⨆ (μ : ℝ), Module.End.eigenspace (↑(solOp (laplaceBilin Ω) ⋯)) μ)ᗮ = ⊥

Spectral theorem for the Dirichlet Laplacian on a bounded measurable domain, with the Rellich compact embedding discharged.

theorem EllipticPdes.Sobolev.symmetric_fullElliptic_spectral_of_bounded {d : ℕ} (Op : FullEllipticOp d) (Ω : Set (EuclideanSpace ℝ (Fin d))) (hΩm : MeasurableSet Ω) (hΩb : Bornology.IsBounded Ω) (hb : ∀ (i : Fin d), ∀ᵐ (x : EuclideanSpace ℝ (Fin d)) ∂MeasureTheory.volume.restrict Ω, Op.b x i = 0) (hc : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)) ∂MeasureTheory.volume.restrict Ω, 0 ≤ Op.c x) (hAsymm : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)) ∂MeasureTheory.volume.restrict Ω, ∀ (i j : Fin d), Op.a x i j = Op.a x j i) (CP : ℝ) (hCP : 0 ≤ CP) (hbase : ∀ {φ : EuclideanSpace ℝ (Fin d) → ℝ} (h : IsTestFn Ω φ), ‖h.testGraph.ofLp 0‖ ^ 2 ≤ CP * ∑ i : Fin d, ‖h.testGraph.ofLp i.succ‖ ^ 2) : (⨆ (μ : ℝ), Module.End.eigenspace (↑(solOp (Op.fullBilin Ω) ⋯)) μ)ᗮ = ⊥

Spectral theorem for the general symmetric divergence-form operator on a bounded measurable domain, with the Rellich compact embedding discharged.

Terminal result of the library. Nothing else consumes it.