Source indexedtheorem · leanprover/lean4:v4.32.0

Perron.HolomorphicOn.upperUIntegral_eq_zero

PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:780 to 791

Source documentation

The second case is when $x>1$ . Here are some auxiliary lemmata for the second case. TODO: Move to more general section

Exact Lean statement

theorem HolomorphicOn.upperUIntegral_eq_zero {f : ℂ → ℂ} {σ σ' T : ℝ} (hσ : σ ≤ σ')
    (hf : HolomorphicOn f {z : ℂ | σ ≤ z.re ∧ z.re ≤ σ' ∧ T ≤ z.im})
    (htop : Tendsto (fun y : ℝ ↦ ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0))
    (hleft : Integrable fun y : ℝ ↦ f (↑σ + ↑y * I))
    (hright : Integrable fun y : ℝ ↦ f (↑σ' + ↑y * I)) :
    UpperUIntegral f σ σ' T = 0

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem HolomorphicOn.upperUIntegral_eq_zero {f : ℂ → ℂ} {σ σ' T : ℝ} (hσ : σ ≤ σ')    (hf : HolomorphicOn f {z : ℂ | σ ≤ z.re ∧ z.re ≤ σ' ∧ T ≤ z.im})    (htop : Tendsto (fun y : ℝ ↦ ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0))    (hleft : Integrable fun y : ℝ ↦ f (↑σ + ↑y * I))    (hright : Integrable fun y : ℝ ↦ f (↑σ' + ↑y * I)) :    UpperUIntegral f σ σ' T = 0 := by  apply tendsto_nhds_unique (RectangleIntegral_tendsTo_UpperU htop hleft hright)  apply EventuallyEq.tendsto  filter_upwards [eventually_ge_atTop T]  refine fun _ hTU ↦ hf.vanishesOnRectangle fun _ ↦ ?_  rw [mem_Rect (by simp [hσ]) (by simp [hTU])]  simpa using by tauto