Commit 2025-04-11 19:15 95542e06

View on Github →

feat: μ.real as the real-valued version of a measure (#23943) We port some API of measures to their real-valued versions. Upstreamed from PFR and Carleson

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

added theorem MeasureTheory.measure_diff_eq_top

added theorem MeasureTheory.measure_symmDiff_eq_top

added theorem MeasureTheory.sum_measure_singleton

Modified Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean

added theorem MeasureTheory.measure_ne_top_of_subset

Created Mathlib/MeasureTheory/Measure/Real.lean

added def Mathlib.Meta.Positivity.evalMeasureReal

added theorem MeasureTheory.Finset.sum_realMeasure_singleton

added theorem MeasureTheory.exists_nonempty_inter_of_measureReal_univ_lt_sum_measureReal

added theorem MeasureTheory.ext_iff_measureReal_singleton

added theorem MeasureTheory.le_measureReal_diff

added theorem MeasureTheory.map_measureReal_apply

added theorem MeasureTheory.measureReal_add_diff

added theorem MeasureTheory.measureReal_add_measureReal_compl

added theorem MeasureTheory.measureReal_add_measureReal_compl₀

added theorem MeasureTheory.measureReal_biUnion_finset

added theorem MeasureTheory.measureReal_biUnion_finset_le

added theorem MeasureTheory.measureReal_biUnion_finset₀

added theorem MeasureTheory.measureReal_compl

added theorem MeasureTheory.measureReal_congr

added theorem MeasureTheory.measureReal_def

added theorem MeasureTheory.measureReal_diff'

added theorem MeasureTheory.measureReal_diff

added theorem MeasureTheory.measureReal_diff_add_inter

added theorem MeasureTheory.measureReal_diff_le_iff_le_add

added theorem MeasureTheory.measureReal_diff_lt_of_lt_add

added theorem MeasureTheory.measureReal_diff_null'

added theorem MeasureTheory.measureReal_diff_null

added theorem MeasureTheory.measureReal_empty

added theorem MeasureTheory.measureReal_ennreal_smul_apply

added theorem MeasureTheory.measureReal_eq_measureReal_larger_of_between_null_diff

added theorem MeasureTheory.measureReal_eq_measureReal_of_between_null_diff

added theorem MeasureTheory.measureReal_eq_measureReal_of_null_diff

added theorem MeasureTheory.measureReal_eq_measureReal_smaller_of_between_null_diff

added theorem MeasureTheory.measureReal_eq_zero_iff

added theorem MeasureTheory.measureReal_iUnion_fintype

added theorem MeasureTheory.measureReal_iUnion_fintype_le

added theorem MeasureTheory.measureReal_inter_add_diff

added theorem MeasureTheory.measureReal_inter_add_diff₀

added theorem MeasureTheory.measureReal_le_measureReal_union_left

added theorem MeasureTheory.measureReal_le_measureReal_union_right

added theorem MeasureTheory.measureReal_mono

added theorem MeasureTheory.measureReal_mono_null

added theorem MeasureTheory.measureReal_nnreal_smul_apply

added theorem MeasureTheory.measureReal_nonneg

added theorem MeasureTheory.measureReal_prod_prod

added theorem MeasureTheory.measureReal_symmDiff_eq

added theorem MeasureTheory.measureReal_symmDiff_le

added theorem MeasureTheory.measureReal_union'

added theorem MeasureTheory.measureReal_union

added theorem MeasureTheory.measureReal_union_add_inter'

added theorem MeasureTheory.measureReal_union_add_inter

added theorem MeasureTheory.measureReal_union_add_inter₀'

added theorem MeasureTheory.measureReal_union_add_inter₀

added theorem MeasureTheory.measureReal_union_congr_of_subset

added theorem MeasureTheory.measureReal_union_le

added theorem MeasureTheory.measureReal_union_null

added theorem MeasureTheory.measureReal_union_null_iff

added theorem MeasureTheory.measureReal_union₀'

added theorem MeasureTheory.measureReal_union₀

added theorem MeasureTheory.measureReal_univ_eq_one

added theorem MeasureTheory.measureReal_univ_ne_zero

added theorem MeasureTheory.measureReal_univ_pos

added theorem MeasureTheory.measureReal_zero

added theorem MeasureTheory.measureReal_zero_apply

added theorem MeasureTheory.nonempty_inter_of_measureReal_lt_add'

added theorem MeasureTheory.nonempty_inter_of_measureReal_lt_add

added theorem MeasureTheory.nonempty_of_measureReal_ne_zero

added theorem MeasureTheory.sum_measureReal_le_measureReal_univ

added theorem MeasureTheory.sum_measureReal_preimage_singleton

Modified scripts/noshake.json