Rellich-Kondrachov reduction from the compact embedding to a compact opK

The Fredholm alternative of Fredholm.lean is conditioned on the abstract hypothesis IsCompactOperator (opK). This file traces that hypothesis to its single analytic source: the Rellich-Kondrachov compact embedding H₀¹(Ω) ↪ L²(Ω), encoded as the coordinate-0 map embL2 Ω : H₀¹(Ω) →L[ℝ] L²(Ω).

• embL2 Ω: the embedding U ↦ U 0, the composition of the submodule inclusion with the PiLp projection onto coordinate 0.
• opT_eq_adjoint_comp: the L² form operator factors as opT = (embL2)† ∘ embL2, because ⟪opT U, V⟫ = ⟪U₀, V₀⟫_{L²} = ⟪embL2 U, embL2 V⟫.
• opT_isCompact / opK_isCompact: given IsCompactOperator (embL2 Ω), both opT and opK = γ·opE⁻¹·opT are compact, by composing the compact embedding with bounded operators.
• fredholm_alternative_rellich / fredholm_unique_imp_exists_rellich: the Fredholm theorems re-stated to take the single hypothesis IsCompactOperator (embL2 Ω) in place of the opaque operator-level IsCompactOperator (opK). The compact embedding for bounded Ω is the one analytic input (Rellich-Kondrachov), threaded as a hypothesis exactly as the Poincaré geometry input was, and deliberately not discharged here.

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

The coordinate-0 embedding H₀¹(Ω) ↪ L²(Ω), U ↦ U 0, as a continuous linear map: the PiLp projection onto coordinate 0 precomposed with the submodule inclusion.

Equations

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

@[simp]

theorem EllipticPdes.Sobolev.embL2_apply {d : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin d))) (U : ↥(H01 Ω)) : (embL2 Ω) U = (↑U).ofLp 0

Simp lemma: embL2 Ω U = (U : H1amb Ω) 0, the function coordinate of U.

theorem EllipticPdes.Sobolev.opT_eq_adjoint_comp {d : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin d))) : FullEllipticOp.opT Ω = ContinuousLinearMap.adjoint (embL2 Ω) ∘SL embL2 Ω

Factorisation of the L² form through the embedding: opT = (embL2)† ∘ embL2. Indeed ⟪opT U, V⟫ = ⟪U₀, V₀⟫_{L²} = ⟪embL2 U, embL2 V⟫ = ⟪(embL2)† (embL2 U), V⟫.

theorem EllipticPdes.Sobolev.opT_isCompact {d : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin d))) (hRellich : IsCompactOperator ⇑(embL2 Ω)) : IsCompactOperator ⇑(FullEllipticOp.opT Ω)

Given the Rellich compact embedding, the L² form operator opT is compact: it is the compact embL2 postcomposed with the bounded (embL2)†.

theorem EllipticPdes.Sobolev.FullEllipticOp.opK_isCompact {d : ℕ} (Op : FullEllipticOp d) (Ω : Set (EuclideanSpace ℝ (Fin d))) (hRellich : IsCompactOperator ⇑(embL2 Ω)) : IsCompactOperator ⇑(Op.opK Ω)

Given the Rellich compact embedding, the reduction operator opK = γ·opE⁻¹·opT is compact: opT is compact and opK postcomposes it with the bounded opE⁻¹ and scales it.

theorem EllipticPdes.Sobolev.FullEllipticOp.fredholm_alternative_rellich {d : ℕ} (Op : FullEllipticOp d) (Ω : Set (EuclideanSpace ℝ (Fin d))) (hRellich : IsCompactOperator ⇑(embL2 Ω)) : (∃ (u : ↥(H01 Ω)), u ≠ 0 ∧ ∀ (v : ↥(H01 Ω)), ((Op.fullBilin Ω) u) v = 0) ∨ ∀ (f : ↥(H01 Ω) →L[ℝ] ℝ), ∃! u : ↥(H01 Ω), ∀ (v : ↥(H01 Ω)), ((Op.fullBilin Ω) u) v = f v

Fredholm alternative on the Rellich embedding hypothesis (Evans §6.2.3, Theorem 4). Identical to fredholm_alternative, but conditioned on the single analytic input IsCompactOperator (embL2 Ω) (the Rellich-Kondrachov compact embedding for bounded Ω) rather than the opaque IsCompactOperator (opK): either Lu = 0 has a nontrivial weak solution, or Lu = f has a unique weak solution for every f.

theorem EllipticPdes.Sobolev.FullEllipticOp.fredholm_unique_imp_exists_rellich {d : ℕ} (Op : FullEllipticOp d) (Ω : Set (EuclideanSpace ℝ (Fin d))) (hRellich : IsCompactOperator ⇑(embL2 Ω)) (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

Fredholm corollary on the Rellich embedding hypothesis: if the homogeneous problem Lu = 0 has only the trivial weak solution, then Lu = f has a unique weak solution for every f, assuming the Rellich-Kondrachov compact embedding.