Source indexedtheorem · leanprover/lean4:v4.32.0

ResidueTheoremInRectangle

PrimeNumberTheoremAnd.ResidueCalcOnRectangles · PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean:583 to 593

Mathematical statement

Exact Lean statement

theorem ResidueTheoremInRectangle
    (zRe_le_wRe : z.re ≤ w.re) (zIm_le_wIm : z.im ≤ w.im)
    (pInRectInterior : Rectangle z w ∈ 𝓝 p) :
    RectangleIntegral' (fun s => c / (s - p)) z w = c

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem ResidueTheoremInRectangle    (zRe_le_wRe : z.re ≤ w.re) (zIm_le_wIm : z.im ≤ w.im)    (pInRectInterior : Rectangle z w ∈ 𝓝 p) :    RectangleIntegral' (fun s => c / (s - p)) z w = c := by  simp only [rectangle_mem_nhds_iff, uIoo_of_le zRe_le_wRe, uIoo_of_le zIm_le_wIm,    mem_reProdIm, mem_Ioo] at pInRectInterior  rw [RectangleIntegral.translate', RectangleIntegral']  have : 1 / (2 * ↑π * I) * (2 * I * ↑π * c) = c := by    field_simp  rwa [ResidueTheoremAtOrigin']  all_goals simp [*]