Commit 2023-06-05 20:26 b895b189

View on Github →

feat: port MeasureTheory.Measure.Haar.NormedSpace (#4704)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Measure/Haar/NormedSpace.lean

added theorem MeasureTheory.Integrable.comp_div

added theorem MeasureTheory.Integrable.comp_mul_left'

added theorem MeasureTheory.Integrable.comp_mul_right'

added theorem MeasureTheory.Integrable.comp_smul

added theorem MeasureTheory.Measure.integral_comp_div

added theorem MeasureTheory.Measure.integral_comp_inv_mul_left

added theorem MeasureTheory.Measure.integral_comp_inv_mul_right

added theorem MeasureTheory.Measure.integral_comp_inv_smul

added theorem MeasureTheory.Measure.integral_comp_inv_smul_of_nonneg

added theorem MeasureTheory.Measure.integral_comp_mul_left

added theorem MeasureTheory.Measure.integral_comp_mul_right

added theorem MeasureTheory.Measure.integral_comp_smul

added theorem MeasureTheory.Measure.integral_comp_smul_of_nonneg

added theorem MeasureTheory.integrable_comp_div_iff

added theorem MeasureTheory.integrable_comp_mul_left_iff

added theorem MeasureTheory.integrable_comp_mul_right_iff

added theorem MeasureTheory.integrable_comp_smul_iff