Fourier Symbol Definition and Basic Properties

Defines the Fourier symbol ψ_λ(ξ) decomposing the energy form in Fourier space:

• Archimedean part: 4 ∫₀^{2L} w(t) sin²(ξt/2) dt
• Prime part: 4 Σ_p Σ_m (log p) p^{-m/2} sin²(ξ · m · log(p) / 2)

Properties: nonnegativity, evenness (from sin²), and vanishing at zero.

Reference: lamportform.tex, Section 7.2, lines 783–842.

Definitions

def ConnesLean.archFourierSymbol (L ξ : ℝ) : ℝ

The archimedean part of the Fourier symbol: 4 ∫ t in (0, 2L), w(t) sin²(ξt/2) dt

Reference: lamportform.tex, line 790.

Equations

• ConnesLean.archFourierSymbol L ξ = 4 * ∫ (t : ℝ) in Set.Ioo 0 (2 * L), ConnesLean.archWeight t * Real.sin (ξ * t / 2) ^ 2

def ConnesLean.primeFourierSymbol (cutoffLambda ξ : ℝ) : ℝ

The prime part of the Fourier symbol: 4 Σ_{p ∈ primeFinset λ} Σ_{m ∈ exponentFinset p λ} (log p) p^{-m/2} sin²(ξ·m·log(p)/2)

Reference: lamportform.tex, line 793.

Equations

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

def ConnesLean.fourierSymbol (cutoffLambda ξ : ℝ) : ℝ

The full Fourier symbol ψ_λ(ξ), defined as the sum of the archimedean and prime parts.

Reference: lamportform.tex, Lemma 9 (line 797).

Equations

• ConnesLean.fourierSymbol cutoffLambda ξ = ConnesLean.archFourierSymbol (Real.log cutoffLambda) ξ + ConnesLean.primeFourierSymbol cutoffLambda ξ

Nonnegativity

theorem ConnesLean.archFourierSymbol_nonneg (L ξ : ℝ) : 0 ≤ archFourierSymbol L ξ

The archimedean Fourier symbol is nonneg: each term has w(t) > 0 and sin² ≥ 0.

theorem ConnesLean.primeFourierSymbol_nonneg (cutoffLambda ξ : ℝ) : 0 ≤ primeFourierSymbol cutoffLambda ξ

The prime Fourier symbol is nonneg: each term has log p > 0, p^{-m/2} > 0, and sin² ≥ 0.

theorem ConnesLean.fourierSymbol_nonneg (cutoffLambda ξ : ℝ) : 0 ≤ fourierSymbol cutoffLambda ξ

The full Fourier symbol is nonneg.

Evenness

theorem ConnesLean.archFourierSymbol_even (L ξ : ℝ) : archFourierSymbol L (-ξ) = archFourierSymbol L ξ

The archimedean Fourier symbol is even: sin²(-x) = sin²(x).

theorem ConnesLean.primeFourierSymbol_even (cutoffLambda ξ : ℝ) : primeFourierSymbol cutoffLambda (-ξ) = primeFourierSymbol cutoffLambda ξ

The prime Fourier symbol is even.

theorem ConnesLean.fourierSymbol_even (cutoffLambda ξ : ℝ) : fourierSymbol cutoffLambda (-ξ) = fourierSymbol cutoffLambda ξ

The full Fourier symbol is even: ψ_λ(-ξ) = ψ_λ(ξ).

Value at zero

theorem ConnesLean.archFourierSymbol_zero (L : ℝ) : archFourierSymbol L 0 = 0

The archimedean Fourier symbol vanishes at ξ = 0.

theorem ConnesLean.primeFourierSymbol_zero (cutoffLambda : ℝ) : primeFourierSymbol cutoffLambda 0 = 0

The prime Fourier symbol vanishes at ξ = 0.

theorem ConnesLean.fourierSymbol_zero (cutoffLambda : ℝ) : fourierSymbol cutoffLambda 0 = 0

The full Fourier symbol vanishes at ξ = 0: ψ_λ(0) = 0.