Commit 2024-02-16 01:59 6ec9e85b

View on Github →

feat: improper integrals of 1/(1 + x^2) (#10234)

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean

added theorem integrable_inv_one_add_sq

added theorem integral_Iic_inv_one_add_sq

added theorem integral_Ioi_inv_one_add_sq

added theorem integral_univ_inv_one_add_sq

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean

added theorem Real.arctan_eq_zero_iff

added theorem Real.arctan_injective

added theorem Real.arctan_strictMono

added theorem Real.tendsto_arctan_atBot

added theorem Real.tendsto_arctan_atTop

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/ArctanDeriv.lean

added theorem Real.hasDerivAt_arctan'

Modified Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean

added theorem MeasureTheory.integral_of_hasDerivAt_of_tendsto

Modified test/RewriteSearch/Polynomial.lean