Fredholm alternative for the elliptic Dirichlet problem

Evans §6.2.3, Theorem 4.

For the full divergence-form operator Lu = -Dⱼ(aᵢⱼDᵢu) + bᵢDᵢu + cu the Gårding inequality makes the shifted form B_γ = B + γ⟨·,·⟩_{L²} coercive (shiftedBilin_coercive), so L + γ is invertible by Lax-Milgram. Writing the solution operator of L + γ and the L² form as bounded operators on H₀¹(Ω) reduces the weak problem Lu = f to a compact-operator equation (1 - K)u = h, to which Mathlib's Fredholm alternative for compact operators (IsCompactOperator.hasEigenvalue_or_mem_resolventSet) applies at the eigenvalue 1.

The reduction is exact:

• opA / opT: the Riesz representatives of the full form B and of the L² form ⟨u₀, v₀⟩ as bounded operators on H₀¹(Ω) (InnerProductSpace.continuousLinearMapOfBilin), with ⟪opA u, v⟫ = B[u,v] and ⟪opT u, v⟫ = ⟨u₀, v₀⟩.
• opE: the coercive Lax-Milgram equivalence of B_γ (for γ = gardingγ), so opA = opE - γ·opT (opA_eq) and hence opA = opE ∘ (1 - opK) (opA_factor) with opK = γ·opE⁻¹·opT.
• fredholm_alternative: assuming opK is a compact operator (the Rellich-Kondrachov input, that the embedding H₀¹(Ω) ↪ L²(Ω) is compact, exactly as the box geometry was the external input for coercivity): either Lu = 0 has a nontrivial weak solution, or Lu = f has a unique weak solution for every f. fredholm_unique_imp_exists is the usual corollary: uniqueness for the homogeneous problem forces solvability of the inhomogeneous one.

Riesz representatives of the forms as bounded operators on H₀¹(Ω)

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

The Riesz representative of the full divergence form B as an operator on H₀¹(Ω): ⟪opA u, v⟫ = B[u, v].

Equations

• Op.opA Ω = InnerProductSpace.continuousLinearMapOfBilin (Op.fullBilin Ω)

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

The Riesz representative of the L² form ⟨u₀, v₀⟩ as an operator on H₀¹(Ω).

Equations

• EllipticPdes.Sobolev.FullEllipticOp.opT Ω = InnerProductSpace.continuousLinearMapOfBilin (EllipticPdes.Sobolev.FullEllipticOp.zerothForm Ω)

noncomputable def EllipticPdes.Sobolev.FullEllipticOp.opE {d : ℕ} (Op : FullEllipticOp d) (Ω : Set (EuclideanSpace ℝ (Fin d))) : ↥(H01 Ω) ≃L[ℝ] ↥(H01 Ω)

The coercive Lax-Milgram equivalence of the shifted form B_γ, γ = gardingγ.

Equations

• Op.opE Ω = ⋯.continuousLinearEquivOfBilin

theorem EllipticPdes.Sobolev.FullEllipticOp.inner_opA {d : ℕ} (Op : FullEllipticOp d) (Ω : Set (EuclideanSpace ℝ (Fin d))) (u v : ↥(H01 Ω)) : inner ℝ ((Op.opA Ω) u) v = ((Op.fullBilin Ω) u) v

Riesz identity: ⟪Op.opA Ω u, v⟫ = Op.fullBilin Ω u v.

theorem EllipticPdes.Sobolev.FullEllipticOp.inner_opT {d : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin d))) (u v : ↥(H01 Ω)) : inner ℝ ((opT Ω) u) v = ((zerothForm Ω) u) v

Riesz identity: ⟪opT Ω u, v⟫ = zerothForm Ω u v = ⟨u₀, v₀⟩_{L²}.

theorem EllipticPdes.Sobolev.FullEllipticOp.inner_opE {d : ℕ} (Op : FullEllipticOp d) (Ω : Set (EuclideanSpace ℝ (Fin d))) (u v : ↥(H01 Ω)) : inner ℝ ((Op.opE Ω) u) v = ((Op.shiftedBilin Ω Op.gardingγ) u) v

Riesz identity: ⟪Op.opE Ω u, v⟫ = Op.shiftedBilin Ω Op.gardingγ u v.

Reduction to 1 - opK

theorem EllipticPdes.Sobolev.FullEllipticOp.opA_eq {d : ℕ} (Op : FullEllipticOp d) (Ω : Set (EuclideanSpace ℝ (Fin d))) : Op.opA Ω = ↑(Op.opE Ω) - Op.gardingγ • opT Ω

opA = opE - γ·opT: subtracting the shift recovers the unshifted form.

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

The compact part of the reduction: opK = γ·opE⁻¹·opT.

Equations

• Op.opK Ω = Op.gardingγ • ↑(Op.opE Ω).symm ∘SL EllipticPdes.Sobolev.FullEllipticOp.opT Ω

theorem EllipticPdes.Sobolev.FullEllipticOp.opA_factor {d : ℕ} (Op : FullEllipticOp d) (Ω : Set (EuclideanSpace ℝ (Fin d))) : Op.opA Ω = ↑(Op.opE Ω) ∘SL (1 - Op.opK Ω)

opA = opE ∘ (1 - opK): the weak problem Lu = f becomes (1 - opK)u = opE⁻¹(opA⁻¹…).

Fredholm alternative

theorem EllipticPdes.Sobolev.FullEllipticOp.fredholm_alternative {d : ℕ} (Op : FullEllipticOp d) (Ω : Set (EuclideanSpace ℝ (Fin d))) (hK : IsCompactOperator ⇑(Op.opK Ω)) : (∃ (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 for the elliptic Dirichlet problem (Evans §6.2.3, Theorem 4). Assume the operator opK is compact: the Rellich-Kondrachov input, that H₀¹(Ω) ↪ L²(Ω) is a compact embedding. Then exactly one of two alternatives holds: either the homogeneous problem Lu = 0 has a nontrivial weak solution u ≠ 0 (∀ v, B[u, v] = 0), or the inhomogeneous problem Lu = f has a unique weak solution for every continuous functional f.

theorem EllipticPdes.Sobolev.FullEllipticOp.fredholm_unique_imp_exists {d : ℕ} (Op : FullEllipticOp d) (Ω : Set (EuclideanSpace ℝ (Fin d))) (hK : IsCompactOperator ⇑(Op.opK Ω)) (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 (the usual working form, Evans §6.2.3): if the homogeneous problem Lu = 0 has only the trivial weak solution, then Lu = f has a unique weak solution for every f. Uniqueness of the homogeneous problem rules out the eigenvalue alternative.