Commit 2023-06-30 17:15 9063facc

View on Github →

feat: define composition of an AEEqFun with a (quasi)measure preserving function (#5217)

Estimated changes

Modified Mathlib/MeasureTheory/Function/AEEqFun.lean

added theorem MeasureTheory.AEEqFun.coeFn_compMeasurePreserving

added theorem MeasureTheory.AEEqFun.coeFn_compQuasiMeasurePreserving

added def MeasureTheory.AEEqFun.compMeasurePreserving

added theorem MeasureTheory.AEEqFun.compMeasurePreserving_eq_mk

added theorem MeasureTheory.AEEqFun.compMeasurePreserving_mk

added def MeasureTheory.AEEqFun.compQuasiMeasurePreserving

added theorem MeasureTheory.AEEqFun.compQuasiMeasurePreserving_eq_mk

added theorem MeasureTheory.AEEqFun.compQuasiMeasurePreserving_mk

Modified Mathlib/MeasureTheory/Function/LpSeminorm.lean

added theorem MeasureTheory.AEEqFun.snorm_compMeasurePreserving

added theorem MeasureTheory.Memℒp.comp_measurePreserving

added theorem MeasureTheory.Memℒp.comp_of_map

added theorem MeasureTheory.snorm_comp_measurePreserving

modified theorem MeasureTheory.zero_mem_ℒp'

Modified Mathlib/MeasureTheory/Function/LpSpace.lean

added theorem MeasureTheory.AEEqFun.compMeasurePreserving_mem_Lp

added theorem MeasureTheory.Lp.coeFn_compMeasurePreserving

added def MeasureTheory.Lp.compMeasurePreserving

added theorem MeasureTheory.Lp.compMeasurePreserving_val

added def MeasureTheory.Lp.compMeasurePreservingₗ

added def MeasureTheory.Lp.compMeasurePreservingₗᵢ

added theorem MeasureTheory.Lp.norm_compMeasurePreserving