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