Source indexedtheorem · leanprover/lean4:v4.32.0

Perron.HolomorphicOn.lowerUIntegral_eq_zero

PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:793 to 805

Mathematical statement

Exact Lean statement

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

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem HolomorphicOn.lowerUIntegral_eq_zero {f : ℂ → ℂ} {σ σ' T : ℝ} (hσ : σ ≤ σ')    (hf : HolomorphicOn f {z : ℂ | σ ≤ z.re ∧ z.re ≤ σ' ∧ z.im ≤ -T})    (hbot : Tendsto (fun (y : ℝ) ↦ ∫ (x : ℝ) in σ..σ', f (x + y * I)) atBot (𝓝 0))    (hleft : Integrable fun y : ℝ ↦ f (↑σ + ↑y * I))    (hright : Integrable fun y : ℝ ↦ f (↑σ' + ↑y * I)) :    LowerUIntegral f σ σ' T = 0 := by  suffices h : - LowerUIntegral f σ σ' T = 0 by exact neg_eq_zero.mp h  apply tendsto_nhds_unique (RectangleIntegral_tendsTo_LowerU hbot 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