Source indexedlemma · leanprover/lean4:v4.32.0

verticalIntegral_eq_verticalIntegral

PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:67 to 77

Mathematical statement

Exact Lean statement

lemma verticalIntegral_eq_verticalIntegral {σ σ' : ℝ} {f : ℂ → ℂ}
    (hf : HolomorphicOn f ([[σ, σ']] ×ℂ univ))
    (hbot : Tendsto (fun (y : ℝ) ↦ ∫ (x : ℝ) in σ..σ', f (x + y * I)) atBot (𝓝 0))
    (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))) :
    VerticalIntegral f σ = VerticalIntegral f σ'

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma verticalIntegral_eq_verticalIntegral {σ σ' : ℝ} {f : ℂ → ℂ}    (hf : HolomorphicOn f ([[σ, σ']] ×ℂ univ))    (hbot : Tendsto (fun (y : ℝ) ↦ ∫ (x : ℝ) in σ..σ', f (x + y * I)) atBot (𝓝 0))    (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))) :    VerticalIntegral f σ = VerticalIntegral f σ' := by  refine zeroTendstoDiff _ _ _ (univ_mem' fun _ ↦ ?_)    (RectangleIntegral_tendsTo_VerticalIntegral hbot htop hleft hright)  exact integral_boundary_rect_eq_zero_of_differentiableOn f _ _    (hf.mono fun z hrect ↦ ⟨by simpa using hrect.1, trivial⟩)