the proof notes (11′), (14′), (15′): tail margin, integration of the configuration bound, and the constant F* = 9(3/2 − log 3) + (9/2)(ℓ − W) ≤ −6.

theorem Zeta32.Analytic.EnergyI.Wt_lower {y : ℝ} (hy : 0 ≤ y) : 2 / 3 * (Real.pi * y - 2 - Real.log (1 + y ^ 2)) ≤ Wt y

theorem Zeta32.Analytic.EnergyI.tail_bound {a : ℝ} (ha : 0 < a) (hm : massA a = 1) : ∃ (B : ℝ), ∀ (x : ℝ), 2 * potA a x - Wt |x| ≤ ellA a - max 0 (|x| - B)

(11′): the margin 2L − W ≤ ℓ − max(0, |x| − B).

theorem Zeta32.Analytic.EnergyI.filter_lt_eq_Ioi {m : ℕ} (l : Fin m) : {l' : Fin m | l < l'} = Finset.Ioi l

theorem Zeta32.Analytic.EnergyI.vandermonde_eq_exp {m : ℕ} (x : Fin m → ℝ) (hx : Function.Injective x) : ∏ l : Fin m, ∏ l' : Fin m with l < l', (x l - x l') ^ 2 = Real.exp (2 * ∑ i : Fin m, ∑ j > i, Real.log |x j - x i|)

theorem Zeta32.Analytic.EnergyI.vandermonde_eq_zero {m : ℕ} (x : Fin m → ℝ) (hx : ¬Function.Injective x) : ∏ l : Fin m, ∏ l' : Fin m with l < l', (x l - x l') ^ 2 = 0

theorem Zeta32.Analytic.EnergyI.config_bound {a : ℝ} (ha : 0 < a) (hm : massA a = 1) : ∃ (B : ℝ) (C : ℝ), ∀ (n : ℕ), 1 ≤ n → ∀ (x : Fin (3 * n) → ℝ), (∏ l : Fin (3 * n), Real.exp (-(3 * ↑n) * Wt |x l|)) * ∏ l : Fin (3 * n), ∏ l' : Fin (3 * n) with l < l', (x l - x l') ^ 2 ≤ Real.exp (9 * ↑n ^ 2 * (ellA a - IA a) + C * ↑n * (Real.log (↑n + 1) + 1)) * ∏ l : Fin (3 * n), Real.exp (-(3 * ↑n) * max 0 (|x l| - B))

Configuration bound: (13′) with ε = (n+1)⁻², combined with 2L − W ≤ ℓ − max(0, |x| − B).

noncomputable def Zeta32.Analytic.EnergyI.tailFun (B m y : ℝ) : ℝ

The tail integrand.

Equations

• Zeta32.Analytic.EnergyI.tailFun B m y = (1 + |y|) ^ 7 * Real.exp (-m * max 0 (|y| - B))

theorem Zeta32.Analytic.EnergyI.continuous_tailFun (B m : ℝ) : Continuous (tailFun B m)

theorem Zeta32.Analytic.EnergyI.tailFun_le_one_add_sq (B : ℝ) {m : ℝ} (hm : 1 ≤ m) (y : ℝ) : tailFun B m y ≤ Real.exp B * (↑(Nat.factorial 9) * Real.exp 1) * (1 + y ^ 2)⁻¹

theorem Zeta32.Analytic.EnergyI.integrable_tailFun (B : ℝ) {m : ℝ} (hm : 1 ≤ m) : MeasureTheory.Integrable (tailFun B m) MeasureTheory.volume

theorem Zeta32.Analytic.EnergyI.integral_tailFun_le (B : ℝ) {m : ℝ} (hm : 1 ≤ m) : ∫ (y : ℝ), tailFun B m y ≤ ∫ (y : ℝ), tailFun B 1 y

theorem Zeta32.Analytic.EnergyI.eventually_lin_log_le (M : ℝ) {δ : ℝ} (hδ : 0 < δ) : ∀ᶠ (n : ℕ) in Filter.atTop, M * ↑n * (Real.log (↑n + 1) + 1) ≤ δ * ↑n ^ 2

theorem Zeta32.Analytic.EnergyI.energy_bound_exp (r : ℚ) (hH : ∀ (n : ℕ), HeineBound r n) (hF : FstarInput) (ε : ℝ) (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, |(Polynomial.aeval (Cr r)) (Qtilde r n)| ≤ Real.exp ((-6 + ε) * ↑n ^ 2)

The energy bound in exponential form (unlike a logarithmic form, it does not need Q ≠ 0).