Documentation

TauCeti.Analysis.InnerProductSpace.Variational.Fredholm

The Fredholm alternative for compact perturbations of coercive forms #

Let B be a bounded coercive bilinear form on a real Hilbert space V, and let J : V → H be a continuous linear map to another real Hilbert space. Lax--Milgram turns the quadratic form

(u, v) ↦ ⟪J u, J v⟫

into an operator K : V → V, characterized by B (K u) v = ⟪J u, J v⟫. When J is compact, so is K. Mathlib's Fredholm alternative for compact operators can therefore be applied to 1 - κK: either the homogeneous compactly perturbed variational problem has a nonzero solution, or every represented forcing has a unique solution. Its kernel is finite dimensional in either case.

This is the abstract functional-analytic assembly used by Lane D.18 of the PDE roadmap. In that application V = H¹₀(Ω), H = L²(Ω), and J is the compact Rellich inclusion.

Main declarations #

The construction consumes Mathlib's IsCompactOperator.hasEigenvalue_or_mem_resolventSet and the Riesz--Schauder kernel theorem IsCompactOperator.finiteDimensional_ker_one_sub.

References #

L. C. Evans, Partial Differential Equations, Section 6.2.3; J. B. Conway, A Course in Functional Analysis, Chapter VI, Section 5.

source
noncomputable def IsCoercive.formPerturbationOperator {V : Type u_1} {H : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) (J : V →L[ℝ] H) :
V →L[ℝ] V

The operator representing the form (u, v) ↦ ⟪J u, J v⟫ relative to a coercive form B. It is characterized by IsCoercive.apply_formPerturbationOperator without unfolding.

Equations
Instances For
    source
    theorem IsCoercive.formPerturbationOperator_apply {V : Type u_1} {H : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) (J : V →L[ℝ] H) (u : V) :
    (hB.formPerturbationOperator J) u = hB.solutionOfInner ((ContinuousLinearMap.adjoint J) (J u))

    The form perturbation operator is the inverse Lax--Milgram operator applied to J†J.

    source
    @[simp]
    theorem IsCoercive.apply_formPerturbationOperator {V : Type u_1} {H : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) (J : V →L[ℝ] H) (u v : V) :
    (B ((hB.formPerturbationOperator J) u)) v = inner ℝ (J u) (J v)

    Characterization of the form perturbation operator by its variational equation.

    source
    theorem IsCoercive.isCompactOperator_formPerturbationOperator {V : Type u_1} {H : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) {J : V →L[ℝ] H} (hJ : IsCompactOperator ⇑J) :
    IsCompactOperator ⇑(hB.formPerturbationOperator J)

    If the continuous linear map J is compact, so is the operator representing its inner-product form.

    source
    theorem IsCoercive.one_sub_smul_formPerturbationOperator_apply_eq_iff {V : Type u_1} {H : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) (J : V →L[ℝ] H) (kappa : ℝ) (F u : V) :
    (1 - kappa • hB.formPerturbationOperator J) u = hB.solutionOfInner F ↔ ∀ (v : V), (B u) v - kappa * inner ℝ (J u) (J v) = inner ℝ F v

    The compactly perturbed operator equation is equivalent to its variational formulation.

    source
    theorem IsCoercive.one_sub_smul_formPerturbationOperator_apply_eq_iff_functional {V : Type u_1} {H : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) (J : V →L[ℝ] H) (kappa : ℝ) (ell : StrongDual ℝ V) (u : V) :
    (1 - kappa • hB.formPerturbationOperator J) u = hB.solutionOfFunctional ell ↔ ∀ (v : V), (B u) v - kappa * inner ℝ (J u) (J v) = ell v

    The compactly perturbed operator equation with an arbitrary continuous functional is equivalent to its variational formulation.

    source
    theorem IsCoercive.finiteDimensional_ker_one_sub_smul_formPerturbationOperator {V : Type u_1} {H : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) {J : V →L[ℝ] H} (hJ : IsCompactOperator ⇑J) (kappa : ℝ) :
    FiniteDimensional ℝ ↥(↑(1 - kappa • hB.formPerturbationOperator J)).ker

    The homogeneous solution space of a compactly perturbed coercive variational problem is finite dimensional.

    source
    theorem IsCoercive.fredholmAlternative_formPerturbation {V : Type u_1} {H : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) {J : V →L[ℝ] H} (hJ : IsCompactOperator ⇑J) (kappa : ℝ) :
    (∃ (u : V), u ≠ 0 ∧ ∀ (v : V), (B u) v - kappa * inner ℝ (J u) (J v) = 0) ∨ ∀ (ell : StrongDual ℝ V), ∃! u : V, ∀ (v : V), (B u) v - kappa * inner ℝ (J u) (J v) = ell v

    The variational Fredholm alternative. For a compact continuous linear map J, either the homogeneous perturbation of B by κ ⟪J ·, J ·⟫ has a nonzero solution, or every represented forcing has a unique solution.