Prime Distribution and Energy Decomposition

Defines prime-indexed bounds, the prime constant c_p(λ), and structures for prime energy terms. For each prime p, the local distribution is W_p(f) = (log p) Σ_{m ≥ 1} p^{-m/2} (f(p^m) + f(p^{-m})), and -W_p(f) decomposes into translation norms plus a correction term.

Reference: lamportform.tex, Section 2, equation (2).

Bounds for prime sums

def ConnesLean.primeBound (cutoffLambda : ℝ) : ℕ

The upper bound for primes in the sum: floor(cutoffLambda^2). Only primes p <= cutoffLambda^2 contribute to the energy decomposition.

Equations

• ConnesLean.primeBound cutoffLambda = ⌊cutoffLambda ^ 2⌋₊

def ConnesLean.primeExponentBound (p : ℕ) (cutoffLambda : ℝ) : ℕ

The upper bound for exponents: floor(2 log cutoffLambda / log p). For prime p, only exponents m with p^m <= cutoffLambda^2 contribute, which is equivalent to m <= 2 log cutoffLambda / log p.

Equations

• ConnesLean.primeExponentBound p cutoffLambda = ⌊2 * Real.log cutoffLambda / Real.log ↑p⌋₊

def ConnesLean.primeFinset (cutoffLambda : ℝ) : Finset ℕ

The finset of primes up to primeBound cutoffLambda.

Equations

• ConnesLean.primeFinset cutoffLambda = Finset.filter Nat.Prime (Finset.range (ConnesLean.primeBound cutoffLambda + 1))

def ConnesLean.exponentFinset (p : ℕ) (cutoffLambda : ℝ) : Finset ℕ

The finset of exponents {1, ..., primeExponentBound p cutoffLambda}.

Equations

• ConnesLean.exponentFinset p cutoffLambda = Finset.Icc 1 (ConnesLean.primeExponentBound p cutoffLambda)

Prime constant

def ConnesLean.primeConstant (p : ℕ) (cutoffLambda : ℝ) : ℝ

The prime constant c_p(cutoffLambda) = -2(log p) Sum_{m=1}^{M_p} p^{-m/2}, where M_p = primeExponentBound p cutoffLambda.

This collects the ‖G‖² terms from applying the unitary identity to each inner product <g, U_{p^m} g>.

Reference: lamportform.tex, line 316.

Equations

• ConnesLean.primeConstant p cutoffLambda = -2 * Real.log ↑p * ∑ m ∈ ConnesLean.exponentFinset p cutoffLambda, ↑p ^ (-↑m / 2)

theorem ConnesLean.primeConstant_nonpos {p : ℕ} (hp : Nat.Prime p) {cutoffLambda : ℝ} (_hLam : 1 < cutoffLambda) : primeConstant p cutoffLambda ≤ 0

The prime constant is nonpositive: c_p(cutoffLambda) <= 0. Each term in the sum is positive (p > 0, log p > 0), so the overall expression with the leading -2 is nonpositive.

Prime energy decomposition structure

def ConnesLean.primeEnergyTerm (p m : ℕ) (G : ℝ → ℂ) (L : ℝ) : ENNReal

The prime energy term for exponent m: the squared L² norm of the difference ‖G_tilde - S_{m log p} G_tilde‖² weighted by (log p) p^{-m/2}.

This is the m-th summand in the prime energy decomposition.

Equations

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

def ConnesLean.totalPrimeEnergy (p : ℕ) (cutoffLambda : ℝ) (G : ℝ → ℂ) (L : ℝ) : ENNReal

The total prime energy: sum of prime energy terms over all relevant exponents. E_p(cutoffLambda, G) = Sum_{m=1}^{M_p} (log p) p^{-m/2} ‖G_tilde - S_{m log p} G_tilde‖².

Equations

• ConnesLean.totalPrimeEnergy p cutoffLambda G L = ∑ m ∈ ConnesLean.exponentFinset p cutoffLambda, ConnesLean.primeEnergyTerm p m G L