Closed Energy Form and Form Domain #

Defines the form domain D(E_λ) and the Kato closed-form structure. Axiomatizes the Fourier representation E_λ(G) = (1/2π) ∫ ψ_λ|Ĝ|² dξ, domain characterization via weighted Fourier space, and closedness on both L²(ℝ) and L²(I).

Reference: lamportform.tex, Section 7.3, Propositions 6–7, lines 844–936.

Form domain #

source

def ConnesLean.formDomain (cutoffLambda : ℝ) :

Set (ℝ → ℂ)

The form domain D(E_λ) is the set of functions with finite energy.

A function G belongs to D(E_λ) when its energy energyForm cutoffLambda G, valued in ENNReal, is not ⊤. This is the natural domain for the quadratic form E_λ.

Equations

ConnesLean.formDomain cutoffLambda = {G : ℝ → ℂ | ConnesLean.energyForm cutoffLambda G ≠ ⊤}

Instances For

Closed form structure #

source

structure ConnesLean.IsClosedEnergyForm (cutoffLambda : ℝ) :

Prop

A Kato closed-form structure for E_λ (cf. Kato, Thm VI.1.17).

Fields:

nonneg: E_λ(G) ≥ 0 (trivial for ENNReal)
zero_energy: E_λ(0) = 0
smooth_in_domain: C_c^∞ ⊂ D(E_λ) (dense domain)
graph_complete: if (Gn) is Cauchy in the graph norm ‖G‖² + E_λ(G) and converges in L², then the limit is in D(E_λ) and E_λ(Gn − G) → 0

nonneg (G : ℝ → ℂ) : 0 ≤ energyForm cutoffLambda G
zero_energy : energyForm cutoffLambda 0 = 0
smooth_in_domain (G : ℝ → ℂ) : HasCompactSupport G → ContDiff ℝ ⊤ G → G ∈ formDomain cutoffLambda
graph_complete (Gn : ℕ → ℝ → ℂ) (G : ℝ → ℂ) : (∀ (n : ℕ), Gn n ∈ formDomain cutoffLambda) → Filter.Tendsto (fun (n : ℕ) => ∫⁻ (u : ℝ), ↑‖Gn n u - G u‖₊ ^ 2) Filter.atTop (nhds 0) → (∀ (ε : ENNReal), 0 < ε → ∃ (N : ℕ), ∀ (n m : ℕ), N ≤ n → N ≤ m → (energyForm cutoffLambda fun (u : ℝ) => Gn n u - Gn m u) < ε) → G ∈ formDomain cutoffLambda ∧ Filter.Tendsto (fun (n : ℕ) => energyForm cutoffLambda fun (u : ℝ) => Gn n u - G u) Filter.atTop (nhds 0)

Instances For

Fourier representation (Lemma 9, axiomatized) #

source

axiom ConnesLean.energyForm_eq_fourierSymbol_integral (cutoffLambda : ℝ) (hLam : 1 < cutoffLambda) (G : ℝ → ℂ) (hG : G ∈ formDomain cutoffLambda) :

(energyForm cutoffLambda G).toReal = 1 / (2 * Real.pi) * ∫ (ξ : ℝ), fourierSymbol cutoffLambda ξ * ‖FourierTransform.fourier G ξ‖ ^ 2

Fourier representation of the energy form: E_λ(G) = (1/2π) ∫ ψ_λ(ξ) |Ĝ(ξ)|² dξ.

Proof sketch (lamportform.tex, Lemma 9, lines 844–872): Write ‖G − S_t G‖² = (1/2π) ∫ 4 sin²(ξt/2) |Ĝ(ξ)|² dξ (Plancherel), substitute into the archimedean integral and prime sum, interchange integration order (Fubini), and recognize fourierSymbol.

Why axiom: Requires Plancherel theorem (not in Mathlib) and Fubini interchange for the double integral.

Soundness: Preconditions are 1 < cutoffLambda and G ∈ formDomain, matching Lemma 9's hypotheses. No structure parameters.

Domain characterization (Proposition 6, Step 2, axiomatized) #

source

axiom ConnesLean.formDomain_eq_weighted_fourier (cutoffLambda : ℝ) (hLam : 1 < cutoffLambda) (G : ℝ → ℂ) :

