Commit 2023-10-30 20:20 4ad9d1eb

View on Github →

feat: additional version of FTC-2 for improper integrals (#7755)

The extra import doesn't import any additional files transitively.
From the Sobolev project

Estimated changes

Modified Mathlib/Analysis/Calculus/Deriv/Support.lean

deleted theorem HasCompactSupport.deriv

Modified Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean

added theorem MeasureTheory.HasCompactSupport.integral_Iic_deriv_eq

added theorem MeasureTheory.HasCompactSupport.integral_Ioi_deriv_eq

modified theorem MeasureTheory.integrableOn_Ioi_deriv_of_nonneg

modified theorem MeasureTheory.integrableOn_Ioi_deriv_of_nonpos

added theorem MeasureTheory.integral_Iic_of_hasDerivAt_of_tendsto'

added theorem MeasureTheory.integral_Iic_of_hasDerivAt_of_tendsto

modified theorem MeasureTheory.integral_Ioi_of_hasDerivAt_of_nonneg

modified theorem MeasureTheory.integral_Ioi_of_hasDerivAt_of_nonpos

modified theorem MeasureTheory.integral_Ioi_of_hasDerivAt_of_tendsto

Modified Mathlib/Topology/Basic.lean

added theorem Filter.EventuallyEq.tendsto

Modified Mathlib/Topology/Instances/Real.lean

added theorem Real.atBot_le_cocompact

added theorem Real.atTop_le_cocompact