Commit 2021-08-24 21:23 6c3dda5c

View on Github →

feat(measure_theory/measure/vector_measure): add absolute continuity for vector measures (#8779) This PR defines absolute continuity for vector measures and shows that a signed measure is absolutely continuous wrt to a positive measure iff its total variation is absolutely continuous wrt to that measure.

Estimated changes

Modified src/measure_theory/decomposition/jordan.lean

added theorem measure_theory.signed_measure.absolutely_continuous_iff

added def measure_theory.signed_measure.total_variation

added theorem measure_theory.signed_measure.total_variation_absolutely_continuous_iff

added theorem measure_theory.signed_measure.total_variation_neg

added theorem measure_theory.signed_measure.total_variation_zero

Modified src/measure_theory/measure/vector_measure.lean

added theorem measure_theory.vector_measure.absolutely_continuous.ennreal_to_measure

added theorem measure_theory.vector_measure.absolutely_continuous.eq

added theorem measure_theory.vector_measure.absolutely_continuous.map

added theorem measure_theory.vector_measure.absolutely_continuous.mk

added theorem measure_theory.vector_measure.absolutely_continuous.refl

added theorem measure_theory.vector_measure.absolutely_continuous.trans

added def measure_theory.vector_measure.absolutely_continuous

added def measure_theory.vector_measure.ennreal_to_measure

added theorem measure_theory.vector_measure.ennreal_to_measure_apply

added def measure_theory.vector_measure.equiv_measure

added theorem measure_theory.vector_measure.map_not_measurable