The logistic density ρ(y) = (π/2) sech²(πy) on the line t = 1/2 + i y, its derivative, the kernel w = 2rρ + iρ' of Interfaces.lean, and integrability of polynomially bounded functions against them (the proof notes, 5.1).

noncomputable def Zeta32.Analytic.Contour.tpt (y : ℝ) : ℂ

The contour point t = 1/2 + i y, written exactly as in heineIntegrand.

Equations

• Zeta32.Analytic.Contour.tpt y = 1 / 2 + Complex.I * ↑y

noncomputable def Zeta32.Analytic.Contour.rho (y : ℝ) : ℝ

The logistic density ρ(y) = (π/2) sech²(πy).

Equations

• Zeta32.Analytic.Contour.rho y = Real.pi / 2 / Real.cosh (Real.pi * y) ^ 2

noncomputable def Zeta32.Analytic.Contour.rhoDeriv (y : ℝ) : ℝ

ρ'(y) = -π² sinh(πy) / cosh³(πy).

Equations

• Zeta32.Analytic.Contour.rhoDeriv y = -(Real.pi ^ 2 * Real.sinh (Real.pi * y) / Real.cosh (Real.pi * y) ^ 3)

theorem Zeta32.Analytic.Contour.tpt_re (y : ℝ) : (tpt y).re = 1 / 2

theorem Zeta32.Analytic.Contour.tpt_im (y : ℝ) : (tpt y).im = y

theorem Zeta32.Analytic.Contour.continuous_tpt : Continuous tpt

theorem Zeta32.Analytic.Contour.cosh_pi_pos (y : ℝ) : 0 < Real.cosh (Real.pi * y)

theorem Zeta32.Analytic.Contour.rho_pos (y : ℝ) : 0 < rho y

theorem Zeta32.Analytic.Contour.continuous_rho : Continuous rho

theorem Zeta32.Analytic.Contour.continuous_rhoDeriv : Continuous rhoDeriv

theorem Zeta32.Analytic.Contour.hasDerivAt_rho (y : ℝ) : HasDerivAt rho (rhoDeriv y) y

theorem Zeta32.Analytic.Contour.rhoDeriv_eq (y : ℝ) : rhoDeriv y = -(2 * Real.pi * Real.tanh (Real.pi * y) * rho y)

theorem Zeta32.Analytic.Contour.wfun_eq (r : ℚ) (y : ℝ) : wfun r y = 2 * ↑r * ↑(rho y) + Complex.I * ↑(rhoDeriv y)

theorem Zeta32.Analytic.Contour.exp_abs_le_two_cosh (x : ℝ) : Real.exp |x| ≤ 2 * Real.cosh x

theorem Zeta32.Analytic.Contour.inv_cosh_sq_le (x : ℝ) : 1 / Real.cosh x ^ 2 ≤ 4 * Real.exp (-(2 * |x|))

theorem Zeta32.Analytic.Contour.rho_le (y : ℝ) : rho y ≤ 2 * Real.pi * Real.exp (-(2 * Real.pi) * |y|)

theorem Zeta32.Analytic.Contour.abs_rhoDeriv_le (y : ℝ) : |rhoDeriv y| ≤ 2 * Real.pi * rho y

theorem Zeta32.Analytic.Contour.integrable_abs_pow_exp (n : ℕ) {b : ℝ} (hb : 0 < b) : MeasureTheory.Integrable (fun (x : ℝ) => |x| ^ n * Real.exp (-b * |x|)) MeasureTheory.volume

theorem Zeta32.Analytic.Contour.integrable_one_add_abs_pow_exp (n : ℕ) {b : ℝ} (hb : 0 < b) : MeasureTheory.Integrable (fun (x : ℝ) => (1 + |x|) ^ n * Real.exp (-b * |x|)) MeasureTheory.volume

theorem Zeta32.Analytic.Contour.integrable_mul_of_le_rho {f : ℝ → ℂ} {g : ℝ → ℝ} (hf : Continuous f) (hg : Continuous g) {c C : ℝ} {N : ℕ} (hgc : ∀ (y : ℝ), |g y| ≤ c * rho y) (hfb : ∀ (y : ℝ), ‖f y‖ ≤ C * (1 + |y|) ^ N) : MeasureTheory.Integrable (fun (y : ℝ) => f y * ↑(g y)) MeasureTheory.volume

A continuous function with polynomial growth, times a real weight bounded by c·ρ, is integrable.

theorem Zeta32.Analytic.Contour.integrable_mul_rho {f : ℝ → ℂ} (hf : Continuous f) {C : ℝ} {N : ℕ} (hfb : ∀ (y : ℝ), ‖f y‖ ≤ C * (1 + |y|) ^ N) : MeasureTheory.Integrable (fun (y : ℝ) => f y * ↑(rho y)) MeasureTheory.volume

theorem Zeta32.Analytic.Contour.integrable_mul_rhoDeriv {f : ℝ → ℂ} (hf : Continuous f) {C : ℝ} {N : ℕ} (hfb : ∀ (y : ℝ), ‖f y‖ ≤ C * (1 + |y|) ^ N) : MeasureTheory.Integrable (fun (y : ℝ) => f y * ↑(rhoDeriv y)) MeasureTheory.volume

theorem Zeta32.Analytic.Contour.integrable_mul_wfun (r : ℚ) {f : ℝ → ℂ} (hf : Continuous f) {C : ℝ} {N : ℕ} (hfb : ∀ (y : ℝ), ‖f y‖ ≤ C * (1 + |y|) ^ N) : MeasureTheory.Integrable (fun (y : ℝ) => f y * wfun r y) MeasureTheory.volume