Commit 2025-09-23 13:41 e02195e6

View on Github →

chore(MeasureTheory): semilinearize composition of integrals with CLM (#29853)

Estimated changes

Modified Mathlib/MeasureTheory/Function/LpSpace/Basic.lean

modified theorem ContinuousLinearMap.add_compLp

modified theorem ContinuousLinearMap.add_compLpL

modified theorem ContinuousLinearMap.coeFn_compLp'

modified theorem ContinuousLinearMap.coeFn_compLp

modified theorem ContinuousLinearMap.coeFn_compLpL

modified def ContinuousLinearMap.compLp

modified def ContinuousLinearMap.compLpL

modified def ContinuousLinearMap.compLpₗ

modified theorem ContinuousLinearMap.comp_memLp'

modified theorem ContinuousLinearMap.comp_memLp

modified theorem ContinuousLinearMap.norm_compLpL_le

modified theorem ContinuousLinearMap.norm_compLp_le

modified theorem ContinuousLinearMap.smul_compLp

modified theorem ContinuousLinearMap.smul_compLpL

Modified Mathlib/MeasureTheory/Integral/Bochner/ContinuousLinearMap.lean

modified theorem ContinuousLinearMap.continuous_integral_comp_L1

modified theorem ContinuousLinearMap.integral_compLp

modified theorem ContinuousLinearMap.integral_comp_L1_comm

modified theorem ContinuousLinearMap.integral_comp_comm'

modified theorem ContinuousLinearMap.integral_comp_comm

added theorem ContinuousLinearMap.integral_comp_commSL

modified theorem ContinuousLinearMap.setIntegral_compLp