Source indexedlemma · leanprover/lean4:v4.32.0

integral_const_div_re_add_self

PrimeNumberTheoremAnd.ResidueCalcOnRectangles · PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean:543 to 559

Mathematical statement

Exact Lean statement

lemma integral_const_div_re_add_self (hx : x ≠ 0) :
    ∫ y : ℝ in y₁..y₂, A / (x + y * I) =
    A / I * (Real.log (y₂ ^ 2 + (-x) ^ 2) / 2 - Real.log (y₁ ^ 2 + (-x) ^ 2) / 2) -
    A / I * I * (arctan (y₂ / -x) - arctan (y₁ / -x))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma integral_const_div_re_add_self (hx : x ≠ 0) :    ∫ y : ℝ in y₁..y₂, A / (x + y * I) =    A / I * (Real.log (y₂ ^ 2 + (-x) ^ 2) / 2 - Real.log (y₁ ^ 2 + (-x) ^ 2) / 2) -    A / I * I * (arctan (y₂ / -x) - arctan (y₁ / -x)) := by  have l1 {y : ℝ} : A / (x + y * I) = A / I / (y + ↑(-x) * I) := by    have e1 : x + y * I ≠ 0 := by      contrapose! hx      simpa using congr_arg re hx    have e2 : y + I * ↑(-x) ≠ 0 := by      contrapose! hx      simpa using congr_arg im hx    field_simp [*]    push_cast    ring_nf    simp  have l2 : -x ≠ 0 := by rwa [neg_ne_zero]  simp_rw [l1, integral_const_div_self_add_im l2]