the proof notes, §5.2: Heine determinant integral and absolute-value bound.

Every entry of X • B + A at X = C_r is ∫ t^i · t^k (t R_n)(t) w(y) dy with t = 1/2 + iy (logistic_representation). Andréief's identity turns the determinant into (1/h!) ∫ det[t_j^i] · det[t_j^i (tR_n)(t_j) w(y_j)] dy; both determinants are Vandermonde determinants in t_j = 1/2 + i y_j, and |t_j − t_l| = |y_j − y_l|, which gives HeineBound. The statement HeineBound of Interfaces.lean is proved literally, for every r and n (including n = 0).

noncomputable def Zeta32.Analytic.heinePhi (r : ℚ) (n : ℕ) (y : ℝ) : ℂ

The one-point factor (t R_n)(t) w(y) of heineIntegrand, t = 1/2 + iy.

Equations

• Zeta32.Analytic.heinePhi r n y = Zeta32.Analytic.Contour.tpt y * Zeta32.Rfun n (Zeta32.Analytic.Contour.tpt y) * Zeta32.wfun r y

noncomputable def Zeta32.Analytic.heineF (n : ℕ) : Fin (3 * n) → ℝ → ℂ

Andréief row functions t^i.

Equations

• Zeta32.Analytic.heineF n i y = Zeta32.Analytic.Contour.tpt y ^ ↑i

noncomputable def Zeta32.Analytic.heineG (r : ℚ) (n : ℕ) : Fin (3 * n) → ℝ → ℂ

Andréief column functions t^k (t R_n)(t) w(y).

Equations

• Zeta32.Analytic.heineG r n k y = Zeta32.Analytic.Contour.tpt y ^ ↑k * Zeta32.Analytic.heinePhi r n y

theorem Zeta32.Analytic.heineF_mul_heineG (r : ℚ) (n : ℕ) (i k : Fin (3 * n)) (y : ℝ) : heineF n i y * heineG r n k y = Contour.tpt y * (Contour.tpt y ^ (↑i + ↑k) * Rfun n (Contour.tpt y)) * wfun r y

theorem Zeta32.Analytic.heine_aeval_Q_eq_det (r : ℚ) (n : ℕ) : ↑((Polynomial.aeval (Cr r)) (Q r n)) = (Matrix.of fun (i k : Fin (3 * n)) => ↑(Cr r) * ↑(slope n (↑i + ↑k)) + ↑(intercept r n (↑i + ↑k))).det

Q_n(C_r) as the determinant of the complex entries C_r · slope + intercept.

theorem Zeta32.Analytic.heine_identity (r : ℚ) (n : ℕ) : ↑((Polynomial.aeval (Cr r)) (Q r n)) = 1 / ↑(3 * n).factorial * ∫ (x : Fin (3 * n) → ℝ), (Matrix.of fun (i j : Fin (3 * n)) => heineF n i (x j)).det * (Matrix.of fun (i j : Fin (3 * n)) => heineG r n i (x j)).det

Heine identity: Q_n(C_r) = (1/h!) ∫ det[t_j^i] det[t_j^i (tR_n)(t_j) w(y_j)] dy.

theorem Zeta32.Analytic.heine_det_F (n : ℕ) (x : Fin (3 * n) → ℝ) : (Matrix.of fun (i j : Fin (3 * n)) => heineF n i (x j)).det = ∏ i : Fin (3 * n), ∏ j > i, (Contour.tpt (x j) - Contour.tpt (x i))

theorem Zeta32.Analytic.heine_det_G (r : ℚ) (n : ℕ) (x : Fin (3 * n) → ℝ) : (Matrix.of fun (i j : Fin (3 * n)) => heineG r n i (x j)).det = (∏ j : Fin (3 * n), heinePhi r n (x j)) * (Matrix.of fun (i j : Fin (3 * n)) => heineF n i (x j)).det

theorem Zeta32.Analytic.heine_tpt_sub (a b : ℝ) : Contour.tpt a - Contour.tpt b = Complex.I * ↑(a - b)

theorem Zeta32.Analytic.heine_norm_vandermonde_sq {m : ℕ} (x : Fin m → ℝ) : ‖∏ i : Fin m, ∏ j > i, (Contour.tpt (x j) - Contour.tpt (x i))‖ ^ 2 = ∏ l : Fin m, ∏ l' : Fin m with l < l', (x l - x l') ^ 2

theorem Zeta32.Analytic.heine_norm_integrand (r : ℚ) (n : ℕ) (x : Fin (3 * n) → ℝ) : ‖(Matrix.of fun (i j : Fin (3 * n)) => heineF n i (x j)).det * (Matrix.of fun (i j : Fin (3 * n)) => heineG r n i (x j)).det‖ = heineIntegrand r n x

theorem Zeta32.Analytic.heine_bound (r : ℚ) (n : ℕ) : HeineBound r n

the proof notes, 5.2 (Heine), bound form.