G ∈ formDomain cutoffLambda ↔ ∫⁻ (ξ : ℝ), ↑‖FourierTransform.fourier G ξ‖₊ ^ 2 < ⊤ ∧ ∫⁻ (ξ : ℝ), ↑(fourierSymbol cutoffLambda ξ).toNNReal * ↑‖FourierTransform.fourier G ξ‖₊ ^ 2 < ⊤

The form domain equals the weighted Fourier space: G ∈ D(E_λ) ↔ Ĝ ∈ L² ∧ ∫ ψ_λ(ξ)|Ĝ(ξ)|² dξ < ∞.

The two conditions are: (1) ∫ ‖Ĝ(ξ)‖₊² dξ < ∞ (Fourier transform in L²), and (2) ∫ ψ_λ(ξ) ‖Ĝ(ξ)‖₊² dξ < ∞ (weighted Fourier integrability). By Plancherel, condition (1) is equivalent to G ∈ L².

Why axiom: Depends on the Fourier representation axiom.

Soundness: Preconditions are 1 < cutoffLambda and a bare function G. The biconditional matches Proposition 6, Step 2. No structure parameters.

Closedness on L²(ℝ) (Proposition 6, axiomatized) #

source

axiom ConnesLean.energyForm_closed_on_line (cutoffLambda : ℝ) (hLam : 1 < cutoffLambda) :

IsClosedEnergyForm cutoffLambda

The energy form E_λ is a closed form on L²(ℝ) in the sense of Kato.

Proof sketch (lamportform.tex, Proposition 6, lines 874–907):

nonneg: trivial (ENNReal).
zero_energy: from energyForm_zero.
smooth_in_domain: for φ ∈ C_c^∞, ‖φ − S_t φ‖ ≤ |t|·‖φ'‖ (MVT), so the energy integral converges by integrability of w(t)·t².
graph_complete: the graph norm ‖G‖_E² = ‖G‖² + E_λ(G) equals (1/2π) ∫ (1 + ψ_λ(ξ)) |Ĝ(ξ)|² dξ, a weighted L² norm. Completeness of weighted L² spaces gives the result.

Why axiom: smooth_in_domain needs the MVT translation estimate plus integrability of w(t)t². graph_complete needs weighted L² completeness via Fourier isometry. Both depend on Plancherel.

Soundness: Sole precondition is 1 < cutoffLambda, matching Proposition 6. The conclusion is an IsClosedEnergyForm structure whose fields encode the four Kato closedness properties. No structure parameters.

Closedness on L²(I) (Proposition 7, axiomatized) #

source

axiom ConnesLean.energyForm_closed_on_interval (cutoffLambda : ℝ) (hLam : 1 < cutoffLambda) (Gn : ℕ → ℝ → ℂ) (G : ℝ → ℂ) :

let L := Real.log cutoffLambda; (∀ (n : ℕ), Function.support (Gn n) ⊆ Set.Icc (-L) L) → (∀ (n : ℕ), Gn n ∈ formDomain cutoffLambda) → Filter.Tendsto (fun (n : ℕ) => ∫⁻ (u : ℝ), ↑‖Gn n u - G u‖₊ ^ 2) Filter.atTop (nhds 0) → (∀ (ε : ENNReal), 0 < ε → ∃ (N : ℕ), ∀ (n m : ℕ), N ≤ n → N ≤ m → (energyForm cutoffLambda fun (u : ℝ) => Gn n u - Gn m u) < ε) → Function.support G ⊆ Set.Icc (-L) L ∧ G ∈ formDomain cutoffLambda

The energy form E_λ is closed on L²(I) where I = [−log λ, log λ].

If (Gn) are supported in I = Icc(−L, L), Cauchy in graph norm, and converge in L² to G, then G is supported in I and belongs to D(E_λ).

Proof sketch (lamportform.tex, Proposition 7, lines 909–936): The subspace H_I = {φ ∈ L²(ℝ) : supp(φ) ⊆ Icc(−L,L)} is closed in L²(ℝ). Since Gn → G in L² with each Gn supported in I, the limit G is supported in I. Proposition 6 (closedness on ℝ) gives G ∈ D(E_λ).

Why axiom: Needs H_I closed in L²(ℝ) + Proposition 6. Standard but requires ~80 lines of L² machinery.

Soundness: Preconditions are 1 < cutoffLambda plus support, domain membership, L² convergence, and energy-Cauchy conditions on the sequence — matching Proposition 7's hypotheses. No structure parameters.