Energy Form E_λ(G) — Definition 3.1

Assembles the difference-energy form from archimedean and prime contributions: E_λ(G) = ∫₀^{2L} w(t) ‖G̃ - S_t G̃‖² dt + Σ_p Σ_m (log p) p^{-m/2} ‖G̃ - S_{m log p} G̃‖²

Key properties: E_λ(G) ≥ 0, c_p(λ) ≤ 0 for each prime, E_λ(0) = 0.

Reference: lamportform.tex, Definition 3.1, lines 435–470.

The energy form

def ConnesLean.energyForm (cutoffLambda : ℝ) (G : ℝ → ℂ) : ENNReal

The difference-energy form E_λ(G) from Definition 3.1 of lamportform.tex.

For G : ℝ → ℂ and cutoff parameter cutoffLambda > 1 with L = log cutoffLambda: E_λ(G) = ∫₀^{2L} w(t) ‖G̃ - S_t G̃‖² dt + Σ_{p prime, p ≤ λ²} Σ_{m=1}^{M_p} (log p) p^{-m/2} ‖G̃ - S_{m log p} G̃‖²

The first term is the archimedean energy integral; the second is the sum of prime energy terms over all relevant primes and exponents.

Valued in ENNReal since each summand is a weighted L² norm (nonneg by construction).

Reference: lamportform.tex, lines 438–443.

Equations

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

The total correction constant

def ConnesLean.totalCorrection (cutoffLambda : ℝ) : ℝ

The total correction constant C_λ = Σ_p c_p(λ) + c_∞(λ).

This collects the ‖G‖² terms from both the prime and archimedean energy decompositions. Note that c_p(λ) ≤ 0 for each prime p, so the sign of C_λ is not controlled in general.

Reference: lamportform.tex, lines 446–452 (remark after Definition 3.1).

Equations

• ConnesLean.totalCorrection cutoffLambda = ∑ p ∈ ConnesLean.primeFinset cutoffLambda, ConnesLean.primeConstant p cutoffLambda + ConnesLean.archConstant cutoffLambda

Basic properties

theorem ConnesLean.energyForm_nonneg (cutoffLambda : ℝ) (G : ℝ → ℂ) : 0 ≤ energyForm cutoffLambda G

The energy form is nonneg: E_λ(G) ≥ 0. Trivial since ENNReal is nonneg by definition.

theorem ConnesLean.totalCorrection_prime_nonpos {cutoffLambda : ℝ} (hLam : 1 < cutoffLambda) : ∑ p ∈ primeFinset cutoffLambda, primeConstant p cutoffLambda ≤ 0

Each prime correction term is nonpositive: c_p(λ) ≤ 0. This follows from primeConstant_nonpos together with the fact that primeFinset membership provides Nat.Prime p.

Zero function gives zero energy

theorem ConnesLean.zeroExtend_zero (I : Set ℝ) : zeroExtend 0 I = 0

Zero-extending the zero function gives the zero function.

theorem ConnesLean.energyForm_zero (cutoffLambda : ℝ) : energyForm cutoffLambda 0 = 0

The energy form of the zero function is zero: E_λ(0) = 0.