Commit 2021-09-19 17:47 965e457f

View on Github →

feat(measure_theory/measure/lebesgue): a linear map rescales Lebesgue by the inverse of its determinant (#9195) Also supporting material to be able to apply Fubini in ι → ℝ by separating some coordinates.

Estimated changes

Modified src/algebra/big_operators/basic.lean

added theorem fintype.prod_subtype_mul_prod_subtype

Modified src/data/equiv/basic.lean

added def equiv.pi_equiv_pi_subtype_prod

Modified src/measure_theory/constructions/pi.lean

added theorem measure_theory.measure.map_pi_equiv_pi_subtype_prod

added theorem measure_theory.measure.map_pi_equiv_pi_subtype_prod_symm

Modified src/measure_theory/constructions/prod.lean

added theorem measure_theory.measure.volume_eq_prod

Modified src/measure_theory/measurable_space.lean

added theorem measurable_pi_equiv_pi_subtype_prod

added theorem measurable_pi_equiv_pi_subtype_prod_symm

Modified src/measure_theory/measure/lebesgue.lean

added theorem real.map_linear_map_volume_pi_eq_smul_volume_pi

added theorem real.map_matrix_volume_pi_eq_smul_volume_pi

added theorem real.map_transvection_volume_pi

added theorem real.map_volume_pi_add_left

added theorem real.smul_map_diagonal_volume_pi

added theorem real.volume_pi_preimage_add_left

added theorem real.volume_preimage_add_left

added theorem real.volume_preimage_add_right

added theorem real.volume_preimage_mul_left

added theorem real.volume_preimage_mul_right