Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-02 10:49 09fb38cc

View on Github →

chore(analysis/box_integral): use GP instead of bot (#15939) This is how this integral is called in the original paper.

Estimated changes

Modified src/analysis/box_integral/divergence_theorem.lean

added theorem box_integral.has_integral_GP_divergence_of_forall_has_deriv_within_at

added theorem box_integral.has_integral_GP_pderiv

deleted theorem box_integral.has_integral_bot_divergence_of_forall_has_deriv_within_at

deleted theorem box_integral.has_integral_bot_pderiv

Modified src/analysis/box_integral/partition/filter.lean

added def box_integral.integration_params.GP

added theorem box_integral.integration_params.GP_le

Modified src/measure_theory/integral/divergence_theorem.lean