Compact Resolvent for the Kato Operator A_λ

The closed energy form E_λ gives rise to a self-adjoint operator A_λ ≥ 0 via the Kato representation theorem. Proves A_λ has compact resolvent by combining the Kato structure with the compact embedding D(E_λ) ↪ L²(I).

Reference: lamportform.tex, Theorem 9 (lines 1159–1209).

Kato operator structure

structure ConnesLean.KatoOperator (cutoffLambda : ℝ) : Type

Structure modeling the resolvent (A_λ + I)⁻¹ of a self-adjoint operator associated to the energy form E_λ via the Kato representation theorem.

The three fields capture:

1. The resolvent maps L² into the form domain D(E_λ)
2. The resolvent preserves compact support in I = [−log λ, log λ]
3. The form identity: ‖(A+I)⁻¹f‖² + E_λ((A+I)⁻¹f) ≤ ‖f‖²

Reference: Kato, Perturbation Theory, Theorem VI.2.1.

• resolvent : (ℝ → ℂ) → ℝ → ℂ
• resolvent_maps_to_domain (f : ℝ → ℂ) : self.resolvent f ∈ formDomain cutoffLambda
• resolvent_supported (f : ℝ → ℂ) : Function.support f ⊆ Set.Icc (-Real.log cutoffLambda) (Real.log cutoffLambda) → Function.support (self.resolvent f) ⊆ Set.Icc (-Real.log cutoffLambda) (Real.log cutoffLambda)
• form_identity (f : ℝ → ℂ) : (∫⁻ (u : ℝ), ↑‖self.resolvent f u‖₊ ^ 2) + energyForm cutoffLambda (self.resolvent f) ≤ ∫⁻ (u : ℝ), ↑‖f u‖₊ ^ 2

Kato representation theorem (axiomatized)

axiom ConnesLean.kato_operator (cutoffLambda : ℝ) (hLam : 1 < cutoffLambda) : KatoOperator cutoffLambda

The Kato representation theorem: every closed, densely defined, nonnegative symmetric form on a Hilbert space determines a unique self-adjoint operator. Applied to E_λ, this gives the operator A_λ ≥ 0 whose resolvent satisfies the form identity.

Why axiom: The Kato representation theorem (Kato, Theorem VI.2.1) is deep functional analysis that is not available in Mathlib. The theorem requires:

• E_λ is a closed form (Stage 5C: energyForm_closed_on_line)
• E_λ is densely defined (follows from C_c^∞ ⊂ D(E_λ))
• E_λ is nonneg (by construction as sum of L² norms)

Soundness: Sole precondition is 1 < cutoffLambda. The conclusion is a KatoOperator structure whose fields (a resolvent operator with domain/support control and the form identity) are substantive — it cannot be trivially constructed.

Reference: lamportform.tex, Theorem 9, Step 1 (lines 1164–1174).

Compact resolvent predicate

def ConnesLean.HasCompactResolvent (cutoffLambda : ℝ) (T : KatoOperator cutoffLambda) : Prop

Sequential characterization of compact resolvent: the resolvent (A_λ + I)⁻¹ maps bounded L² sequences (supported in I) to sequences with L²-convergent subsequences.

This is equivalent to saying the resolvent is a compact operator on L²(I), which in turn means A_λ has purely discrete spectrum with eigenvalues accumulating only at +∞.

Reference: lamportform.tex, Theorem 9, Step 3 (lines 1192–1209).

Equations

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

Proved theorems

theorem ConnesLean.resolvent_mem_formNormBall (cutoffLambda : ℝ) (T : KatoOperator cutoffLambda) (f : ℝ → ℂ) (hsupp : Function.support f ⊆ Set.Icc (-Real.log cutoffLambda) (Real.log cutoffLambda)) {C : ENNReal} (hbdd : ∫⁻ (u : ℝ), ↑‖f u‖₊ ^ 2 ≤ C) : T.resolvent f ∈ formNormBall cutoffLambda C

The resolvent maps bounded, compactly supported L² functions into the form-norm ball. This is the key link between the Kato operator and the compact embedding: the form identity gives the graph-norm bound needed to land in formNormBall.

Reference: lamportform.tex, Theorem 9, Steps 2.3–2.4 (lines 1183–1191).

theorem ConnesLean.compact_resolvent_of_compact_embedding (cutoffLambda : ℝ) (hLam : 1 < cutoffLambda) : HasCompactResolvent cutoffLambda (kato_operator cutoffLambda hLam)

Main theorem (Theorem 9): The operator A_λ has compact resolvent.

The proof chains the Kato form identity with the compact embedding:

1. Each resolvent image lands in the form-norm ball (by resolvent_mem_formNormBall)
2. The form-norm ball is relatively compact in L² (by formNormBall_isRelativelyCompactL2)
3. Therefore the resolvent sequence has a convergent subsequence

Reference: lamportform.tex, Theorem 9, Step 3 (lines 1192–1209).

theorem ConnesLean.kato_resolvent_in_formDomain (cutoffLambda : ℝ) (hLam : 1 < cutoffLambda) (f : ℝ → ℂ) : (kato_operator cutoffLambda hLam).resolvent f ∈ formDomain cutoffLambda

Convenience wrapper: the Kato resolvent maps any function into the form domain.