Commit 2021-11-08 08:27 62f94ad6

View on Github →

feat(measure_theory/measurable_space): define measurable_embedding (#10023) This way we can generalize our theorems about measurable_equiv and closed_embeddings.

Estimated changes

Modified src/data/set/function.lean

added theorem set.range_extend

added theorem set.range_extend_subset

Modified src/measure_theory/constructions/borel_space.lean

deleted theorem ae_measurable_comp_iff_of_closed_embedding

deleted theorem ae_measurable_comp_right_iff_of_closed_embedding

deleted theorem closed_embedding.measurable_inv_fun

deleted theorem measurable_comp_iff_of_closed_embedding

Modified src/measure_theory/function/l1_space.lean

added theorem measurable_embedding.integrable_map_iff

Modified src/measure_theory/function/lp_space.lean

Modified src/measure_theory/integral/bochner.lean

added theorem closed_embedding.integral_map

added theorem measurable_embedding.integral_map

deleted theorem measure_theory.integral_map_of_closed_embedding

Modified src/measure_theory/integral/integrable_on.lean

added theorem measurable_embedding.integrable_on_map_iff

Modified src/measure_theory/integral/interval_integral.lean

Modified src/measure_theory/integral/lebesgue.lean

added theorem measurable_embedding.lintegral_map

added def measure_theory.simple_func.extend

added theorem measure_theory.simple_func.extend_apply

added theorem measure_theory.simple_func.extend_comp_eq'

added theorem measure_theory.simple_func.extend_comp_eq

added theorem measure_theory.simple_func.lintegral_map'

modified theorem measure_theory.simple_func.lintegral_map

deleted theorem measure_theory.simple_func.lintegral_map_equiv

Modified src/measure_theory/integral/set_integral.lean

added theorem closed_embedding.set_integral_map

added theorem measurable_embedding.set_integral_map

deleted theorem measure_theory.set_integral_map_of_closed_embedding

Modified src/measure_theory/measurable_space.lean

added theorem measurable.dite

added theorem measurable_embedding.comp

added theorem measurable_embedding.exists_measurable_extend

added theorem measurable_embedding.id

added theorem measurable_embedding.measurable_comp_iff

added theorem measurable_embedding.measurable_extend

added theorem measurable_embedding.measurable_range_splitting

added theorem measurable_embedding.measurable_set_image

added theorem measurable_embedding.measurable_set_preimage

added theorem measurable_embedding.measurable_set_range

added theorem measurable_embedding.of_measurable_inverse

added theorem measurable_embedding.of_measurable_inverse_on_range

added theorem measurable_embedding.subtype_coe

added structure measurable_embedding

added theorem measurable_equiv.image_eq_preimage

added theorem measurable_equiv.measurable_set_image

added theorem measurable_equiv.measurable_set_preimage

added theorem measurable_equiv.symm_preimage_preimage

added theorem measurable_of_restrict_of_restrict_compl

added theorem measurable_set.exists_measurable_proj

Modified src/measure_theory/measure/measure_space.lean

added theorem ae_measurable.subtype_mk

added theorem ae_measurable_restrict_iff_comap_subtype

added theorem ae_restrict_iff_subtype

added theorem comap_subtype_coe_apply

added theorem map_comap_subtype_coe

added theorem measurable_embedding.ae_map_iff

added theorem measurable_embedding.ae_measurable_comp_iff

added theorem measurable_embedding.ae_measurable_map_iff

added theorem measurable_embedding.comap_apply

added theorem measurable_embedding.map_apply

added theorem measurable_embedding.map_comap

added theorem measurable_embedding.restrict_map

added theorem measurable_set.map_coe_volume

deleted theorem measure_theory.measure.map_comap_subtype_coe

added theorem volume_image_subtype_coe

added theorem volume_set_coe_def