Commit 2023-06-20 11:14 08173634

View on Github →

feat: port Analysis.BoundedVariation (#4824) This PR also corrects a mis-forward-port of leanprover-community/mathlib#18080

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/Basic.lean

modified theorem multiplicative_of_isTotal

Created Mathlib/Analysis/BoundedVariation.lean

added theorem BoundedVariationOn.dist_le

added theorem BoundedVariationOn.locallyBoundedVariationOn

added theorem BoundedVariationOn.mono

added theorem BoundedVariationOn.sub_le

added def BoundedVariationOn

added theorem LipschitzOnWith.ae_differentiableWithinAt

added theorem LipschitzOnWith.ae_differentiableWithinAt_of_mem

added theorem LipschitzOnWith.comp_boundedVariationOn

added theorem LipschitzOnWith.comp_eVariationOn_le

added theorem LipschitzOnWith.comp_locallyBoundedVariationOn

added theorem LipschitzOnWith.locallyBoundedVariationOn

added theorem LipschitzWith.ae_differentiableAt

added theorem LipschitzWith.comp_boundedVariationOn

added theorem LipschitzWith.comp_locallyBoundedVariationOn

added theorem LipschitzWith.locallyBoundedVariationOn

added theorem LocallyBoundedVariationOn.ae_differentiableAt

added theorem LocallyBoundedVariationOn.ae_differentiableWithinAt

added theorem LocallyBoundedVariationOn.ae_differentiableWithinAt_of_mem

added theorem LocallyBoundedVariationOn.ae_differentiableWithinAt_of_mem_pi

added theorem LocallyBoundedVariationOn.ae_differentiableWithinAt_of_mem_real

added theorem LocallyBoundedVariationOn.exists_monotoneOn_sub_monotoneOn

added def LocallyBoundedVariationOn

added theorem MonotoneOn.eVariationOn_le

added theorem MonotoneOn.locallyBoundedVariationOn

added theorem Set.subsingleton_Icc_of_ge

added theorem eVariationOn.Icc_add_Icc

added theorem eVariationOn.add_le_union

added theorem eVariationOn.add_point

added theorem eVariationOn.comp_eq_of_antitoneOn

added theorem eVariationOn.comp_eq_of_monotoneOn

added theorem eVariationOn.comp_inter_Icc_eq_of_monotoneOn

added theorem eVariationOn.comp_le_of_antitoneOn

added theorem eVariationOn.comp_le_of_monotoneOn

added theorem eVariationOn.comp_ofDual

added theorem eVariationOn.constant_on

added theorem eVariationOn.edist_le

added theorem eVariationOn.eq_of_edist_zero_on

added theorem eVariationOn.eq_of_eqOn

added theorem eVariationOn.eq_zero_iff

added theorem eVariationOn.lowerSemicontinuous_aux

added theorem eVariationOn.lowerSemicontinuous_uniformOn

added theorem eVariationOn.mono

added theorem eVariationOn.nonempty_monotone_mem

added theorem eVariationOn.sum_le

added theorem eVariationOn.sum_le_of_monotoneOn_Icc

added theorem eVariationOn.sum_le_of_monotoneOn_Iic

added theorem eVariationOn.union