Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-09-27 15:46
5a2fc855
View on Github →
feat(HaarToSphere): add integrability lemmas (
#24248
)
Estimated changes
Modified
Mathlib/MeasureTheory/Constructions/HaarToSphere.lean
added
theorem
MeasureTheory.Measure.toSphere_eq_zero_iff
added
theorem
MeasureTheory.Measure.toSphere_eq_zero_iff_finrank
added
theorem
MeasureTheory.Measure.toSphere_ne_zero
added
theorem
MeasureTheory.integrable_fun_norm_addHaar
Modified
Mathlib/MeasureTheory/Integral/Prod.lean
added
theorem
MeasureTheory.AEStronglyMeasurable.comp_fst_iff
added
theorem
MeasureTheory.AEStronglyMeasurable.comp_snd_iff
modified
theorem
MeasureTheory.AEStronglyMeasurable.prodMk_left
added
theorem
MeasureTheory.AEStronglyMeasurable.prodMk_right
added
theorem
MeasureTheory.Integrable.comp_fst_iff
added
theorem
MeasureTheory.Integrable.comp_snd_iff
added
theorem
MeasureTheory.Integrable.of_comp_fst
added
theorem
MeasureTheory.Integrable.of_comp_snd