the proof notes (6′): the scaling y = n x of the Heine integral.

∫_{ℝ^h} heine(y) dy = n^h ∫ heine(n x) dx, Δ(n x)² = n^{h(h−1)} Δ(x)², and (5′) per coordinate; with log F_n ≥ h² log h − (3/2)h² − 2h log h this gives |Q_n(C_r)| ≤ exp(9(3/2 − log 3)n² + C n log(n+1)) ∫ D for every integrable D dominating ∏_l (1+|x_l|)^7 e^{−3n W(x_l)} · Δ(x)².

def Zeta32.Analytic.EnergyI.vdm {m : ℕ} (x : Fin m → ℝ) : ℝ

The squared Vandermonde product in the form of heineIntegrand.

Equations

• Zeta32.Analytic.EnergyI.vdm x = ∏ l : Fin m, ∏ l' : Fin m with l < l', (x l - x l') ^ 2

theorem Zeta32.Analytic.EnergyI.vdm_nonneg {m : ℕ} (x : Fin m → ℝ) : 0 ≤ vdm x

theorem Zeta32.Analytic.EnergyI.sum_card_filter_lt (m : ℕ) : (∑ l : Fin m, {l' : Fin m | l < l'}.card) * 2 = m * (m - 1)

theorem Zeta32.Analytic.EnergyI.vdm_smul {m : ℕ} (c : ℝ) (x : Fin m → ℝ) : vdm (c • x) = c ^ (m * (m - 1)) * vdm x

theorem Zeta32.Analytic.EnergyI.heineIntegrand_eq (r : ℚ) (n : ℕ) (y : Fin (3 * n) → ℝ) : heineIntegrand r n y = (∏ l : Fin (3 * n), psiH r n (y l)) * vdm y

theorem Zeta32.Analytic.EnergyI.heine_scaled (r : ℚ) : ∃ (C : ℝ), ∀ (n : ℕ), 1 ≤ n → HeineBound r n → ∀ (D : (Fin (3 * n) → ℝ) → ℝ), MeasureTheory.Integrable D MeasureTheory.volume → (∀ (x : Fin (3 * n) → ℝ), (∏ l : Fin (3 * n), (1 + |x l|) ^ 7 * Real.exp (-(3 * ↑n) * Wt |x l|)) * ∏ l : Fin (3 * n), ∏ l' : Fin (3 * n) with l < l', (x l - x l') ^ 2 ≤ D x) → |(Polynomial.aeval (Cr r)) (Qtilde r n)| ≤ Real.exp (9 * (3 / 2 - Real.log 3) * ↑n ^ 2 + C * ↑n * Real.log (↑n + 1)) * ∫ (x : Fin (3 * n) → ℝ), D x

(5′)+(6′): the Heine bound after scaling, with the external field nV = −h W.