Archimedean Distribution W_R(f)

Defines the archimedean distribution combining the logarithmic constant term and weighted integral of shifted function differences: W_R(f) = (log 4π + γ) f(1) + ∫₀^∞ (f(eᵗ) + f(e⁻ᵗ) - 2 e⁻ᵗ/² f(1)) w(t) dt

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

Auxiliary: exponential negation

@[simp]

theorem ConnesLean.expToRPos_neg (t : ℝ) : expToRPos (-t) = (expToRPos t)⁻¹

expToRPos (-t) equals (expToRPos t)⁻¹: negating the additive coordinate corresponds to inversion in the multiplicative group R_+*.

The archimedean distribution

def ConnesLean.archDistribution (f : RPos → ℂ) : ℂ

The archimedean distribution W_R(f) from equation (3) of lamportform.tex.

For f : RPos → ℂ, this is: W_R(f) = (log 4π + γ) f(1) + ∫_{(0,∞)} (f(e^t) + f(e^{-t}) - 2 e^{-t/2} f(1)) w(t) dt

The Bochner integral returns 0 for non-integrable integrands, so this definition is total. It is meaningful when f has compact support in RPos.

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

Equations

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

Properties of the archimedean distribution

theorem ConnesLean.archDistribution_zero : archDistribution 0 = 0

The archimedean distribution of the zero function is zero.

theorem ConnesLean.archDistribution_const (c : ℂ) : (archDistribution fun (x : RPos) => c) = ↑(Real.log (4 * Real.pi) + Real.eulerMascheroniConstant) * c + ∫ (t : ℝ) in Set.Ioi 0, (2 - 2 * ↑(Real.exp (-t / 2))) * ↑(archWeight t) * c

The archimedean distribution at a constant function f(x) = c equals (log 4π + γ) c + ∫_{(0,∞)} (2 - 2 exp(-t/2)) w(t) dt · c. In particular the singular part (log 4π + γ) c is explicitly visible.