Documentation

LeanPool.SpectralPositivity.Operator.JentzschProof

Proof of Jentzsch's Theorem via the Variational Absolute Value Trick #

This file proves Jentzsch's theorem for compact self-adjoint positivity-improving operators on L²(ℝ^n, Lebesgue). The proof avoids the Krein-Rutman / Banach lattice cone machinery and uses only the Rayleigh quotient, Cauchy-Schwarz, and L² lattice structure (absolute value, positive/negative parts).

Proof outline (Courant-Hilbert / Barry Simon) #

  1. Phase 1: Positivity-preserving operators satisfy |Tf| ≤ T|f| a.e.
  2. Phase 2: Therefore |⟨f, Tf⟩| ≤ ⟨|f|, T|f|⟩.
  3. Phase 3: If f is a ground state (Tf = lam₀f), then |f| is also a ground state.
  4. Phase 4: By positivity-improving, the ground state is strictly positive a.e.
  5. Phase 5: Every ground state eigenvector has constant sign a.e.
  6. Phase 6: The ground state eigenvalue lam₀ is simple (multiplicity 1).
  7. Phase 7: All other eigenvalues satisfy |λ| < lam₀ (strict spectral gap).

References #

Definitions #

An operator on L²(ℝ^n) is positivity-preserving if it maps nonneg functions to nonneg functions. This is weaker than positivity-improving.

