Archimedean Weight and Pointwise Bounds

Defines the archimedean weight w(t) = exp(t/2) / (2 sinh t) for t > 0 and proves key estimates: positivity, sinh t ≥ t, w(t) ≤ exp(t/2)/(2t), the cancellation identity 2 exp(-t/2) w(t) = 1/sinh(t), tail bound 1/sinh(t) < 4 exp(-t) for t ≥ 1, and integrability of correction terms.

Reference: lamportform.tex, Section 2, lines 329–332, 399–416.

The archimedean weight function

def ConnesLean.archWeight (t : ℝ) : ℝ

The archimedean weight w(t) = exp(t/2) / (2 sinh t), defined for all t : ℝ. Meaningful for t > 0 where sinh t > 0.

Reference: lamportform.tex, line 331.

Equations

• ConnesLean.archWeight t = Real.exp (t / 2) / (2 * Real.sinh t)

Auxiliary lemmas

theorem ConnesLean.sinh_ge_self {t : ℝ} (ht : 0 ≤ t) : t ≤ Real.sinh t

sinh t ≥ t for t ≥ 0, via the mean value theorem: sinh' = cosh ≥ 1 and sinh 0 = 0.

theorem ConnesLean.sinh_pos_of_pos {t : ℝ} (ht : 0 < t) : 0 < Real.sinh t

sinh t > 0 for t > 0.

Positivity and basic bounds

theorem ConnesLean.archWeight_pos {t : ℝ} (ht : 0 < t) : 0 < archWeight t

The archimedean weight is positive for t > 0.

theorem ConnesLean.two_exp_neg_half_mul_archWeight {t : ℝ} (ht : 0 < t) : 2 * Real.exp (-t / 2) * archWeight t = 1 / Real.sinh t

The key cancellation: 2 exp(-t/2) w(t) = 1 / sinh t. This simplifies the tail integrand in Step 7.2.

theorem ConnesLean.archWeight_le_inv_two_t {t : ℝ} (ht : 0 < t) : archWeight t ≤ Real.exp (t / 2) / (2 * t)

w(t) ≤ exp(t/2) / (2t) for t > 0, using sinh t ≥ t.

Estimates for the tail integral

theorem ConnesLean.sinh_gt_exp_div_four {t : ℝ} (ht : 1 ≤ t) : Real.exp t / 4 < Real.sinh t

For t ≥ 1, sinh t > exp t / 4. Since exp t ≥ 2 for t ≥ 1, we get exp(-t) ≤ 1/2, and 2 sinh t = exp t - exp(-t) > exp t / 2.

theorem ConnesLean.one_div_sinh_lt_four_exp_neg {t : ℝ} (ht : 1 ≤ t) : 1 / Real.sinh t < 4 * Real.exp (-t)

For t ≥ 1, 1 / sinh t < 4 exp(-t).

Bound on the correction integrand

theorem ConnesLean.abs_exp_neg_half_sub_one_le {t : ℝ} (ht : 0 ≤ t) : |Real.exp (-t / 2) - 1| ≤ t / 2

For t ≥ 0, |exp(-t/2) - 1| ≤ t/2. Since -t/2 ≤ 0, we have exp(-t/2) ≤ 1, and by add_one_le_exp, 1 - t/2 ≤ exp(-t/2).

theorem ConnesLean.correction_integrand_bound {t : ℝ} (ht : 0 < t) : |2 * (Real.exp (-t / 2) - 1) * archWeight t| ≤ Real.exp (t / 2) / 2

The correction integrand |2(exp(-t/2) - 1) w(t)| is bounded by exp(t/2) / 2 for t > 0, using |exp(-t/2) - 1| ≤ t/2 and w(t) ≤ exp(t/2)/(2t).

Integrability estimates

theorem ConnesLean.arch_tail_integrable {L : ℝ} (hL : 1 / 2 ≤ L) : MeasureTheory.IntegrableOn (fun (t : ℝ) => 1 / Real.sinh t) (Set.Ioi (2 * L)) MeasureTheory.volume

The tail integrand 1/sinh t is integrable on (2L, ∞) for L ≥ 1/2. By comparison with 4 exp(-t) (from one_div_sinh_lt_four_exp_neg) which is integrable on (2L, ∞) (from integrableOn_exp_neg_Ioi).

Reference: lamportform.tex, Step 7.2.

theorem ConnesLean.arch_correction_integrable {L : ℝ} (_hL : 0 < L) : MeasureTheory.IntegrableOn (fun (t : ℝ) => 2 * (Real.exp (-t / 2) - 1) * archWeight t) (Set.Ioc 0 (2 * L)) MeasureTheory.volume

The correction integrand 2(exp(-t/2) - 1) w(t) is integrable on (0, 2L]. By correction_integrand_bound, the integrand is bounded by exp(t/2)/2 for each t, and on Ioc 0 (2L) we have t ≤ 2L, so t/2 ≤ L and hence exp(t/2) ≤ exp(L). Thus the integrand is uniformly bounded by exp(L)/2 on this finite-measure set.

Reference: lamportform.tex, Step 8.2.

theorem ConnesLean.measurable_archEnergyIntegrand {G : ℝ → ℂ} (hG : Measurable G) (L : ℝ) : Measurable fun (t : ℝ) => ∫⁻ (u : ℝ), ↑‖zeroExtend G (logInterval L) u - translationOp t (zeroExtend G (logInterval L)) u‖₊ ^ 2

The map t ↦ ‖G̃ - S_t G̃‖² is measurable as a function of t. This is a prerequisite for the outer integral in the energy decomposition to type-check. Follows from measurability of translationOp in t and measurability of the Lebesgue integral.

Archimedean energy integrand

def ConnesLean.archEnergyIntegrand (G : ℝ → ℂ) (L t : ℝ) : ENNReal

The archimedean energy integrand: w(t) * ‖G̃ - S_t G̃‖² as an ENNReal-valued function of t.

This is the integrand in the archimedean energy decomposition.

Equations

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

def ConnesLean.archEnergyIntegral (G : ℝ → ℂ) (L : ℝ) : ENNReal

The archimedean energy integral on (0, 2L): ∫₀^{2L} w(t) ‖G̃ - S_t G̃‖² dt.

Equations

• ConnesLean.archEnergyIntegral G L = ∫⁻ (t : ℝ) in Set.Ioo 0 (2 * L), ConnesLean.archEnergyIntegrand G L t

The archimedean constant

def ConnesLean.archConstant (cutoffLambda : ℝ) : ℝ

The archimedean constant c_∞(λ): c_∞(λ) = -(log 4π + γ) + ∫₀^{2L} 2(e^{-t/2} - 1) w(t) dt + ∫_{2L}^∞ 2 e^{-t/2} w(t) dt, where L = log cutoffLambda.

This definition matches the expression used in lamportform.tex (Steps 7.2, 8.2, and 9, around line ~420); analytic convergence of the two integrals is treated there and in subsequent lemmas.

Equations

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