Source indexedlemma · leanprover/lean4:v4.32.0

Perron.contourPull

PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:717 to 726

Mathematical statement

Exact Lean statement

lemma contourPull {σ' σ'' : ℝ} (xpos : 0 < x) (hσ0 : 0 ∉ [[σ', σ'']])
    (hσ1 : -1 ∉ [[σ', σ'']]) :
    VerticalIntegral (f x) σ' = VerticalIntegral (f x) σ''

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma contourPull {σ' σ'' : ℝ} (xpos : 0 < x) (hσ0 : 0 ∉ [[σ', σ'']])    (hσ1 : -1 ∉ [[σ', σ'']]) :    VerticalIntegral (f x) σ' = VerticalIntegral (f x) σ'' := by  refine verticalIntegral_eq_verticalIntegral ((isHolomorphicOn xpos).mono ?_)    (tendsto_zero_Lower xpos σ' σ'') (tendsto_zero_Upper xpos σ' σ'')    (isIntegrable xpos (fun h ↦ hσ0 (h ▸ left_mem_uIcc))      (fun h ↦ hσ1 (h ▸ left_mem_uIcc)))    (isIntegrable xpos (fun h ↦ hσ0 (h ▸ right_mem_uIcc))      (fun h ↦ hσ1 (h ▸ right_mem_uIcc)))  rintro ⟨x, y⟩ ⟨hx, hy⟩ ⟨hc | hc⟩ <;> simp_all [Complex.ext_iff]