Commit 2023-07-31 19:47 31d6c54a

View on Github →

feat(MeasureTheory): define DomMulAct action on Lp (#6190)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Function/AEEqFun/DomAct.lean

added theorem DomMulAct.smul_aeeqFun_const

Modified Mathlib/MeasureTheory/Function/LpSpace.lean

Created Mathlib/MeasureTheory/Function/LpSpace/DomAct/Basic.lean

added theorem DomMulAct.dist_smul_Lp

added theorem DomMulAct.edist_smul_Lp

added theorem DomMulAct.mk_smul_toLp

added theorem DomMulAct.nnnorm_smul_Lp

added theorem DomMulAct.norm_smul_Lp

added theorem DomMulAct.smul_Lp_add

added theorem DomMulAct.smul_Lp_ae_eq

added theorem DomMulAct.smul_Lp_const

added theorem DomMulAct.smul_Lp_neg

added theorem DomMulAct.smul_Lp_sub

added theorem DomMulAct.smul_Lp_val

added theorem DomMulAct.smul_Lp_zero

Modified Mathlib/MeasureTheory/Group/Integration.lean