Source indexedtheorem · leanprover/lean4:v4.32.0

tendsto_truncated_vertical_shift_with_simple_pole_Ioo

PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:191 to 207

Source documentation

Set-integral form of tendsto_truncated_vertical_shift_with_simple_pole, normalized as (2π)⁻¹ ∫ f(σ + it) dt.

Exact Lean statement

theorem tendsto_truncated_vertical_shift_with_simple_pole_Ioo
    {σ σ' : ℝ} {f : ℂ → ℂ} {p A : ℂ} (hσ : σ < p.re ∧ p.re < σ')
    (hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p}))
    (hpole : (f - (fun s ↦ A / (s - p))) =O[𝓝[≠] p] (1 : ℂ → ℂ))
    (hbot : Tendsto (fun (y : ℝ) ↦ ∫ (x : ℝ) in σ..σ', f (x + y * I)) atBot (𝓝 0))
    (htop : Tendsto (fun (y : ℝ) ↦ ∫ (x : ℝ) in σ..σ', f (x + y * I)) atTop (𝓝 0))
    (hright : Integrable (fun (y : ℝ) ↦ f (σ' + y * I))) :
    Tendsto (fun T : ℝ ↦ (1 / (2 * π) : ℂ) * ∫ t in Set.Ioo (-T) T,
        f (σ + t * I)) atTop (𝓝 (VerticalIntegral' f σ' - A))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem tendsto_truncated_vertical_shift_with_simple_pole_Ioo    {σ σ' : ℝ} {f : ℂ → ℂ} {p A : ℂ} (hσ : σ < p.re ∧ p.re < σ')    (hf : HolomorphicOn f (Icc σ σ' ×ℂ univ \ {p}))    (hpole : (f - (fun s ↦ A / (s - p))) =O[𝓝[≠] p] (1 : ℂ → ℂ))    (hbot : Tendsto (fun (y : ℝ) ↦ ∫ (x : ℝ) in σ..σ', f (x + y * I)) atBot (𝓝 0))    (htop : Tendsto (fun (y : ℝ) ↦ ∫ (x : ℝ) in σ..σ', f (x + y * I)) atTop (𝓝 0))    (hright : Integrable (fun (y : ℝ) ↦ f (σ' + y * I))) :    Tendsto (fun T : ℝ ↦ (1 / (2 * π) : ℂ) * ∫ t in Set.Ioo (-T) T,        f (σ + t * I)) atTop (𝓝 (VerticalIntegral' f σ' - A)) := by  have hbase := tendsto_truncated_vertical_shift_with_simple_pole hσ hf hpole hbot htop hright  refine hbase.congr' ?_  filter_upwards [eventually_ge_atTop (0 : ℝ)] with T hT  rw [VIntegral]  rw [intervalIntegral.integral_of_le (by linarith : -T ≤ T),    MeasureTheory.integral_Ioc_eq_integral_Ioo]  simp only [smul_eq_mul]  field_simp [Complex.I_ne_zero, Real.pi_ne_zero]