Commit 2023-06-08 05:08 62217985

View on Github →

feat: port MeasureTheory.Integral.DivergenceTheorem (#4814)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Integral/DivergenceTheorem.lean

added theorem MeasureTheory.integral2_divergence_prod_of_hasFDerivWithinAt_off_countable

added theorem MeasureTheory.integral_divergence_of_hasFDerivWithinAt_off_countable'

added theorem MeasureTheory.integral_divergence_of_hasFDerivWithinAt_off_countable

added theorem MeasureTheory.integral_divergence_of_hasFDerivWithinAt_off_countable_aux₁

added theorem MeasureTheory.integral_divergence_of_hasFDerivWithinAt_off_countable_aux₂

added theorem MeasureTheory.integral_divergence_of_hasFDerivWithinAt_off_countable_of_equiv

added theorem MeasureTheory.integral_divergence_prod_Icc_of_hasFDerivWithinAt_off_countable_of_le

added theorem MeasureTheory.integral_eq_of_hasDerivWithinAt_off_countable_of_le

added theorem MeasureTheory.integral_eq_of_has_deriv_within_at_off_countable