Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-30 10:07 8069521e

View on Github →

feat(measure_theory): Absolute continuity (#5948)

Define absolute continuity between measures (@mzinkevi)
State monotonicity of ae_measurable w.r.t. absolute continuity
Weaken some measurable assumptions in prod.lean to ae_measurable
Some docstring fixes
Some cleanup

Estimated changes

Modified src/measure_theory/borel_space.lean

Modified src/measure_theory/group.lean

Modified src/measure_theory/haar_measure.lean

Modified src/measure_theory/integration.lean

Modified src/measure_theory/measure_space.lean

added theorem ae_measurable.comp_measurable'

added theorem measure_theory.ae_eq_comp'

added theorem measure_theory.measure.absolutely_continuous.mk

added theorem measure_theory.measure.absolutely_continuous.refl

added theorem measure_theory.measure.absolutely_continuous.rfl

added theorem measure_theory.measure.absolutely_continuous.trans

added def measure_theory.measure.absolutely_continuous

added theorem measure_theory.measure.absolutely_continuous_of_eq

added theorem measure_theory.measure.preimage_null_of_map_null

modified def measure_theory.to_measurable

Modified src/measure_theory/prod.lean

added theorem ae_measurable.fst

modified theorem ae_measurable.prod_swap

added theorem ae_measurable.snd

deleted theorem measure_theory.lintegral_prod'

modified theorem measure_theory.lintegral_prod

modified theorem measure_theory.lintegral_prod_mul

added theorem measure_theory.lintegral_prod_of_measurable

added theorem measure_theory.measure.prod_fst_absolutely_continuous

added theorem measure_theory.measure.prod_snd_absolutely_continuous

Modified src/measure_theory/prod_group.lean

Modified src/topology/subset_properties.lean

modified theorem compact_pi_infinite

modified theorem compact_univ_pi