/-
Copyright (c) 2026 Michael R. Douglas. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.

# Jentzsch's Theorem and Kernel Positivity

This file states Jentzsch's theorem (proved in JentzschProof.lean), axiomatizes
kernel positivity facts about the transfer operator, and derives the
Perron-Frobenius properties needed for the P(Φ)₂ construction.

## Theorem: Jentzsch's theorem (Reed-Simon IV, XIII.43–44)

For a compact, self-adjoint, positivity-improving operator T on L² with
eigenbasis indexed by a type with ≥ 2 elements:
- The spectral radius r is a simple eigenvalue with strictly positive value.
- All other eigenvalues λ satisfy |λ| < r.

Proved in `JentzschProof.lean` via the variational absolute value trick.

**Important**: Jentzsch does NOT imply all eigenvalues are positive.
Counterexample: [[1,2],[2,1]] is positivity-improving with eigenvalues 3,-1.

## Axiom 2: Transfer operator positivity-improving

The kernel T(ψ,ψ') = w(ψ)·G(ψ-ψ')·w(ψ') > 0 is strictly positive.

## Axiom 3: Gaussian kernel is strictly positive definite

⟨f, Tf⟩ > 0 for nonzero f, since the Gaussian kernel exp(-½‖·‖²) has
strictly positive Fourier transform (Bochner), and w > 0 preserves this.

## Axiom 4: L²(ℝ^Ns) Hilbert basis nontriviality

Any Hilbert basis of L²(ℝ^Ns) has at least 2 elements.

## Derived theorems

From Jentzsch + axioms 2-4 we derive:
- `transferOperator_inner_nonneg`: ⟨f, Tf⟩ ≥ 0
- `transferOperator_eigenvalues_pos`: all λᵢ > 0
- `transferOperator_ground_simple`: unique leading eigenvalue with strict gap
- `transferOperator_ground_simple_spectral`: packaged spectral data

## References

- Reed-Simon IV, Theorems XIII.43–44
- Simon, *The P(φ)₂ Euclidean QFT*, §III.2
- Glimm-Jaffe, *Quantum Physics*, §6.1
-/

import Pphi2.TransferMatrix.L2Operator
import Pphi2.TransferMatrix.JentzschProof
import Pphi2.TransferMatrix.GaussianFourier

noncomputable section

open MeasureTheory

/-! ## Jentzsch's theorem (proved in JentzschProof.lean) -/

/-- **Jentzsch's theorem** for compact self-adjoint positivity-improving
operators on L²(ℝ^n).

Given a nontrivial eigenbasis (|ι| ≥ 2), there exists a distinguished index
i₀ (ground) such that:
(a) λ(i₀) > 0 (the leading eigenvalue is strictly positive).
(b) λ(i₀) is simple: it is the unique index with this eigenvalue.
(c) |λ(i)| < λ(i₀) for all i ≠ i₀ (strict spectral gap).

Proved in `JentzschProof.lean` via the variational absolute value trick.
The bridge from `IsPositivityImproving` (ae) to `IsPositivityImproving'` (Lp lattice)
is `IsPositivityImproving.toPI'`.

**References**: Reed-Simon IV, Theorems XIII.43–44. -/
theorem jentzsch_theorem {n : ℕ}
    (T : Lp ℝ 2 (volume : Measure (Fin n → ℝ)) →L[ℝ]
      Lp ℝ 2 (volume : Measure (Fin n → ℝ)))
    (hT_compact : IsCompactOperator T)
    (hT_sa : IsSelfAdjoint T)
    (hT_pi : IsPositivityImproving T) :
    ∀ {ι : Type}
      (b : HilbertBasis ι ℝ (Lp ℝ 2 (volume : Measure (Fin n → ℝ))))
      (eigenval : ι → ℝ)
      (_h_eigen : ∀ i,
        (T : Lp ℝ 2 (volume : Measure (Fin n → ℝ)) →ₗ[ℝ]
          Lp ℝ 2 (volume : Measure (Fin n → ℝ))) (b i) = eigenval i • b i)
      (_h_sum : ∀ x, 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_theorem_proved T hT_compact hT_sa hT_pi.toPI'

namespace Pphi2

variable (Ns : ℕ) [NeZero Ns]

/-! ## Axiom 2: Transfer operator is positivity-improving -/

/-- The transfer operator is positivity-improving.

The kernel `T(ψ,ψ') = exp(-(a/2)h(ψ)) · exp(-½‖ψ-ψ'‖²) · exp(-(a/2)h(ψ')) > 0`
is strictly positive for all ψ, ψ'. For f ≥ 0, f ≠ 0, the set
S = {ψ' : f(ψ') > 0} has positive measure, so
(Tf)(ψ) = ∫ T(ψ,ψ') f(ψ') dψ' ≥ ∫_S T(ψ,ψ') f(ψ') dψ' > 0.

**Proof**: Uses the factorization T = M_w ∘ Conv_G ∘ M_w where w > 0 (exp) and G > 0 (exp).
Multiplication by w > 0 preserves nonneg/nonzero. Convolution with the strictly positive
Gaussian kernel maps nonneg nonzero functions to ae strictly positive functions (by
`integral_pos_iff_support_of_nonneg_ae` and translation invariance of Lebesgue measure).
Final multiplication by w > 0 preserves ae strict positivity. -/
theorem transferOperator_positivityImproving (P : InteractionPolynomial) (a mass : ℝ)
    (ha : 0 < a) (hmass : 0 < mass) :
    IsPositivityImproving (transferOperatorCLM Ns P a mass ha hmass) := by
  intro f hf_nonneg hf_nonzero
  -- Abbreviations for the building blocks
  set w := transferWeight Ns P a mass
  set G := transferGaussian Ns
  set hw_meas := transferWeight_measurable Ns P a mass
  set C := (transferWeight_bound Ns P a mass ha hmass).choose
  set hC := (transferWeight_bound Ns P a mass ha hmass).choose_spec.1
  set hw_bound := (transferWeight_bound Ns P a mass ha hmass).choose_spec.2
  set hG := transferGaussian_memLp Ns
  -- Key positivity facts
  have hw_pos : ∀ ψ, 0 < w ψ := transferWeight_pos Ns P a mass
  have hG_pos : ∀ ψ, 0 < G ψ := transferGaussian_pos Ns
  -- T f = M_w (Conv_G (M_w f))
  -- Step 1: g := M_w f satisfies g ≥ 0 ae, g ≢ 0 ae
  set g := mulCLM w hw_meas C hC hw_bound f with hg_def
  have hg_spec := mulCLM_spec w hw_meas C hC hw_bound f
  have hg_nonneg : ∀ᵐ x ∂(volume : Measure (SpatialField Ns)), 0 ≤ (g : SpatialField Ns → ℝ) x := by
    filter_upwards [hg_spec, hf_nonneg] with x hx hfx
    rw [hx]; exact mul_nonneg (le_of_lt (hw_pos x)) hfx
  have hg_nonzero : ¬ (g : SpatialField Ns → ℝ) =ᵐ[volume] 0 := by
    intro h_absurd
    apply hf_nonzero
    -- g =ᵐ 0 and g =ᵐ w * f, so w * f =ᵐ 0, so f =ᵐ 0 (since w > 0)
    have h_wf_zero : (fun x => w x * (f : SpatialField Ns → ℝ) x) =ᵐ[volume] 0 := by
      filter_upwards [h_absurd, hg_spec] with x hx1 hx2
      rwa [← hx2]
    filter_upwards [h_wf_zero] with x hx
    exact (mul_eq_zero.mp hx).resolve_left (ne_of_gt (hw_pos x))
  -- Step 2: h := Conv_G g satisfies h > 0 ae
  set h := convCLM G hG g with hh_def
  have hh_spec := convCLM_spec G hG g
  -- The convolution ∫ G(t) · g(x-t) dt is > 0 because G > 0 and g ≥ 0 ae, g ≢ 0 ae
  have hh_pos : ∀ᵐ x ∂(volume : Measure (SpatialField Ns)),
      0 < (h : SpatialField Ns → ℝ) x := by
    -- Use convCLM_spec: ↑↑h =ᵐ realConv vol G ⇑g
    -- Then show realConv vol G ⇑g x = ∫ G(t) * ⇑g(x-t) dt > 0 for all x
    -- by integral_pos_iff_support_of_nonneg_ae
    filter_upwards [hh_spec] with x hx
    rw [hx]
    -- Goal: 0 < realConv volume G ⇑g x = ∫ G(t) * ⇑g(x-t) dt
    -- Helper: the map t ↦ x - t preserves Lebesgue measure (neg + left translation)
    have h_mp : MeasurePreserving (fun t : SpatialField Ns => x - t) volume volume :=
      (measurePreserving_add_left volume x).comp (Measure.measurePreserving_neg volume)
    -- Step 2a: the integrand t ↦ G(t) * ⇑g(x-t) is nonneg ae
    have h_integrand_nonneg : ∀ᵐ t ∂(volume : Measure (SpatialField Ns)),
        0 ≤ G t * (g : SpatialField Ns → ℝ) (x - t) := by
      have h_trans : ∀ᵐ t ∂volume, 0 ≤ (g : SpatialField Ns → ℝ) (x - t) := by
        rw [ae_iff] at hg_nonneg ⊢
        -- volume {t | ¬0 ≤ g(x-t)} = volume (f⁻¹'S) ≤ volume S = 0
        exact le_antisymm (hg_nonneg ▸ h_mp.measure_preimage_le _) (zero_le)
      filter_upwards [h_trans] with t ht
      exact mul_nonneg (le_of_lt (hG_pos t)) ht
    -- Step 2b: the integrand is integrable (L² × L² → L¹ by Cauchy-Schwarz)
    have h_integrand_int : Integrable (fun t => G t * (g : SpatialField Ns → ℝ) (x - t))
        (volume : Measure (SpatialField Ns)) := by
      -- Both G and g(x-·) are in L², use integrable_inner from L2Space
      have hG2 : MemLp G 2 volume := transferGaussian_memLp_two Ns
      have hgx : MemLp ((↑↑g : SpatialField Ns → ℝ) ∘ (x - ·)) 2 volume :=
        (Lp.memLp g).comp_measurePreserving h_mp
      set G' := hG2.toLp G
      set gx' := hgx.toLp _
      refine (L2.integrable_inner (𝕜 := ℝ) G' gx').congr ?_
      filter_upwards [hG2.coeFn_toLp, hgx.coeFn_toLp] with t hGt hgxt
      -- Goal: ⟪G'(t), gx'(t)⟫_ℝ = G t * g(x-t)
      -- For ℝ: inner unfolds via star/re to plain multiplication
      simp only [inner, Inner.inner, starRingEnd_apply, star_trivial, RCLike.re_to_real]
      simp only [Function.comp_apply] at hgxt
      rw [hGt, hgxt, mul_comm]
    -- Step 2c: the support of the integrand has positive measure
    have h_support_pos : 0 < (volume : Measure (SpatialField Ns))
        (Function.support (fun t => G t * (g : SpatialField Ns → ℝ) (x - t))) := by
      -- Support of G*g(x-·) ⊇ (x-·)⁻¹'(support g), both have same measure
      have h_subset : (fun t => x - t) ⁻¹'
            (Function.support (g : SpatialField Ns → ℝ)) ⊆
          Function.support (fun t => G t * (g : SpatialField Ns → ℝ) (x - t)) := by
        intro t ht
        simp only [Function.mem_support, Set.mem_preimage] at ht ⊢
        exact mul_ne_zero (ne_of_gt (hG_pos t)) ht
      have h_g_support : 0 < volume (Function.support (g : SpatialField Ns → ℝ)) := by
        rw [pos_iff_ne_zero]
        intro h_eq
        exact hg_nonzero (ae_iff.mpr h_eq)
      calc volume (Function.support fun t => G t * (g : SpatialField Ns → ℝ) (x - t))
          ≥ volume ((fun t => x - t) ⁻¹'
              Function.support (g : SpatialField Ns → ℝ)) :=
            measure_mono h_subset
        _ = volume (Function.support (g : SpatialField Ns → ℝ)) :=
            h_mp.measure_preimage
              (measurableSet_support
                (Lp.stronglyMeasurable g).measurable).nullMeasurableSet
        _ > 0 := h_g_support
    -- Combine using integral_pos_iff_support_of_nonneg_ae
    rw [show realConv volume G (⇑g) x =
        ∫ t, G t * (g : SpatialField Ns → ℝ) (x - t) ∂volume from by
      simp [realConv, convolution, ContinuousLinearMap.lsmul_apply]]
    exact (integral_pos_iff_support_of_nonneg_ae h_integrand_nonneg h_integrand_int).mpr
      h_support_pos
  -- Step 3: T f = M_w h, and M_w maps ae positive to ae positive
  -- transferOperatorCLM f = mulCLM w ... (convCLM G ... (mulCLM w ... f)) = mulCLM w ... h
  have hTf_coercion : (transferOperatorCLM Ns P a mass ha hmass f : SpatialField Ns → ℝ) =
      (mulCLM w hw_meas C hC hw_bound h : SpatialField Ns → ℝ) :=
    congr_arg (fun e : L2SpatialField Ns => (e : SpatialField Ns → ℝ))
      (show transferOperatorCLM Ns P a mass ha hmass f =
        mulCLM w hw_meas C hC hw_bound h from rfl)
  have hresult_spec := mulCLM_spec w hw_meas C hC hw_bound h
  simp only [hTf_coercion]
  filter_upwards [hresult_spec, hh_pos] with x hx hhx
  rw [hx]; exact mul_pos (hw_pos x) hhx

/-! ## Axiom 3: Gaussian convolution is strictly positive definite

The Gaussian kernel G(x) = exp(-½‖x‖²) has Fourier transform
Ĝ(k) = (2π)^{n/2} exp(-½‖k‖²) > 0 everywhere. By Bochner's theorem and
Plancherel, convolution by G is strictly positive definite on L²:

  ⟨f, Conv_G f⟩ = ∫ |f̂(k)|² Ĝ(k) dk > 0  for f ≠ 0.

This is the bridge axiom from the [bochner](https://github.com/mrdouglasny/bochner)
formalization project. -/

/-- Convolution with the Gaussian kernel is strictly positive definite on L².

**Proof**: Factored through the square-root Gaussian H(x) = exp(-‖x‖²):
  ⟨f, Conv_G f⟩ = C · ‖Conv_H f‖²
where C > 0 (from the Gaussian convolution identity G = C⁻¹ · H⋆H),
and Conv_H is injective (since Ĥ > 0 everywhere). See `GaussianFourier.lean`. -/
theorem convolution_gaussian_strictly_positive_definite :
    ∀ (g : L2SpatialField Ns), g ≠ 0 →
      0 < @inner ℝ _ _ g (convCLM (transferGaussian Ns) (transferGaussian_memLp Ns) g) :=
  gaussian_conv_strictlyPD Ns

/-! ## Derived: Transfer operator strictly positive definite

From the factorization T = M_w ∘ Conv_G ∘ M_w with M_w self-adjoint:
  ⟨f, Tf⟩ = ⟨M_w f, Conv_G(M_w f)⟩ > 0
since w > 0 makes M_w injective (f ≠ 0 → M_w f ≠ 0) and Conv_G is
strictly PD by the axiom above. -/

/-- The transfer operator is strictly positive definite: ⟨f, Tf⟩ > 0 for
all nonzero f ∈ L².

**Proof**: Uses self-adjointness of M_w to rewrite
⟨f, M_w(Conv_G(M_w f))⟩ = ⟨M_w f, Conv_G(M_w f)⟩,
injectivity of M_w (from w > 0) to show M_w f ≠ 0,
and the Gaussian convolution strict PD axiom. -/
theorem transferOperator_strictly_positive_definite (P : InteractionPolynomial) (a mass : ℝ)
    (ha : 0 < a) (hmass : 0 < mass) :
    ∀ (f : L2SpatialField Ns), f ≠ 0 →
      0 < @inner ℝ _ _ f (transferOperatorCLM Ns P a mass ha hmass f) := by
  intro f hf
  -- Abbreviations for the building blocks
  set w := transferWeight Ns P a mass
  set G := transferGaussian Ns
  set hw_meas := transferWeight_measurable Ns P a mass
  set C := (transferWeight_bound Ns P a mass ha hmass).choose
  set hC := (transferWeight_bound Ns P a mass ha hmass).choose_spec.1
  set hw_bound := (transferWeight_bound Ns P a mass ha hmass).choose_spec.2
  set hG := transferGaussian_memLp Ns
  set A := mulCLM w hw_meas C hC hw_bound
  set B := convCLM G hG
  -- Self-adjointness of M_w
  have hA_sa : IsSelfAdjoint A := mulCLM_isSelfAdjoint w hw_meas C hC hw_bound
  -- Step 1: ⟨f, Tf⟩ = ⟨f, A(B(Af))⟩ = ⟨Af, B(Af)⟩
  have hT_eq : transferOperatorCLM Ns P a mass ha hmass f = A (B (A f)) := rfl
  rw [hT_eq, show @inner ℝ _ _ f (A (B (A f))) = @inner ℝ _ _ (A f) (B (A f))
    from (hA_sa.isSymmetric f (B (A f))).symm]
  -- Step 2: M_w f ≠ 0 (since w > 0 and f ≠ 0)
  have hw_pos : ∀ ψ, 0 < w ψ := transferWeight_pos Ns P a mass
  have hAf_ne : A f ≠ 0 := by
    intro h_absurd
    apply hf
    -- A f = 0 in L² means w * f = 0 a.e., and w > 0, so f = 0 a.e.
    have hAf_spec := mulCLM_spec w hw_meas C hC hw_bound f
    have hAf_zero : (A f : SpatialField Ns → ℝ) =ᵐ[volume] 0 := by
      rw [h_absurd]; exact Lp.coeFn_zero _ _ _
    have hf_ae_zero : (f : SpatialField Ns → ℝ) =ᵐ[volume] 0 := by
      filter_upwards [hAf_spec, hAf_zero] with x hx1 hx2
      have : w x * (f : SpatialField Ns → ℝ) x = 0 := by rwa [← hx1]
      exact (mul_eq_zero.mp this).resolve_left (ne_of_gt (hw_pos x))
    exact Lp.eq_zero_iff_ae_eq_zero.mpr hf_ae_zero
  -- Step 3: Apply Gaussian convolution strict PD
  exact convolution_gaussian_strictly_positive_definite Ns (A f) hAf_ne

/-! ## L²(ℝ^Ns) Hilbert basis nontriviality

L²(ℝ^Ns, Lebesgue) is infinite-dimensional (it contains orthogonal indicator
functions of disjoint sets), so any Hilbert basis has at least 2 elements. -/

/-- Any Hilbert basis of L²(ℝ^Ns) has at least 2 elements.

**Proof**: Construct two orthogonal nonzero elements using indicator functions
of disjoint balls, then use the Hilbert basis expansion to derive that ι
must have ≥ 2 elements. -/
theorem l2SpatialField_hilbertBasis_nontrivial
    {ι : Type} (b : HilbertBasis ι ℝ (L2SpatialField Ns)) :
    ∃ j k : ι, j ≠ k := by
  classical
  -- Construct two disjoint balls with positive finite Lebesgue measure
  let μ : Measure (Fin Ns → ℝ) := volume
  let A := Metric.ball (0 : Fin Ns → ℝ) 1
  let B := Metric.ball (fun _ : Fin Ns => (4 : ℝ)) 1
  have hA_meas : MeasurableSet A := measurableSet_ball
  have hB_meas : MeasurableSet B := measurableSet_ball
  have hA_fin : μ A ≠ ⊤ := measure_ball_ne_top
  have hB_fin : μ B ≠ ⊤ := measure_ball_ne_top
  have hA_pos : μ A ≠ 0 := ne_of_gt (Metric.measure_ball_pos μ 0 one_pos)
  have hB_pos : μ B ≠ 0 := ne_of_gt (Metric.measure_ball_pos μ _ one_pos)
  -- Balls are disjoint via triangle inequality
  have hAB : Disjoint A B := Set.disjoint_left.mpr fun x hxA hxB => by
    have h1 : dist x 0 < 1 := Metric.mem_ball.mp hxA
    have h2 : dist x (fun _ => (4:ℝ)) < 1 := Metric.mem_ball.mp hxB
    have htri : dist (0 : Fin Ns → ℝ) (fun _ => (4:ℝ)) < 2 :=
      calc dist 0 (fun _ => (4:ℝ))
          ≤ dist (0 : Fin Ns → ℝ) x + dist x (fun _ => 4) := dist_triangle _ _ _
        _ = dist x 0 + dist x (fun _ => 4) := by rw [dist_comm]
        _ < 1 + 1 := add_lt_add h1 h2
        _ = 2 := by ring
    have hge : (4 : ℝ) ≤ dist (0 : Fin Ns → ℝ) (fun _ => (4:ℝ)) := by
      have i₀ : Fin Ns := ⟨0, Fin.pos'⟩
      have h1 : dist (0 : ℝ) 4 = 4 := by norm_num
      have h2 : dist ((0 : Fin Ns → ℝ) i₀) ((fun _ => (4:ℝ)) i₀)
          = dist (0 : ℝ) 4 := by simp
      have h3 : dist ((0 : Fin Ns → ℝ) i₀) ((fun _ => (4:ℝ)) i₀)
          ≤ dist (0 : Fin Ns → ℝ) (fun _ => (4:ℝ)) := by
        exact dist_le_pi_dist (0 : Fin Ns → ℝ) (fun _ => (4:ℝ)) i₀
      linarith
    linarith
  -- Construct indicator functions in L²
  let f₁ := indicatorConstLp (E := ℝ) 2 hA_meas hA_fin 1
  let f₂ := indicatorConstLp (E := ℝ) 2 hB_meas hB_fin 1
  -- They are nonzero (norm > 0)
  have hf₁_ne : f₁ ≠ 0 := by
    intro h; have h1 := congr_arg (‖·‖) h
    simp only [norm_zero] at h1
    rw [show f₁ = indicatorConstLp 2 hA_meas hA_fin (1:ℝ) from rfl,
      norm_indicatorConstLp (by norm_num) (by norm_num),
      norm_one, one_mul] at h1
    have : (0 : ℝ) < μ.real A := ENNReal.toReal_pos hA_pos hA_fin
    linarith [Real.rpow_pos_of_pos this (1 / (2:ENNReal).toReal)]
  have hf₂_ne : f₂ ≠ 0 := by
    intro h; have h1 := congr_arg (‖·‖) h
    simp only [norm_zero] at h1
    rw [show f₂ = indicatorConstLp 2 hB_meas hB_fin (1:ℝ) from rfl,
      norm_indicatorConstLp (by norm_num) (by norm_num),
      norm_one, one_mul] at h1
    have : (0 : ℝ) < μ.real B := ENNReal.toReal_pos hB_pos hB_fin
    linarith [Real.rpow_pos_of_pos this (1 / (2:ENNReal).toReal)]
  -- They are orthogonal (disjoint supports)
  have h_orth : @inner ℝ _ _ f₁ f₂ = 0 := by
    change @inner ℝ _ _ (indicatorConstLp 2 hA_meas hA_fin (1:ℝ))
      (indicatorConstLp 2 hB_meas hB_fin (1:ℝ)) = 0
    rw [MeasureTheory.L2.inner_indicatorConstLp_indicatorConstLp]
    simp [hAB.inter_eq]
  -- By contradiction: assume ι has < 2 elements
  by_contra h_not
  push Not at h_not
  -- h_not : ∀ j k : ι, j = k (ι is subsingleton)
  by_cases hι : IsEmpty ι
  · -- ι empty: b.repr maps to ℓ²(∅) = {0}, so f₁ = 0
    exact hf₁_ne (b.repr.injective (by ext i; exact hι.elim i))
  · -- ι has exactly one element j₀
    rw [not_isEmpty_iff] at hι
    obtain ⟨j₀⟩ := hι
    -- Every vector is a scalar multiple of b j₀
    have h_span : ∀ v : L2SpatialField Ns,
        v = @inner ℝ _ _ (b j₀) v • b j₀ := by
      intro v
      have h_expand := b.hasSum_repr v
      have h_repr_eq : ∀ i, b.repr v i = @inner ℝ _ _ (b i) v :=
        fun i => b.repr_apply_apply v i
      simp_rw [h_repr_eq] at h_expand
      have heq : (fun i => @inner ℝ _ _ (b i) v • b i) =
          (fun _ => @inner ℝ _ _ (b j₀) v • b j₀) :=
        funext fun i => by rw [h_not i j₀]
      rw [heq] at h_expand
      have h_ite : HasSum (fun i => if i = j₀
          then @inner ℝ _ _ (b j₀) v • (b j₀ : L2SpatialField Ns)
          else 0) (@inner ℝ _ _ (b j₀) v • (b j₀ : L2SpatialField Ns)) := by
        convert hasSum_ite_eq j₀ (@inner ℝ _ _ (b j₀) v • (b j₀ : L2SpatialField Ns))
      have h_same : (fun _ : ι => @inner ℝ _ _ (b j₀) v • (b j₀ : L2SpatialField Ns))
          = (fun i => if i = j₀
            then @inner ℝ _ _ (b j₀) v • (b j₀ : L2SpatialField Ns)
            else 0) :=
        funext fun i => by simp [h_not i j₀]
      rw [h_same] at h_expand
      exact h_expand.unique h_ite
    -- inner f₁ f₂ = c₁ * c₂
    have h1 := h_span f₁
    have h2 := h_span f₂
    rw [h1, h2] at h_orth
    simp only [inner_smul_left, inner_smul_right,
      real_inner_self_eq_norm_sq, b.orthonormal.norm_eq_one j₀,
      one_pow, mul_one] at h_orth
    rcases mul_eq_zero.mp h_orth with hc | hc
    · exact hf₂_ne (by rw [h2, hc, zero_smul])
    · rw [starRingEnd_apply, star_trivial] at hc
      exact hf₁_ne (by rw [h1, hc, zero_smul])

/-! ## Derived theorems

We now derive the Perron-Frobenius properties of the transfer
operator from the axioms above. These have the same signatures as the
former axioms in L2Operator.lean, ensuring downstream compatibility. -/

/-- ⟨f, Tf⟩ ≥ 0 for all f. Immediate from strict PD (which gives > 0 for f ≠ 0,
and ⟨0, T0⟩ = 0 for f = 0). -/
theorem transferOperator_inner_nonneg (P : InteractionPolynomial) (a mass : ℝ)
    (ha : 0 < a) (hmass : 0 < mass) :
    ∀ (f : L2SpatialField Ns),
      0 ≤ @inner ℝ _ _ f (transferOperatorCLM Ns P a mass ha hmass f) := by
  intro f
  by_cases hf : f = 0
  · rw [hf, map_zero, inner_self_eq_zero.mpr rfl]
  · exact le_of_lt (transferOperator_strictly_positive_definite Ns P a mass ha hmass f hf)

/-- All eigenvalues of the transfer operator are strictly positive.

Proof: ⟨bᵢ, T(bᵢ)⟩ = λᵢ · ‖bᵢ‖² = λᵢ > 0 by strict positive definiteness,
since bᵢ ≠ 0 (it has norm 1). -/
theorem transferOperator_eigenvalues_pos (P : InteractionPolynomial) (a mass : ℝ)
    (ha : 0 < a) (hmass : 0 < mass)
    {ι : Type} (b : HilbertBasis ι ℝ (L2SpatialField Ns)) (eigenval : ι → ℝ)
    (h_eigen : ∀ i, (transferOperatorCLM Ns P a mass ha hmass :
        L2SpatialField Ns →ₗ[ℝ] L2SpatialField Ns) (b i) = eigenval i • b i)
    (i : ι) : 0 < eigenval i := by
  -- bᵢ ≠ 0 since ‖bᵢ‖ = 1
  have hbi_ne : (b i : L2SpatialField Ns) ≠ 0 := by
    intro h
    have := b.orthonormal.norm_eq_one i
    rw [h, norm_zero] at this
    exact one_ne_zero this.symm
  -- ⟨bᵢ, Tbᵢ⟩ > 0 by strict PD
  have hpd := transferOperator_strictly_positive_definite Ns P a mass ha hmass (b i) hbi_ne
  -- Rewrite ⟨bᵢ, Tbᵢ⟩ = λᵢ · ‖bᵢ‖² = λᵢ
  have h_eigen_i := h_eigen i
  have hconv : (transferOperatorCLM Ns P a mass ha hmass :
    L2SpatialField Ns →ₗ[ℝ] L2SpatialField Ns) (b i) =
    transferOperatorCLM Ns P a mass ha hmass (b i) := rfl
  rw [← hconv, h_eigen_i] at hpd
  rw [@inner_smul_right ℝ, @real_inner_self_eq_norm_sq] at hpd
  have hnorm : ‖b i‖ = 1 := b.orthonormal.norm_eq_one i
  rw [hnorm, one_pow, mul_one] at hpd
  exact hpd

/-- Ground-state simplicity and existence of first excited level.

Derived from Jentzsch (which gives i₀ with spectral gap) combined with
nontriviality (to pick some i₁ ≠ i₀) and eigenvalue positivity
(to convert |λᵢ| < λ₀ to λᵢ < λ₀). -/
theorem transferOperator_ground_simple (P : InteractionPolynomial) (a mass : ℝ)
    (ha : 0 < a) (hmass : 0 < mass) :
    ∀ {ι : Type} (b : HilbertBasis ι ℝ (L2SpatialField Ns)) (eigenval : ι → ℝ)
      (_h_eigen : ∀ i, (transferOperatorCLM Ns P a mass ha hmass :
          L2SpatialField Ns →ₗ[ℝ] L2SpatialField Ns) (b i) = eigenval i • b i)
      (_h_sum : ∀ x, HasSum (fun i => (eigenval i * @inner ℝ _ _ (b i) x) • b i)
          (transferOperatorCLM Ns P a mass ha hmass x)),
      ∃ i₀ i₁ : ι, i₁ ≠ i₀ ∧ eigenval i₁ < eigenval i₀ := by
  intro ι b eigenval h_eigen h_sum
  -- Nontriviality: L²(ℝ^Ns) is infinite-dimensional
  have h_nt := l2SpatialField_hilbertBasis_nontrivial Ns b
  -- Jentzsch gives i₀ with positivity, simplicity, and spectral gap
  obtain ⟨i₀, hpos, _hsimple, hgap⟩ := jentzsch_theorem
    (transferOperatorCLM Ns P a mass ha hmass)
    (transferOperator_isCompact Ns P a mass ha hmass)
    (transferOperator_isSelfAdjoint Ns P a mass ha hmass)
    (transferOperator_positivityImproving Ns P a mass ha hmass)
    b eigenval h_eigen h_sum h_nt
  -- Pick any i₁ ≠ i₀ from nontriviality
  obtain ⟨j, k, hjk⟩ := h_nt
  have h_exists_ne : ∃ i₁, i₁ ≠ i₀ := by
    by_cases hj : j = i₀
    · exact ⟨k, fun hk => hjk (hj.trans hk.symm)⟩
    · exact ⟨j, hj⟩
  obtain ⟨i₁, hi₁_ne⟩ := h_exists_ne
  -- All eigenvalues positive, so |λᵢ| = λᵢ → gap gives λ(i₁) < λ(i₀)
  have hall_pos : ∀ i, 0 < eigenval i :=
    fun i => transferOperator_eigenvalues_pos Ns P a mass ha hmass b eigenval h_eigen i
  have hlt : eigenval i₁ < eigenval i₀ := by
    have := hgap i₁ hi₁_ne
    rwa [abs_of_pos (hall_pos i₁)] at this
  exact ⟨i₀, i₁, hi₁_ne, hlt⟩

/-- Spectral data with distinguished ground and first excited levels. -/
theorem transferOperator_ground_simple_spectral (P : InteractionPolynomial) (a mass : ℝ)
    (ha : 0 < a) (hmass : 0 < mass) :
    ∃ (ι : Type) (b : HilbertBasis ι ℝ (L2SpatialField Ns)) (eigenval : ι → ℝ)
      (i₀ i₁ : ι),
      (∀ i, (transferOperatorCLM Ns P a mass ha hmass :
          L2SpatialField Ns →ₗ[ℝ] L2SpatialField Ns) (b i) = eigenval i • b i) ∧
      (∀ x, HasSum (fun i => (eigenval i * @inner ℝ _ _ (b i) x) • b i)
          (transferOperatorCLM Ns P a mass ha hmass x)) ∧
      i₁ ≠ i₀ ∧ eigenval i₁ < eigenval i₀ := by
  rcases transferOperator_spectral Ns P a mass ha hmass with ⟨ι, b, eigenval, h_eigen, h_sum⟩
  rcases transferOperator_ground_simple Ns P a mass ha hmass b eigenval h_eigen h_sum
    with ⟨i₀, i₁, hi_ne, hlt⟩
  exact ⟨ι, b, eigenval, i₀, i₁, h_eigen, h_sum, hi_ne, hlt⟩

end Pphi2

end
