Documentation

LeanPool.Zeta32.Analytic.Contour.Shift

The shift rule of the proof notes, §0 for the logistic functional E[φ] = ∫ φ(1/2 + i y) ρ(y) dy: for F holomorphic on 0 < Re t < 2 with polynomial growth on 1/2 ≤ Re t ≤ 3/2, E[F(t+1)] − E[F(t)] = F'(1). Obtained from boundaryIntegral_mul_Kc by letting the height T → ∞: on both vertical edges π²/sin²(πt) = 2πρ(y), and on the horizontal edges |π²/sin²(πt)| ≤ 16π² e^{-2πT}.

source
theorem Zeta32.Analytic.Contour.complexSin_norm_sq (z : ℂ) :
‖Complex.sin z‖ ^ 2 = Real.sin z.re ^ 2 + Real.sinh z.im ^ 2
source
theorem Zeta32.Analytic.Contour.complexSinh_abs_im_le_norm_sin (z : ℂ) :
Real.sinh |z.im| ≤ ‖Complex.sin z‖
source
theorem Zeta32.Analytic.Contour.exp_quarter_le_sinh {t : ℝ} (ht : 1 ≤ t) :
Real.exp t / 4 ≤ Real.sinh t
source
theorem Zeta32.Analytic.Contour.complexSin_pi_norm_ge_exp (z : ℂ) (hz : 1 ≤ |z.im|) :
Real.exp (Real.pi * |z.im|) / 4 ≤ ‖Complex.sin (↑Real.pi * z)‖
source
theorem Zeta32.Analytic.Contour.norm_Kc_le (z : ℂ) (hz : 1 ≤ |z.im|) :
‖Kc z‖ ≤ 16 * Real.pi ^ 2 * Real.exp (-(2 * Real.pi) * |z.im|)
source
theorem Zeta32.Analytic.Contour.Kc_add_one (t : ℂ) :
Kc (t + 1) = Kc t
source
theorem Zeta32.Analytic.Contour.sin_pi_tpt (y : ℝ) :
Complex.sin (↑Real.pi * tpt y) = ↑(Real.cosh (Real.pi * y))
source
theorem Zeta32.Analytic.Contour.Kc_tpt (y : ℝ) :
Kc (tpt y) = 2 * ↑Real.pi * ↑(rho y)
source
theorem Zeta32.Analytic.Contour.tpt_mem_strip (y : ℝ) :
tpt y ∈ strip
source
theorem Zeta32.Analytic.Contour.tpt_add_one_mem_strip (y : ℝ) :
tpt y + 1 ∈ strip
source
theorem Zeta32.Analytic.Contour.zT_re (T : ℝ) :
(zT T).re = 1 / 2
source
theorem Zeta32.Analytic.Contour.zT_im (T : ℝ) :
(zT T).im = -T
source
theorem Zeta32.Analytic.Contour.wT_re (T : ℝ) :
(wT T).re = 3 / 2
source
theorem Zeta32.Analytic.Contour.wT_im (T : ℝ) :
(wT T).im = T
source
theorem Zeta32.Analytic.Contour.left_pt (y : ℝ) :
↑(1 / 2) + ↑y * Complex.I = tpt y
source
theorem Zeta32.Analytic.Contour.right_pt (y : ℝ) :
↑(3 / 2) + ↑y * Complex.I = tpt y + 1
source
def Zeta32.Analytic.Contour.PolyGrowth (F : ℂ → ℂ) (C : ℝ) (N : ℕ) :
Prop

The growth hypothesis on the closed strip 1/2 ≤ Re t ≤ 3/2.

Equations
Instances For
    source
    theorem Zeta32.Analytic.Contour.horizontal_bound {F : ℂ → ℂ} {C : ℝ} {N : ℕ} (hg : PolyGrowth F C N) {c : ℝ} (hc : 1 ≤ |c|) :
    ‖∫ (x : ℝ) in 1 / 2..3 / 2, F (↑x + ↑c * Complex.I) * Kc (↑x + ↑c * Complex.I)‖ ≤ C * (1 + |c|) ^ N * (16 * Real.pi ^ 2 * Real.exp (-(2 * Real.pi) * |c|))
    source
    theorem Zeta32.Analytic.Contour.tendsto_growth_exp (C : ℝ) (N : ℕ) :
    Filter.Tendsto (fun (T : ℝ) => C * (1 + T) ^ N * (16 * Real.pi ^ 2 * Real.exp (-(2 * Real.pi) * T))) Filter.atTop (nhds 0)
    source
    theorem Zeta32.Analytic.Contour.polyGrowth_line {F : ℂ → ℂ} {C : ℝ} {N : ℕ} (hg : PolyGrowth F C N) (y : ℝ) :
    ‖F (tpt y)‖ ≤ C * (1 + |y|) ^ N
    source
    theorem Zeta32.Analytic.Contour.polyGrowth_line_add_one {F : ℂ → ℂ} {C : ℝ} {N : ℕ} (hg : PolyGrowth F C N) (y : ℝ) :
    ‖F (tpt y + 1)‖ ≤ C * (1 + |y|) ^ N
    source
    theorem Zeta32.Analytic.Contour.shift_rule {F : ℂ → ℂ} (hF : DifferentiableOn ℂ F strip) {C : ℝ} {N : ℕ} (hg : PolyGrowth F C N) :
    (∫ (y : ℝ), F (tpt y + 1) * ↑(rho y)) - ∫ (y : ℝ), F (tpt y) * ↑(rho y) = deriv F 1

    Shift rule E[F(t+1)] − E[F(t)] = F'(1).