Commit 2020-06-17 19:10 48c4f400

View on Github →

refactor(measure_theory): make volume a bundled measure (#3075) This way we can apply and rw lemmas about measures without introducing a volume-specific version.

Estimated changes

Modified src/data/set/disjointed.lean

added theorem pairwise.pairwise_on

added theorem set.pairwise_on.on_injective

Modified src/measure_theory/ae_eq_fun.lean

Modified src/measure_theory/bochner_integration.lean

Modified src/measure_theory/giry_monad.lean

Modified src/measure_theory/integration.lean

modified theorem measure_theory.measure.integral_zero

Modified src/measure_theory/l1_space.lean

Modified src/measure_theory/lebesgue_measure.lean

Modified src/measure_theory/measure_space.lean

added theorem measure_theory.ae_all_iff

added theorem measure_theory.ae_eq_refl

added theorem measure_theory.ae_eq_symm

added theorem measure_theory.ae_eq_trans

added theorem measure_theory.ae_iff

added theorem measure_theory.ae_of_all

deleted def measure_theory.all_ae

deleted theorem measure_theory.all_ae_all_iff

deleted theorem measure_theory.all_ae_and_iff

deleted theorem measure_theory.all_ae_congr

deleted theorem measure_theory.all_ae_eq_refl

deleted theorem measure_theory.all_ae_eq_symm

deleted theorem measure_theory.all_ae_eq_trans

deleted theorem measure_theory.all_ae_iff

deleted theorem measure_theory.all_ae_imp_distrib_left

deleted theorem measure_theory.all_ae_of_all

deleted theorem measure_theory.all_ae_or_distrib_left

deleted theorem measure_theory.all_ae_or_distrib_right

added theorem measure_theory.exists_nonempty_inter_of_measure_univ_lt_sum_measure

added theorem measure_theory.exists_nonempty_inter_of_measure_univ_lt_tsum_measure

deleted theorem measure_theory.exists_nonempty_inter_of_volume_univ_lt_sum_volume

deleted theorem measure_theory.exists_nonempty_inter_of_volume_univ_lt_tsum_volume

deleted def measure_theory.measure.a_e

added def measure_theory.measure.ae

deleted theorem measure_theory.measure.mem_a_e_iff

added theorem measure_theory.measure_bUnion_finset

added theorem measure_theory.measure_zero_iff_ae_nmem

added theorem measure_theory.mem_ae_iff

added theorem measure_theory.sum_measure_le_measure_univ

deleted theorem measure_theory.sum_volume_le_volume_univ

added theorem measure_theory.tsum_measure_le_measure_univ

deleted theorem measure_theory.tsum_volume_le_volume_univ

deleted def measure_theory.volume

deleted theorem measure_theory.volume_Union

deleted theorem measure_theory.volume_Union_le

deleted theorem measure_theory.volume_Union_null

deleted theorem measure_theory.volume_bUnion

deleted theorem measure_theory.volume_bUnion_finset

deleted theorem measure_theory.volume_diff

deleted theorem measure_theory.volume_empty

deleted theorem measure_theory.volume_mono

deleted theorem measure_theory.volume_mono_null

deleted theorem measure_theory.volume_sUnion

deleted theorem measure_theory.volume_union

deleted theorem measure_theory.volume_union_le

deleted theorem measure_theory.volume_union_null

deleted theorem measure_theory.volume_zero_iff_all_ae_nmem

Modified src/measure_theory/set_integral.lean

Modified src/measure_theory/simple_func_dense.lean