The Fredholm alternative for the Dirichlet problem

Let B be the bounded coercive energy form of a divergence-form operator on H¹₀(Ω). Shifting its mass coefficient by a constant -κ changes the weak equation to

B(u, v) - κ ⟪u, v⟫_{L²} = ⟪f, v⟫_{L²}.

When Ω is bounded, Rellich--Kondrachov makes the value inclusion H¹₀(Ω) → L²(Ω) compact. The abstract variational Fredholm alternative therefore gives the classical dichotomy: either the homogeneous shifted problem has a nonzero solution, or every L² forcing has a unique weak solution. The homogeneous solution space is always finite dimensional.

This is the compact-resolvent step of Lane D.18 of TauCetiRoadmap/PDE/README.md. The unshifted form B can itself contain bounded measurable principal, drift, and mass coefficients; only the additional perturbation is the scalar mass shift. This is the standard reduction of a Gårding form to a coercive form by adding a sufficiently large constant.

Main declarations

• TauCeti.PDE.dirichletMassOperator: the operator representing the L² mass form relative to the coercive energy form; TauCeti.PDE.isCompactOperator_dirichletMassOperator proves it compact on bounded domains.
• TauCeti.PDE.IsWeakSolutionDirichletMassShift: the weak equation with scalar mass shift.
• TauCeti.PDE.finiteDimensional_ker_one_sub_smul_dirichletMassOperator: finite dimensionality of its homogeneous solution space.
• TauCeti.PDE.fredholmAlternative_isWeakSolutionDirichlet_sub_const: the Fredholm dichotomy for the operator with mass coefficient c - κ.

References

Lane D, item 18 of TauCetiRoadmap/PDE/README.md; L. C. Evans, Partial Differential Equations, Section 6.2.3; D. Gilbarg and N. Trudinger, Elliptic Partial Differential Equations of Second Order, Chapter 8, Theorem 8.3.

@[instance_reducible]

noncomputable def TauCeti.PDE.instNormedAddCommGroupH1ZeroFredholm {ι : Type u_1} [Fintype ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)} : NormedAddCommGroup ↥(W1p0 mu Omega 2)

Shortcut normed group instance on H¹₀(Ω), needed by the inherited Hilbert structure.

Equations

• TauCeti.PDE.instNormedAddCommGroupH1ZeroFredholm = inferInstance

@[instance_reducible]

noncomputable def TauCeti.PDE.instInnerProductSpaceH1ZeroFredholm {ι : Type u_1} [Fintype ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)} : InnerProductSpace ℝ ↥(W1p0 mu Omega 2)

Shortcut inner-product instance on H¹₀(Ω).

Equations

• TauCeti.PDE.instInnerProductSpaceH1ZeroFredholm = inferInstance

noncomputable def TauCeti.PDE.dirichletMassOperator {ι : Type u_1} [Fintype ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)} {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ} {b : EuclideanSpace ℝ ι → EuclideanSpace ℝ ι} {c : EuclideanSpace ℝ ι → ℝ} (hcoeff : MeasureTheory.MemLp (fun (x : EuclideanSpace ℝ ι) => energyIntegrand (a x) (b x) (c x)) ⊤ (mu.restrict ↑Omega)) (hcoercive : IsCoercive (energyFormH1L0 hcoeff)) : ↥(W1p0 mu Omega 2) →L[ℝ] ↥(W1p0 mu Omega 2)

The Lax--Milgram operator representing the L² mass form on H¹₀(Ω). It is characterized by TauCeti.PDE.energyFormH1_dirichletMassOperator.

Equations

• TauCeti.PDE.dirichletMassOperator hcoeff hcoercive = hcoercive.formPerturbationOperator TauCeti.W1p0.valueL

@[simp]