Equations
Instances For

    An operator on L²(ℝ^n) is positivity-improving if it maps nonneg nonzero functions to a.e. strictly positive functions (ae-filter version).

    Equations
    Instances For

      An operator on L²(ℝ^n) is positivity-improving if it maps nonneg nonzero functions to a.e. strictly positive functions (Lp lattice version).

      Equations
      Instances For

        Positivity-improving implies positivity-preserving. If f ≥ 0 and f ≠ 0, then Tf > 0 a.e. ≥ 0. If f = 0, then Tf = 0 ≥ 0.

        IsPositivityImproving (ae conditions) implies IsPositivityImproving' (Lp lattice). The definitions differ only in whether the hypotheses use ae-filter or Lp order/equality:

        • 0 ≤ f in Lp ↔ 0 ≤ᵐ[μ] f (by Lp.coeFn_nonneg)
        • f ≠ 0 in Lp ↔ ¬ f =ᵐ[μ] 0 (by Lp.eq_zero_iff_ae_eq_zero)

        Phase 1: Absolute value inequality #

        For a positivity-preserving operator T on L²: |Tf| ≤ T|f| a.e.

        Proof: f = f⁺ - f⁻ with f⁺, f⁻ ≥ 0. Since T is positivity-preserving, Tf⁺ ≥ 0 and Tf⁻ ≥ 0. Then: |Tf| = |Tf⁺ - Tf⁻| ≤ Tf⁺ + Tf⁻ = T(f⁺ + f⁻) = T|f|

        Phase 1: Absolute value inequality for positivity-preserving operators.

        Phase 2: Inner product inequality #

        |⟨f, Tf⟩| ≤ ⟨|f|, T|f|⟩

        Proof: |⟨f, Tf⟩| = |∫ f(x) (Tf)(x) dx| ≤ ∫ |f(x)| |Tf(x)| dx (integral triangle inequality) ≤ ∫ |f(x)| (T|f|)(x) dx (Phase 1: |Tf| ≤ T|f|, and |f| ≥ 0) = ⟨|f|, T|f|⟩ (since |f| ≥ 0 and T|f| ≥ 0)

        Phase 3: |f| is a ground state if f is #

        The Rayleigh quotient R(g) = ⟨g, Tg⟩ / ‖g‖² achieves its supremum at the ground state eigenvector. The chain of inequalities:

        lam₀ ‖f‖² = ⟨f, Tf⟩ ≤ |⟨f, Tf⟩| ≤ ⟨|f|, T|f|⟩ ≤ lam₀ ‖|f|‖²

        Since ‖|f|‖ = ‖f‖, we get equality throughout, so |f| achieves the supremum of R, hence |f| is an eigenvector for lam₀.

        theorem abs_eigenvector_of_top_eigenvector {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] (T : (MeasureTheory.Lp 2 MeasureTheory.volume) →L[] (MeasureTheory.Lp 2 MeasureTheory.volume)) (_hT_compact : IsCompactOperator T) (hT_sa : IsSelfAdjoint T) (hT_pp : IsPositivityPreserving T) (f : (MeasureTheory.Lp 2 MeasureTheory.volume)) (hf_ne : f 0) (lam₀ : ) (hlam₀ : 0 < lam₀) (hf_eigen : T f = lam₀ f) (hlam₀_top : ∀ (g : (MeasureTheory.Lp 2 MeasureTheory.volume)), inner g (T g) lam₀ * g ^ 2) :
        T |f| = lam₀ |f|

        Phase 3: If f is an eigenvector for the top eigenvalue lam₀, then |f| is also an eigenvector for lam₀.

        Phase 4: Ground state is strictly positive a.e. #

        Since |f| ≥ 0 and |f| ≠ 0, and T is positivity-improving, T|f| > 0 a.e. But T|f| = lam₀|f|, so |f| > 0 a.e.

        theorem ground_state_strictly_positive {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] (T : (MeasureTheory.Lp 2 MeasureTheory.volume) →L[] (MeasureTheory.Lp 2 MeasureTheory.volume)) (hT_pi : IsPositivityImproving' T) (e₀ : (MeasureTheory.Lp 2 MeasureTheory.volume)) (he₀_ne : e₀ 0) (he₀_nonneg : 0 e₀) (lam₀ : ) (hlam₀ : 0 < lam₀) (he₀_eigen : T e₀ = lam₀ e₀) :
        ∀ᵐ (x : Ω), 0 < e₀ x

        Phase 4: The ground state eigenvector (after taking absolute value) is strictly positive almost everywhere.

        Phase 5: Every ground state eigenvector has constant sign #

        If f is an eigenvector for lam₀, then |f| is also (Phase 3). Define h = |f| - f. Then h ≥ 0 and h is an eigenvector for lam₀. By Phase 4, either h = 0 a.e. (so f = |f| ≥ 0, hence f > 0 a.e.) or h > 0 a.e. Since h = |f| - f, having h > 0 a.e. means |f(x)| > f(x) a.e., i.e., f(x) < 0 a.e. (strictly).

        So every ground state eigenvector is either strictly positive or strictly negative a.e.

        theorem eigenvector_constant_sign {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] (T : (MeasureTheory.Lp 2 MeasureTheory.volume) →L[] (MeasureTheory.Lp 2 MeasureTheory.volume)) (hT_compact : IsCompactOperator T) (hT_sa : IsSelfAdjoint T) (hT_pi : IsPositivityImproving' T) (f : (MeasureTheory.Lp 2 MeasureTheory.volume)) (hf_ne : f 0) (lam₀ : ) (hlam₀ : 0 < lam₀) (hf_eigen : T f = lam₀ f) (hlam₀_top : ∀ (g : (MeasureTheory.Lp 2 MeasureTheory.volume)), inner g (T g) lam₀ * g ^ 2) :
        (∀ᵐ (x : Ω), 0 < f x) ∀ᵐ (x : Ω), f x < 0

        Phase 5: Every eigenvector for the top eigenvalue has constant sign.

        Phase 6: The top eigenvalue lam₀ is simple #

        If u, v are two orthogonal eigenvectors for lam₀ with ⟨u, v⟩ = 0, then by Phase 5, we may assume u > 0 a.e. and v > 0 a.e. (or multiply by -1). But then ⟨u, v⟩ = ∫ u(x)v(x) dx > 0, contradicting orthogonality.

        theorem top_eigenvalue_simple {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] [(MeasureTheory.ae MeasureTheory.volume).NeBot] (T : (MeasureTheory.Lp 2 MeasureTheory.volume) →L[] (MeasureTheory.Lp 2 MeasureTheory.volume)) (hT_compact : IsCompactOperator T) (hT_sa : IsSelfAdjoint T) (hT_pi : IsPositivityImproving' T) (lam₀ : ) (hlam₀ : 0 < lam₀) (hlam₀_top : ∀ (g : (MeasureTheory.Lp 2 MeasureTheory.volume)), inner g (T g) lam₀ * g ^ 2) (u v : (MeasureTheory.Lp 2 MeasureTheory.volume)) (hu_ne : u 0) (hv_ne : v 0) (hu_eigen : T u = lam₀ u) (hv_eigen : T v = lam₀ v) (h_orth : inner u v = 0) :

        Phase 6: The top eigenvalue has multiplicity 1 (is simple).

        Phase 7: Strict spectral gap #

        For any eigenvalue μ ≠ lam₀, we have |μ| < lam₀.

        Case 1: μ ≥ 0. Then μ < lam₀ by simplicity (if μ = lam₀, the eigenspace is 1-dimensional by Phase 6, so the eigenvector would be in the same eigenspace).

        Case 2: μ < 0. Suppose |μ| = lam₀, i.e., μ = -lam₀. Let g be an eigenvector for -lam₀. By self-adjointness, ⟨e₀, g⟩ = 0. Apply the absolute value trick: |Tg| = |-lam₀g| = lam₀|g|. Phase 1 gives |Tg| ≤ T|g|, so lam₀|g| ≤ T|g|. The Rayleigh quotient bound gives ⟨|g|, T|g|⟩ ≤ lam₀ ‖g‖². Together: T|g| = lam₀|g|, so |g| is in the lam₀-eigenspace. By simplicity (Phase 6), |g| = c·e₀ for some c > 0. So |g| > 0 a.e. Phase 5 forces g to have constant sign. But ⟨e₀, g⟩ = 0 with e₀ > 0 and |g| > 0 contradicts constant sign.

        theorem spectral_gap {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] [(MeasureTheory.ae MeasureTheory.volume).NeBot] (T : (MeasureTheory.Lp 2 MeasureTheory.volume) →L[] (MeasureTheory.Lp 2 MeasureTheory.volume)) (_hT_compact : IsCompactOperator T) (hT_sa : IsSelfAdjoint T) (hT_pi : IsPositivityImproving' T) (e₀ : (MeasureTheory.Lp 2 MeasureTheory.volume)) (_he₀_ne : e₀ 0) (lam₀ : ) (hlam₀ : 0 < lam₀) (_he₀_eigen : T e₀ = lam₀ e₀) (hlam₀_top : ∀ (g : (MeasureTheory.Lp 2 MeasureTheory.volume)), inner g (T g) lam₀ * g ^ 2) (_hlam₀_simple : ∀ (v : (MeasureTheory.Lp 2 MeasureTheory.volume)), v 0T v = lam₀ v∃ (c : ), v = c e₀) (μ : ) (hμ_ne : μ lam₀) (g : (MeasureTheory.Lp 2 MeasureTheory.volume)) (hg_ne : g 0) (hg_eigen : T g = μ g) :
        |μ| < lam₀

        Phase 7: All eigenvalues other than lam₀ satisfy |μ| < lam₀.

        Spectral decomposition of the Rayleigh quotient #

        Assembly: Jentzsch's theorem #

        Combine all phases to prove the full theorem.

        theorem exists_pos_eigenvalue {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] [(MeasureTheory.ae MeasureTheory.volume).NeBot] (T : (MeasureTheory.Lp 2 MeasureTheory.volume) →L[] (MeasureTheory.Lp 2 MeasureTheory.volume)) (hT_pi : IsPositivityImproving' T) {ι : Type} (b : HilbertBasis ι (MeasureTheory.Lp 2 MeasureTheory.volume)) (eigenval : ι) (h_norm_one : ∀ (i : ι), b i = 1) (h_sum : ∀ (x : (MeasureTheory.Lp 2 MeasureTheory.volume)), HasSum (fun (i : ι) => (eigenval i * inner (b i) x) b i) (T x)) (h_nt : ∃ (j : ι) (k : ι), j k) :
        ∃ (i : ι), 0 < eigenval i

        A positivity-improving compact self-adjoint operator has a strictly positive eigenvalue. If all eigenvalues were ≤ 0, then ⟨f, Tf⟩ ≤ 0 for every f by the spectral decomposition, contradicting ⟨|b j|, T|b j|⟩ > 0 which holds because T is positivity-improving.

        theorem jentzsch_theorem_proved {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] [(MeasureTheory.ae MeasureTheory.volume).NeBot] (T : (MeasureTheory.Lp 2 MeasureTheory.volume) →L[] (MeasureTheory.Lp 2 MeasureTheory.volume)) (hT_compact : IsCompactOperator T) (hT_sa : IsSelfAdjoint T) (hT_pi : IsPositivityImproving' T) {ι : Type} (b : HilbertBasis ι (MeasureTheory.Lp 2 MeasureTheory.volume)) (eigenval : ι) (_h_eigen : ∀ (i : ι), T (b i) = eigenval i b i) (_h_sum : ∀ (x : (MeasureTheory.Lp 2 MeasureTheory.volume)), HasSum (fun (i : ι) => (eigenval i * inner (b i) x) b i) (T x)) (_h_nt : ∃ (j : ι) (k : ι), j k) :
        ∃ (i₀ : ι), 0 < eigenval i₀ (∀ (i : ι), eigenval i = eigenval i₀i = i₀) ∀ (i : ι), i i₀|eigenval i| < eigenval i₀

        Jentzsch's theorem (proved).

        For a compact, self-adjoint, positivity-improving operator on L²(ℝ^n) with eigenbasis indexed by a type with ≥ 2 elements:

        • The top eigenvalue lam₀ > 0 is simple.
        • All other eigenvalues satisfy |λ| < lam₀.