Documentation Verification Report

DomAct

📁 Source: Mathlib/MeasureTheory/Function/AEEqFun/DomAct.lean

Statistics

Metric	Count
Definitions `instAddActionAEEqFun`, `instVAddAEEqFun`, `instDistribMulActionAEEqFun`, `instDistribSMulAEEqFun`, `instMulActionAEEqFun`, `instMulDistribMulActionAEEqFun`, `instSMulAEEqFun`, `instSMulZeroClassAEEqFun`	8
Theorems `instVAddCommClassAEEqFun_2`, `mk_vadd_mk_aeeqFun`, `vadd_aeeqFun_aeeq`, `vadd_aeeqFun_const`, `instSMulCommClassAEEqFun`, `instSMulCommClassAEEqFun_1`, `instSMulCommClassAEEqFun_2`, `mk_smul_mk_aeeqFun`, `smul_aeeqFun_aeeq`, `smul_aeeqFun_const`	10
Total	18

DomAddAct

Definitions

Name	Category	Theorems
`instAddActionAEEqFun` 📖	CompOp	—
`instVAddAEEqFun` 📖	CompOp	5 math math: `instVAddCommClassAEEqFun_2`, `vadd_aeeqFun_const`, `vadd_aeeqFun_aeeq`, `mk_vadd_mk_aeeqFun`, `vadd_Lp_val`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instVAddCommClassAEEqFun_2` 📖	mathematical	—	`VAddCommClass` `DomAddAct` `MeasureTheory.AEEqFun` `instVAddAEEqFun`	—	`Function.Surjective.forall` `Equiv.surjective` `MeasureTheory.AEEqFun.induction_on` `MeasureTheory.AEStronglyMeasurable.comp_measurePreserving` `MeasureTheory.measurePreserving_vadd` `VAddCommClass.vadd_comm`
`mk_vadd_mk_aeeqFun` 📖	mathematical	`MeasureTheory.AEStronglyMeasurable`	`HVAdd.hVAdd` `DomAddAct` `MeasureTheory.AEEqFun` `instHVAdd` `instVAddAEEqFun` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `MeasureTheory.AEStronglyMeasurable.comp_measurePreserving` `MeasureTheory.measurePreserving_vadd`	—	—
`vadd_aeeqFun_aeeq` 📖	mathematical	—	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.AEEqFun.cast` `HVAdd.hVAdd` `DomAddAct` `MeasureTheory.AEEqFun` `instHVAdd` `instVAddAEEqFun` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm`	—	`MeasureTheory.AEEqFun.coeFn_compMeasurePreserving`
`vadd_aeeqFun_const` 📖	mathematical	—	`HVAdd.hVAdd` `DomAddAct` `MeasureTheory.AEEqFun` `instHVAdd` `instVAddAEEqFun` `MeasureTheory.AEEqFun.const`	—	—

DomMulAct

Definitions

Name	Category	Theorems
`instDistribMulActionAEEqFun` 📖	CompOp	—
`instDistribSMulAEEqFun` 📖	CompOp	—
`instMulActionAEEqFun` 📖	CompOp	—
`instMulDistribMulActionAEEqFun` 📖	CompOp	—
`instSMulAEEqFun` 📖	CompOp	7 math math: `smul_aeeqFun_aeeq`, `instSMulCommClassAEEqFun_2`, `instSMulCommClassAEEqFun_1`, `smul_aeeqFun_const`, `instSMulCommClassAEEqFun`, `smul_Lp_val`, `mk_smul_mk_aeeqFun`
`instSMulZeroClassAEEqFun` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instSMulCommClassAEEqFun` 📖	mathematical	—	`SMulCommClass` `DomMulAct` `MeasureTheory.AEEqFun` `instSMulAEEqFun` `MeasureTheory.AEEqFun.instSMul`	—	—
`instSMulCommClassAEEqFun_1` 📖	mathematical	—	`SMulCommClass` `DomMulAct` `MeasureTheory.AEEqFun` `MeasureTheory.AEEqFun.instSMul` `instSMulAEEqFun`	—	`SMulCommClass.symm` `instSMulCommClassAEEqFun`
`instSMulCommClassAEEqFun_2` 📖	mathematical	—	`SMulCommClass` `DomMulAct` `MeasureTheory.AEEqFun` `instSMulAEEqFun`	—	`Function.Surjective.forall` `Equiv.surjective` `MeasureTheory.AEEqFun.induction_on` `MeasureTheory.AEStronglyMeasurable.comp_measurePreserving` `MeasureTheory.measurePreserving_smul` `SMulCommClass.smul_comm`
`mk_smul_mk_aeeqFun` 📖	mathematical	`MeasureTheory.AEStronglyMeasurable`	`DomMulAct` `MeasureTheory.AEEqFun` `instSMulAEEqFun` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `MeasureTheory.AEStronglyMeasurable.comp_measurePreserving` `MeasureTheory.measurePreserving_smul`	—	—
`smul_aeeqFun_aeeq` 📖	mathematical	—	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.AEEqFun.cast` `DomMulAct` `MeasureTheory.AEEqFun` `instSMulAEEqFun` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm`	—	`MeasureTheory.AEEqFun.coeFn_compMeasurePreserving`
`smul_aeeqFun_const` 📖	mathematical	—	`DomMulAct` `MeasureTheory.AEEqFun` `instSMulAEEqFun` `MeasureTheory.AEEqFun.const`	—	—

---

← Back to Index