Source indexedlemma · leanprover/lean4:v4.32.0

integral_self_div_sq_add_sq

PrimeNumberTheoremAnd.ResidueCalcOnRectangles · PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean:497 to 508

Mathematical statement

Exact Lean statement

lemma integral_self_div_sq_add_sq (hy : y ≠ 0) :
    ∫ x in x₁..x₂, x / (x ^ 2 + y ^ 2) =
    Real.log (x₂ ^ 2 + y ^ 2) / 2 - Real.log (x₁ ^ 2 + y ^ 2) / 2

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma integral_self_div_sq_add_sq (hy : y ≠ 0) :    ∫ x in x₁..x₂, x / (x ^ 2 + y ^ 2) =    Real.log (x₂ ^ 2 + y ^ 2) / 2 - Real.log (x₁ ^ 2 + y ^ 2) / 2 := by  let f (x : ℝ) : ℝ := Real.log (x ^ 2 + y ^ 2) / 2  have e1 {x} := HasDerivAt.add_const (y ^ 2) (by simpa using hasDerivAt_pow 2 x)  have e2 {x} : HasDerivAt f (x / (x ^ 2 + y ^ 2)) x := by    convert! (e1.log (sq_add_sq_ne_zero hy)).div_const 2 using 1    field_simp  have e3 : deriv f = fun x => x / (x ^ 2 + y ^ 2) := funext (fun _ => e2.deriv)  have e4 : Continuous (deriv f) := by simpa only [e3] using continuous_self_div_sq_add_sq hy  simp_rw [← e2.deriv]  exact integral_deriv_eq_sub (fun _ _ => e2.differentiableAt) (e4.intervalIntegrable _ _)