Moments of the logistic functional E[φ] = ∫ φ(1/2 + iy) ρ(y) dy (the proof notes, §0, §5.1): E[t^m] = B_m (Bernoulli numbers with B₁ = +1/2, i.e. bernoulli'), and for j ≥ 0, p ≥ 0, E[(t+j)^{-(p+1)}] = (p+1) (ζ(p+2) − H_j^{(p+2)}). Both follow from the shift rule E[F(t+1)] − E[F(t)] = F'(1) alone.

noncomputable def Zeta32.Analytic.Contour.Erho (φ : ℂ → ℂ) : ℂ

The logistic functional.

Equations

• Zeta32.Analytic.Contour.Erho φ = ∫ (y : ℝ), φ (Zeta32.Analytic.Contour.tpt y) * ↑(Zeta32.Analytic.Contour.rho y)

theorem Zeta32.Analytic.Contour.norm_tpt_le (y : ℝ) : ‖tpt y‖ ≤ 1 + |y|

theorem Zeta32.Analytic.Contour.norm_le_of_strip {t : ℂ} (h1 : 1 / 2 ≤ t.re) (h2 : t.re ≤ 3 / 2) : ‖t‖ ≤ 2 * (1 + |t.im|)

theorem Zeta32.Analytic.Contour.polyGrowth_pow (m : ℕ) : PolyGrowth (fun (t : ℂ) => t ^ m) (2 ^ m) m

theorem Zeta32.Analytic.Contour.integrable_pow_rho (m : ℕ) : MeasureTheory.Integrable (fun (y : ℝ) => tpt y ^ m * ↑(rho y)) MeasureTheory.volume

theorem Zeta32.Analytic.Contour.Erho_pow_recursion (m : ℕ) : (∑ k ∈ Finset.range m, ↑(m.choose k) * Erho fun (t : ℂ) => t ^ k) = ↑m

The recursion Σ_{k<m} C(m,k) E[t^k] = m.

theorem Zeta32.Analytic.Contour.Erho_pow (m : ℕ) : (Erho fun (t : ℂ) => t ^ m) = ↑(bernoulli' m)

Polynomial moments: E[t^m] = B_m with B₁ = +1/2.

Poles

noncomputable def Zeta32.Analytic.Contour.invPow (j p : ℕ) (t : ℂ) : ℂ

(t + j)^{-(p+1)}.

Equations

• Zeta32.Analytic.Contour.invPow j p t = ((t + ↑j) ^ (p + 1))⁻¹

theorem Zeta32.Analytic.Contour.add_nat_re (t : ℂ) (j : ℕ) : (t + ↑j).re = t.re + ↑j

theorem Zeta32.Analytic.Contour.norm_add_nat_ge {t : ℂ} (j : ℕ) : t.re + ↑j ≤ ‖t + ↑j‖

theorem Zeta32.Analytic.Contour.add_nat_ne_zero {t : ℂ} (ht : 0 < t.re) (j : ℕ) : t + ↑j ≠ 0

theorem Zeta32.Analytic.Contour.differentiableOn_invPow (j p : ℕ) : DifferentiableOn ℂ (invPow j p) strip

theorem Zeta32.Analytic.Contour.norm_invPow_le {t : ℂ} (ht : 1 / 2 ≤ t.re) (j p : ℕ) : ‖invPow j p t‖ ≤ 2 ^ (p + 1)

theorem Zeta32.Analytic.Contour.polyGrowth_invPow (j p : ℕ) : PolyGrowth (invPow j p) (2 ^ (p + 1)) 0

theorem Zeta32.Analytic.Contour.norm_invPow_tpt_le (j p : ℕ) (hj : 1 ≤ j) (y : ℝ) : ‖invPow j p (tpt y)‖ ≤ 1 / ↑j

theorem Zeta32.Analytic.Contour.invPow_add_one (j p : ℕ) (t : ℂ) : invPow j p (t + 1) = invPow (j + 1) p t

theorem Zeta32.Analytic.Contour.hasDerivAt_invPow (j p : ℕ) : HasDerivAt (invPow j p) (-↑(p + 1) / (1 + ↑j) ^ (p + 2)) 1

theorem Zeta32.Analytic.Contour.integrable_invPow_rho (j p : ℕ) : MeasureTheory.Integrable (fun (y : ℝ) => invPow j p (tpt y) * ↑(rho y)) MeasureTheory.volume

theorem Zeta32.Analytic.Contour.integrable_rho : MeasureTheory.Integrable rho MeasureTheory.volume

theorem Zeta32.Analytic.Contour.norm_Erho_le {φ : ℂ → ℂ} {c : ℝ} (h : ∀ (y : ℝ), ‖φ (tpt y)‖ ≤ c) : ‖Erho φ‖ ≤ c * ∫ (y : ℝ), rho y

theorem Zeta32.Analytic.Contour.Erho_invPow_succ (j p : ℕ) : Erho (invPow (j + 1) p) = Erho (invPow j p) - ↑(p + 1) / ↑(j + 1) ^ (p + 2)

The pole recursion E[(t+j+1)^{-(p+1)}] = E[(t+j)^{-(p+1)}] − (p+1)/(j+1)^{p+2}.

noncomputable def Zeta32.Analytic.Contour.tailTerm (s j k : ℕ) : ℝ

Real p-series tail term 1/(k + j + 1)^s.

Equations

• Zeta32.Analytic.Contour.tailTerm s j k = 1 / (↑k + ↑j + 1) ^ s

theorem Zeta32.Analytic.Contour.Erho_invPow_telescope (j p N : ℕ) : Erho (invPow j p) = Erho (invPow (j + N) p) + ↑(p + 1) * ∑ k ∈ Finset.range N, ↑(tailTerm (p + 2) j k)

theorem Zeta32.Analytic.Contour.summable_zetaTerm {s : ℕ} (hs : 1 < s) : Summable fun (k : ℕ) => 1 / (↑k + 1) ^ s

theorem Zeta32.Analytic.Contour.H_eq_sum_range (e j : ℕ) : ↑(H e j) = ∑ i ∈ Finset.range j, 1 / (↑i + 1) ^ e

theorem Zeta32.Analytic.Contour.tsum_tailTerm {s : ℕ} (hs : 1 < s) (j : ℕ) : ∑' (k : ℕ), tailTerm s j k = ∑' (k : ℕ), 1 / (↑k + 1) ^ s - ↑(H s j)

Σ_{k ≥ 0} 1/(k+j+1)^s = ζ(s) − H_j^{(s)} with ζ(s) written as a tsum.

theorem Zeta32.Analytic.Contour.Erho_invPow (j p : ℕ) : Erho (invPow j p) = ↑(p + 1) * ↑(∑' (k : ℕ), 1 / (↑k + 1) ^ (p + 2) - ↑(H (p + 2) j))

Pole moments E[(t+j)^{-(p+1)}] = (p+1)(ζ(p+2) − H_j^{(p+2)}).