theorem TauCeti.PDE.energyFormH1_dirichletMassOperator {ι : Type u_1} [Fintype ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)} {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ} {b : EuclideanSpace ℝ ι → EuclideanSpace ℝ ι} {c : EuclideanSpace ℝ ι → ℝ} (hcoeff : MeasureTheory.MemLp (fun (x : EuclideanSpace ℝ ι) => energyIntegrand (a x) (b x) (c x)) ⊤ (mu.restrict ↑Omega)) (hcoercive : IsCoercive (energyFormH1L0 hcoeff)) (u v : ↥(W1p0 mu Omega 2)) : energyFormH1 a b c ↑((dirichletMassOperator hcoeff hcoercive) u) ↑v = inner ℝ (W1p.value ↑u) (W1p.value ↑v)

The Dirichlet mass operator represents the L² inner product relative to the base energy form.

theorem TauCeti.PDE.isCompactOperator_dirichletMassOperator {ι : Type u_1} [Fintype ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)} {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ} {b : EuclideanSpace ℝ ι → EuclideanSpace ℝ ι} {c : EuclideanSpace ℝ ι → ℝ} (hcoeff : MeasureTheory.MemLp (fun (x : EuclideanSpace ℝ ι) => energyIntegrand (a x) (b x) (c x)) ⊤ (mu.restrict ↑Omega)) (hcoercive : IsCoercive (energyFormH1L0 hcoeff)) (hOmega : Bornology.IsBounded ↑Omega) : IsCompactOperator ⇑(dirichletMassOperator hcoeff hcoercive)

On a bounded domain, the Dirichlet mass operator is compact by Rellich--Kondrachov.

def TauCeti.PDE.IsWeakSolutionDirichletMassShift {ι : Type u_1} [Fintype ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)} (a : EuclideanSpace ℝ ι → Matrix ι ι ℝ) (b : EuclideanSpace ℝ ι → EuclideanSpace ℝ ι) (c : EuclideanSpace ℝ ι → ℝ) (kappa : ℝ) (f : ↥(MeasureTheory.Lp ℝ 2 (mu.restrict ↑Omega))) (u : ↥(W1p0 mu Omega 2)) : Prop

The weak Dirichlet equation obtained by shifting the base operator's mass coefficient by the constant -κ. It says B(u,v) - κ⟪u,v⟫_{L²} = ⟪f,v⟫_{L²} for every v ∈ H¹₀(Ω).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.PDE.isWeakSolutionDirichletMassShift_iff {ι : Type u_1} [Fintype ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)} {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ} {b : EuclideanSpace ℝ ι → EuclideanSpace ℝ ι} {c : EuclideanSpace ℝ ι → ℝ} (kappa : ℝ) (f : ↥(MeasureTheory.Lp ℝ 2 (mu.restrict ↑Omega))) (u : ↥(W1p0 mu Omega 2)) : IsWeakSolutionDirichletMassShift a b c kappa f u ↔ ∀ (v : ↥(W1p0 mu Omega 2)), energyFormH1 a b c ↑u ↑v - kappa * inner ℝ (W1p.value ↑u) (W1p.value ↑v) = ∫ (x : EuclideanSpace ℝ ι) in ↑Omega, ↑↑f x * ↑↑(W1p.value ↑v) x ∂mu

Being a mass-shifted weak solution, written out as the integral identity B(u, v) - κ⟪u, v⟫_{L²} = ∫_Ω f v.

theorem TauCeti.PDE.isWeakSolutionDirichletMassShift_zero_iff {ι : Type u_1} [Fintype ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)} {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ} {b : EuclideanSpace ℝ ι → EuclideanSpace ℝ ι} {c : EuclideanSpace ℝ ι → ℝ} (f : ↥(MeasureTheory.Lp ℝ 2 (mu.restrict ↑Omega))) (u : ↥(W1p0 mu Omega 2)) : IsWeakSolutionDirichletMassShift a b c 0 f u ↔ IsWeakSolutionDirichlet a b c f u

A zero mass shift recovers the unshifted Dirichlet weak equation.

This named specialization is not a simp lemma because isWeakSolutionDirichletMassShift_iff already reduces its left-hand side; registering both lemmas would violate the simpNF linter.

theorem TauCeti.PDE.isWeakSolutionDirichletMassShift_iff_isWeakSolutionDirichlet_sub_const {ι : Type u_1} [Fintype ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)} {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ} {b : EuclideanSpace ℝ ι → EuclideanSpace ℝ ι} {c : EuclideanSpace ℝ ι → ℝ} (hcoeff : MeasureTheory.MemLp (fun (x : EuclideanSpace ℝ ι) => energyIntegrand (a x) (b x) (c x)) ⊤ (mu.restrict ↑Omega)) (kappa : ℝ) (f : ↥(MeasureTheory.Lp ℝ 2 (mu.restrict ↑Omega))) (u : ↥(W1p0 mu Omega 2)) : IsWeakSolutionDirichletMassShift a b c kappa f u ↔ IsWeakSolutionDirichlet a b (fun (x : EuclideanSpace ℝ ι) => c x - kappa) f u

For essentially bounded energy coefficients, the mass-shifted equation is the usual weak Dirichlet equation with mass coefficient c - κ.

theorem TauCeti.PDE.isWeakSolutionDirichletMassShift_iff_operator_eq {ι : Type u_1} [Fintype ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)} {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ} {b : EuclideanSpace ℝ ι → EuclideanSpace ℝ ι} {c : EuclideanSpace ℝ ι → ℝ} (hcoeff : MeasureTheory.MemLp (fun (x : EuclideanSpace ℝ ι) => energyIntegrand (a x) (b x) (c x)) ⊤ (mu.restrict ↑Omega)) (hcoercive : IsCoercive (energyFormH1L0 hcoeff)) (kappa : ℝ) (f : ↥(MeasureTheory.Lp ℝ 2 (mu.restrict ↑Omega))) (u : ↥(W1p0 mu Omega 2)) : IsWeakSolutionDirichletMassShift a b c kappa f u ↔ (1 - kappa • dirichletMassOperator hcoeff hcoercive) u = weakSolutionDirichlet hcoeff hcoercive f

The mass-shifted weak equation written as an operator equation on H¹₀(Ω).

theorem TauCeti.PDE.finiteDimensional_ker_one_sub_smul_dirichletMassOperator {ι : Type u_1} [Fintype ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)} {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ} {b : EuclideanSpace ℝ ι → EuclideanSpace ℝ ι} {c : EuclideanSpace ℝ ι → ℝ} (hcoeff : MeasureTheory.MemLp (fun (x : EuclideanSpace ℝ ι) => energyIntegrand (a x) (b x) (c x)) ⊤ (mu.restrict ↑Omega)) (hcoercive : IsCoercive (energyFormH1L0 hcoeff)) (hOmega : Bornology.IsBounded ↑Omega) (kappa : ℝ) : FiniteDimensional ℝ ↥(↑(1 - kappa • dirichletMassOperator hcoeff hcoercive)).ker

The homogeneous solution space of a scalar mass shift of a coercive Dirichlet form is finite dimensional on a bounded domain.

theorem TauCeti.PDE.fredholmAlternative_isWeakSolutionDirichlet_sub_const {ι : Type u_1} [Fintype ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)} {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ} {b : EuclideanSpace ℝ ι → EuclideanSpace ℝ ι} {c : EuclideanSpace ℝ ι → ℝ} (hcoeff : MeasureTheory.MemLp (fun (x : EuclideanSpace ℝ ι) => energyIntegrand (a x) (b x) (c x)) ⊤ (mu.restrict ↑Omega)) (hcoercive : IsCoercive (energyFormH1L0 hcoeff)) (hOmega : Bornology.IsBounded ↑Omega) (kappa : ℝ) : (∃ (u : ↥(W1p0 mu Omega 2)), u ≠ 0 ∧ IsWeakSolutionDirichlet a b (fun (x : EuclideanSpace ℝ ι) => c x - kappa) 0 u) ∨ ∀ (f : ↥(MeasureTheory.Lp ℝ 2 (mu.restrict ↑Omega))), ∃! u : ↥(W1p0 mu Omega 2), IsWeakSolutionDirichlet a b (fun (x : EuclideanSpace ℝ ι) => c x - kappa) f u

The Fredholm alternative for the mass-shifted Dirichlet problem. On a bounded domain, the operator with mass coefficient c - κ either has a nonzero homogeneous weak solution, or admits a unique weak solution for every L² forcing.