AEMeasurable

📁 Source: Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean

Statistics

Metric	Count
Definitions lpMeas, lpMeasSubgroup, lpMeasSubgroupToLpMeasIso, lpMeasSubgroupToLpTrim, lpMeasSubgroupToLpTrimIso, lpMeasToLpTrim, lpMeasToLpTrimLie, lpTrimToLpMeas, lpTrimToLpMeasSubgroup	9
Theorems comp_ae_measurable', induction_stronglyMeasurable, induction_stronglyMeasurable_aux, induction_stronglyMeasurable, ae_eq_trim_iff_of_aestronglyMeasurable, instCompleteSpaceSubtypeAEEqFunMemAddSubgroupLpLpMeasSubgroupOfFactLeMeasurableSpace, instCompleteSpaceSubtypeAEEqFunMemAddSubgroupLpSubmoduleLpMeasOfFactLeMeasurableSpace, isClosed_aestronglyMeasurable, isComplete_aestronglyMeasurable, isometry_lpMeasSubgroupToLpTrim, ae_fin_strongly_measurable', aestronglyMeasurable, lpMeasSubgroupToLpTrim_add, lpMeasSubgroupToLpTrim_ae_eq, lpMeasSubgroupToLpTrim_left_inv, lpMeasSubgroupToLpTrim_neg, lpMeasSubgroupToLpTrim_norm_map, lpMeasSubgroupToLpTrim_right_inv, lpMeasSubgroupToLpTrim_sub, lpMeasToLpTrimLie_symm_indicator, lpMeasToLpTrimLie_symm_toLp, lpMeasToLpTrim_ae_eq, lpMeasToLpTrim_smul, lpTrimToLpMeasSubgroup_ae_eq, lpTrimToLpMeas_ae_eq, memLp_trim_of_mem_lpMeasSubgroup, mem_lpMeasSubgroup_iff_aestronglyMeasurable, mem_lpMeasSubgroup_toLp_of_trim, mem_lpMeas_iff_aestronglyMeasurable, mem_lpMeas_indicatorConstLp, mem_lpMeas_self	31
Total	40

MeasureTheory

Definitions

Name	Category	Theorems
lpMeas 📖	CompOp	39 math math: norm_condExpL2_le, inner_condExpL2_left_eq_right, condExpL2_ae_eq_zero_of_ae_eq_zero, MemLp.condExpL2_ae_eq_condExp, aestronglyMeasurable_condExpL2, condExpL2_indicator_ae_eq_smul, integral_condExpL2_eq, setIntegral_condExpL2_indicator, lintegral_nnnorm_condExpL2_indicator_le, norm_condExpL2_coe_le, setLIntegral_nnnorm_condExpL2_indicator_le, mem_lpMeas_iff_aestronglyMeasurable, mem_lpMeas_indicatorConstLp, lintegral_nnnorm_condExpL2_le, lpMeasToLpTrimLie_symm_indicator, integral_condExpL2_eq_of_fin_meas_real, condExpL2_indicator_of_measurable, condExpL2_indicator_eq_toSpanSingleton_comp, instCompleteSpaceSubtypeAEEqFunMemAddSubgroupLpSubmoduleLpMeasOfFactLeMeasurableSpace, lintegral_nnnorm_condExpL2_indicator_le_real, condExpL1CLM_lpMeas, integrable_condExpL2_of_isFiniteMeasure, integrable_condExpL2_indicator, MemLp.condExpL2_ae_eq_condExp', lpTrimToLpMeas_ae_eq, inner_condExpL2_eq_inner_fun, mem_lpMeas_self, integrableOn_condExpL2_of_measure_ne_top, lpMeasToLpTrim_ae_eq, eLpNorm_condExpL2_le, lpMeasToLpTrim_smul, condExpIndSMul_ae_eq_smul, lpMeas.ae_fin_strongly_measurable', lpMeasToLpTrimLie_symm_toLp, norm_condExpL2_le_one, condExpL2_comp_continuousLinearMap, condExpL2_const_inner, condExpL2_indicator_nonneg, lpMeas.aestronglyMeasurable
lpMeasSubgroup 📖	CompOp	12 math math: mem_lpMeasSubgroup_iff_aestronglyMeasurable, lpMeasSubgroupToLpTrim_neg, lpMeasSubgroupToLpTrim_ae_eq, lpMeasSubgroupToLpTrim_sub, lpMeasSubgroupToLpTrim_right_inv, mem_lpMeasSubgroup_toLp_of_trim, lpMeasSubgroupToLpTrim_add, lpMeasSubgroupToLpTrim_left_inv, lpMeasSubgroupToLpTrim_norm_map, isometry_lpMeasSubgroupToLpTrim, instCompleteSpaceSubtypeAEEqFunMemAddSubgroupLpLpMeasSubgroupOfFactLeMeasurableSpace, lpTrimToLpMeasSubgroup_ae_eq
lpMeasSubgroupToLpMeasIso 📖	CompOp	—
lpMeasSubgroupToLpTrim 📖	CompOp	8 math math: lpMeasSubgroupToLpTrim_neg, lpMeasSubgroupToLpTrim_ae_eq, lpMeasSubgroupToLpTrim_sub, lpMeasSubgroupToLpTrim_right_inv, lpMeasSubgroupToLpTrim_add, lpMeasSubgroupToLpTrim_left_inv, lpMeasSubgroupToLpTrim_norm_map, isometry_lpMeasSubgroupToLpTrim
lpMeasSubgroupToLpTrimIso 📖	CompOp	—
lpMeasToLpTrim 📖	CompOp	2 math math: lpMeasToLpTrim_ae_eq, lpMeasToLpTrim_smul
lpMeasToLpTrimLie 📖	CompOp	2 math math: lpMeasToLpTrimLie_symm_indicator, lpMeasToLpTrimLie_symm_toLp
lpTrimToLpMeas 📖	CompOp	1 math math: lpTrimToLpMeas_ae_eq
lpTrimToLpMeasSubgroup 📖	CompOp	3 math math: lpMeasSubgroupToLpTrim_right_inv, lpMeasSubgroupToLpTrim_left_inv, lpTrimToLpMeasSubgroup_ae_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_eq_trim_iff_of_aestronglyMeasurable 📖	mathematical	MeasurableSpace MeasurableSpace.instLE AEStronglyMeasurable	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.trim	—	Measure.instOuterMeasureClass StronglyMeasurable.ae_eq_trim_iff Filter.EventuallyEq.trans Filter.EventuallyEq.symm
instCompleteSpaceSubtypeAEEqFunMemAddSubgroupLpLpMeasSubgroupOfFactLeMeasurableSpace 📖	mathematical	—	CompleteSpace AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike Lp AddSubgroup.toAddGroup lpMeasSubgroup instUniformSpaceSubtype Lp.instNormedAddCommGroup	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Fact.elim IsometryEquiv.completeSpace_iff Lp.instCompleteSpace
instCompleteSpaceSubtypeAEEqFunMemAddSubgroupLpSubmoduleLpMeasOfFactLeMeasurableSpace 📖	mathematical	—	CompleteSpace AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike Lp Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup AEEqFun.instAddCommGroup NormedAddCommGroup.toAddCommGroup Lp.instModule NormedCommRing.toNormedRing NormedField.toNormedCommRing NormedSpace.toModule NormedSpace.toIsBoundedSMul Submodule.setLike lpMeas instUniformSpaceSubtype Lp.instNormedAddCommGroup	—	SeminormedAddCommGroup.toIsTopologicalAddGroup NormedSpace.toIsBoundedSMul IsometryEquiv.completeSpace_iff instCompleteSpaceSubtypeAEEqFunMemAddSubgroupLpLpMeasSubgroupOfFactLeMeasurableSpace
isClosed_aestronglyMeasurable 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	IsClosed AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike Lp Lp.instNormedAddCommGroup setOf AEStronglyMeasurable AEEqFun.cast	—	IsComplete.isClosed SeminormedAddCommGroup.toIsTopologicalAddGroup T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace isComplete_aestronglyMeasurable
isComplete_aestronglyMeasurable 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	IsComplete AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike Lp Lp.instNormedAddCommGroup setOf AEStronglyMeasurable AEEqFun.cast	—	SeminormedAddCommGroup.toIsTopologicalAddGroup completeSpace_coe_iff_isComplete instCompleteSpaceSubtypeAEEqFunMemAddSubgroupLpLpMeasSubgroupOfFactLeMeasurableSpace
isometry_lpMeasSubgroupToLpTrim 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	Isometry AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike Lp AddSubgroup.toAddGroup lpMeasSubgroup Measure.trim instPseudoEMetricSpaceSubtype EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace Lp.instNormedAddCommGroup lpMeasSubgroupToLpTrim	—	Isometry.of_dist_eq SeminormedAddCommGroup.toIsTopologicalAddGroup dist_eq_norm lpMeasSubgroupToLpTrim_sub lpMeasSubgroupToLpTrim_norm_map
lpMeasSubgroupToLpTrim_add 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	lpMeasSubgroupToLpTrim AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike Lp AddSubgroup.toAddGroup lpMeasSubgroup AddSubgroup.add Measure.trim	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Lp.ext Mathlib.Tactic.GCongr.rel_imp_rel Measure.instOuterMeasureClass instIsTransOfTrans Filter.EventuallyEq.refl Filter.EventuallyEq.symm Lp.coeFn_add StronglyMeasurable.ae_eq_trim_of_stronglyMeasurable EMetricSpace.metrizableSpace Lp.stronglyMeasurable StronglyMeasurable.add IsTopologicalAddGroup.toContinuousAdd lpMeasSubgroupToLpTrim_ae_eq Filter.EventuallyEq.add
lpMeasSubgroupToLpTrim_ae_eq 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass AEEqFun.cast Measure.trim UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AEEqFun AddSubgroup AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike Lp lpMeasSubgroupToLpTrim SeminormedAddCommGroup.toIsTopologicalAddGroup AddSubgroup.toAddGroup lpMeasSubgroup	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Filter.EventuallyEq.trans Measure.instOuterMeasureClass mem_lpMeasSubgroup_iff_aestronglyMeasurable Subtype.mem memLp_trim_of_mem_lpMeasSubgroup ae_eq_of_ae_eq_trim MemLp.coeFn_toLp Filter.EventuallyEq.symm
lpMeasSubgroupToLpTrim_left_inv 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike Lp AddSubgroup.toAddGroup lpMeasSubgroup Measure.trim lpTrimToLpMeasSubgroup lpMeasSubgroupToLpTrim	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Lp.ext Filter.EventuallyEq.trans Measure.instOuterMeasureClass lpTrimToLpMeasSubgroup_ae_eq lpMeasSubgroupToLpTrim_ae_eq
lpMeasSubgroupToLpTrim_neg 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	lpMeasSubgroupToLpTrim AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike Lp AddSubgroup.toAddGroup lpMeasSubgroup AddSubgroup.neg Measure.trim	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Lp.ext Mathlib.Tactic.GCongr.rel_imp_rel Measure.instOuterMeasureClass instIsTransOfTrans Filter.EventuallyEq.refl Filter.EventuallyEq.symm Lp.coeFn_neg StronglyMeasurable.ae_eq_trim_of_stronglyMeasurable EMetricSpace.metrizableSpace Lp.stronglyMeasurable StronglyMeasurable.neg IsTopologicalAddGroup.toContinuousNeg lpMeasSubgroupToLpTrim_ae_eq Filter.EventuallyEq.neg
lpMeasSubgroupToLpTrim_norm_map 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	Norm.norm AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Measure.trim AddSubgroup AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike Lp Lp.instNorm lpMeasSubgroupToLpTrim AddSubgroup.toAddGroup lpMeasSubgroup NormedAddCommGroup.toNorm AddSubgroup.normedAddCommGroup Lp.instNormedAddCommGroup	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Lp.norm_def eLpNorm_trim Lp.stronglyMeasurable eLpNorm_congr_ae lpMeasSubgroupToLpTrim_ae_eq
lpMeasSubgroupToLpTrim_right_inv 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike Lp AddSubgroup.toAddGroup lpMeasSubgroup Measure.trim lpTrimToLpMeasSubgroup lpMeasSubgroupToLpTrim	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Lp.ext StronglyMeasurable.ae_eq_trim_of_stronglyMeasurable EMetricSpace.metrizableSpace Lp.stronglyMeasurable Filter.EventuallyEq.trans Measure.instOuterMeasureClass lpMeasSubgroupToLpTrim_ae_eq lpTrimToLpMeasSubgroup_ae_eq
lpMeasSubgroupToLpTrim_sub 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	lpMeasSubgroupToLpTrim AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike Lp AddSubgroup.toAddGroup lpMeasSubgroup AddSubgroup.sub Measure.trim	—	SeminormedAddCommGroup.toIsTopologicalAddGroup sub_eq_add_neg lpMeasSubgroupToLpTrim_add lpMeasSubgroupToLpTrim_neg
lpMeasToLpTrimLie_symm_indicator 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasurableSet	AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike Lp Submodule Real DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField Real.instRCLike AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup AEEqFun.instAddCommGroup NormedAddCommGroup.toAddCommGroup Lp.instModule NormedCommRing.toNormedRing NormedField.toNormedCommRing NormedSpace.toModule NormedSpace.toIsBoundedSMul Submodule.setLike lpMeas DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Measure.trim Lp.instNormedAddCommGroup Submodule.seminormedAddCommGroup NormedRing.toRing Submodule.module EquivLike.toFunLike LinearIsometryEquiv.instEquivLike LinearIsometryEquiv.symm lpMeasToLpTrimLie indicatorConstLp LT.lt.ne ENNReal PartialOrder.toPreorder ENNReal.instPartialOrder Measure Set Measure.instFunLike Top.top OrderTop.toTop Preorder.toLE ENNReal.instOrderTop LE.le.trans_lt le_trim Ne.lt_top	—	Lp.ext SeminormedAddCommGroup.toIsTopologicalAddGroup NormedSpace.toIsBoundedSMul RingHomInvPair.ids LT.lt.ne LE.le.trans_lt le_trim Ne.lt_top Measure.instOuterMeasureClass Mathlib.Tactic.GCongr.rel_imp_rel instIsTransOfTrans lpTrimToLpMeas_ae_eq Filter.EventuallyEq.refl ae_eq_of_ae_eq_trim indicatorConstLp_coeFn Filter.EventuallyEq.symm
lpMeasToLpTrimLie_symm_toLp 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace Measure.trim	AEEqFun AddSubgroup AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike Lp Submodule Real DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField Real.instRCLike AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup AEEqFun.instAddCommGroup NormedAddCommGroup.toAddCommGroup Lp.instModule NormedCommRing.toNormedRing NormedField.toNormedCommRing NormedSpace.toModule NormedSpace.toIsBoundedSMul Submodule.setLike lpMeas DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Lp.instNormedAddCommGroup Submodule.seminormedAddCommGroup NormedRing.toRing Submodule.module EquivLike.toFunLike LinearIsometryEquiv.instEquivLike LinearIsometryEquiv.symm lpMeasToLpTrimLie MemLp.toLp memLp_of_memLp_trim	—	Lp.ext SeminormedAddCommGroup.toIsTopologicalAddGroup NormedSpace.toIsBoundedSMul RingHomInvPair.ids memLp_of_memLp_trim Measure.instOuterMeasureClass Mathlib.Tactic.GCongr.rel_imp_rel instIsTransOfTrans lpTrimToLpMeas_ae_eq Filter.EventuallyEq.refl ae_eq_of_ae_eq_trim MemLp.coeFn_toLp Filter.EventuallyEq.symm
lpMeasToLpTrim_ae_eq 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass AEEqFun.cast Measure.trim UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AEEqFun AddSubgroup AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike Lp lpMeasToLpTrim SeminormedAddCommGroup.toIsTopologicalAddGroup Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup AEEqFun.instAddCommGroup NormedAddCommGroup.toAddCommGroup Lp.instModule NormedCommRing.toNormedRing NormedField.toNormedCommRing NormedSpace.toModule NormedSpace.toIsBoundedSMul Submodule.setLike lpMeas	—	SeminormedAddCommGroup.toIsTopologicalAddGroup NormedSpace.toIsBoundedSMul Filter.EventuallyEq.trans Measure.instOuterMeasureClass mem_lpMeasSubgroup_iff_aestronglyMeasurable Subtype.mem memLp_trim_of_mem_lpMeasSubgroup ae_eq_of_ae_eq_trim MemLp.coeFn_toLp Filter.EventuallyEq.symm
lpMeasToLpTrim_smul 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	lpMeasToLpTrim AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike Lp Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup AEEqFun.instAddCommGroup NormedAddCommGroup.toAddCommGroup Lp.instModule NormedCommRing.toNormedRing NormedField.toNormedCommRing NormedSpace.toModule NormedSpace.toIsBoundedSMul Submodule.setLike lpMeas Submodule.smul Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Lp.instIsScalarTower IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Measure.trim	—	SeminormedAddCommGroup.toIsTopologicalAddGroup NormedSpace.toIsBoundedSMul Lp.ext Lp.instIsScalarTower IsScalarTower.left Mathlib.Tactic.GCongr.rel_imp_rel Measure.instOuterMeasureClass instIsTransOfTrans Filter.EventuallyEq.refl Filter.EventuallyEq.symm Lp.coeFn_smul StronglyMeasurable.ae_eq_trim_of_stronglyMeasurable EMetricSpace.metrizableSpace Lp.stronglyMeasurable StronglyMeasurable.const_smul UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul lpMeasToLpTrim_ae_eq Filter.EventuallyEq.const_smul
lpTrimToLpMeasSubgroup_ae_eq 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass AEEqFun.cast UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AEEqFun AddSubgroup AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike Lp AddSubgroup.toAddGroup lpMeasSubgroup lpTrimToLpMeasSubgroup Measure.trim	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MemLp.coeFn_toLp memLp_of_memLp_trim Lp.memLp
lpTrimToLpMeas_ae_eq 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass AEEqFun.cast UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AEEqFun AddSubgroup AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike Lp Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup AEEqFun.instAddCommGroup NormedAddCommGroup.toAddCommGroup Lp.instModule NormedCommRing.toNormedRing NormedField.toNormedCommRing NormedSpace.toModule NormedSpace.toIsBoundedSMul Submodule.setLike lpMeas lpTrimToLpMeas Measure.trim	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MemLp.coeFn_toLp memLp_of_memLp_trim Lp.memLp
memLp_trim_of_mem_lpMeasSubgroup 📖	mathematical	MeasurableSpace MeasurableSpace.instLE AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike Lp AddSubgroup.toAddGroup lpMeasSubgroup	MemLp ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddGroup.toContinuousENorm StronglyMeasurable Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass AEEqFun.cast AEStronglyMeasurable mem_lpMeasSubgroup_iff_aestronglyMeasurable Measure.trim	—	SeminormedAddCommGroup.toIsTopologicalAddGroup mem_lpMeasSubgroup_iff_aestronglyMeasurable Measure.instOuterMeasureClass StronglyMeasurable.aestronglyMeasurable eLpNorm_trim eLpNorm_congr_ae Filter.EventuallyEq.symm Lp.eLpNorm_lt_top
mem_lpMeasSubgroup_iff_aestronglyMeasurable 📖	mathematical	—	AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike Lp AddSubgroup.toAddGroup lpMeasSubgroup AEStronglyMeasurable AEEqFun.cast	—	SeminormedAddCommGroup.toIsTopologicalAddGroup AddSubgroup.mem_carrier lpMeasSubgroup.eq_1 Set.mem_setOf_eq
mem_lpMeasSubgroup_toLp_of_trim 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike Lp AddSubgroup.toAddGroup lpMeasSubgroup MemLp.toLp AEEqFun.cast Measure.trim memLp_of_memLp_trim SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Lp.memLp	—	SeminormedAddCommGroup.toIsTopologicalAddGroup memLp_of_memLp_trim Lp.memLp mem_lpMeasSubgroup_iff_aestronglyMeasurable AEStronglyMeasurable.congr AEStronglyMeasurable.of_trim Lp.aestronglyMeasurable Filter.EventuallyEq.symm Measure.instOuterMeasureClass MemLp.coeFn_toLp
mem_lpMeas_iff_aestronglyMeasurable 📖	mathematical	—	AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike Lp Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup AEEqFun.instAddCommGroup NormedAddCommGroup.toAddCommGroup Lp.instModule NormedCommRing.toNormedRing NormedField.toNormedCommRing NormedSpace.toModule NormedSpace.toIsBoundedSMul Submodule.setLike lpMeas AEStronglyMeasurable AEEqFun.cast	—	SeminormedAddCommGroup.toIsTopologicalAddGroup NormedSpace.toIsBoundedSMul SetLike.mem_coe Submodule.mem_carrier lpMeas.eq_1 Set.mem_setOf_eq
mem_lpMeas_indicatorConstLp 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasurableSet	AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike Lp Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup AEEqFun.instAddCommGroup NormedAddCommGroup.toAddCommGroup Lp.instModule NormedCommRing.toNormedRing NormedField.toNormedCommRing NormedSpace.toModule NormedSpace.toIsBoundedSMul Submodule.setLike lpMeas indicatorConstLp	—	Measure.instOuterMeasureClass StronglyMeasurable.indicator stronglyMeasurable_const indicatorConstLp_coeFn
mem_lpMeas_self 📖	mathematical	—	AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike Lp Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup AEEqFun.instAddCommGroup NormedAddCommGroup.toAddCommGroup Lp.instModule NormedCommRing.toNormedRing NormedField.toNormedCommRing NormedSpace.toModule NormedSpace.toIsBoundedSMul Submodule.setLike lpMeas	—	SeminormedAddCommGroup.toIsTopologicalAddGroup NormedSpace.toIsBoundedSMul mem_lpMeas_iff_aestronglyMeasurable Lp.aestronglyMeasurable

MeasureTheory.AEStronglyMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_ae_measurable' 📖	mathematical	MeasureTheory.AEStronglyMeasurable MeasureTheory.Measure.map AEMeasurable	MeasurableSpace.comap	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.StronglyMeasurable.comp_measurable measurable_iff_comap_le le_rfl MeasureTheory.ae_eq_comp

MeasureTheory.Lp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
induction_stronglyMeasurable 📖	—	MeasurableSpace MeasurableSpace.instLE MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp AddSubgroup.toAddGroup simpleFunc simpleFunc.indicatorConst LT.lt.ne ENNReal PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike Top.top instTopENNReal AddSubgroup.add MeasureTheory.MemLp.toLp MeasureTheory.AEStronglyMeasurable MeasureTheory.AEEqFun.cast	—	—	SeminormedAddCommGroup.toIsTopologicalAddGroup LT.lt.ne NormedSpace.toIsBoundedSMul MeasureTheory.StronglyMeasurable.measurableSet_support EMetricSpace.metrizableSpace MeasureTheory.Measure.instOuterMeasureClass Filter.EventuallyEq.support Filter.EventuallyEq.symm Filter.EventuallyEq.trans Filter.EventuallyEq.inter Set.disjoint_iff_inter_eq_empty Filter.EventuallyEq.refl Set.diff_inter_self_eq_diff Set.inter_comm Filter.EventuallyEq.diff MeasureTheory.ae_eq_refl Set.diff_empty indicator_ae_eq_of_ae_eq_set Set.indicator_support MeasureTheory.StronglyMeasurable.indicator MeasurableSet.diff MeasureTheory.MemLp.ae_eq Disjoint.mono Set.support_indicator_subset disjoint_sdiff_sdiff MeasureTheory.MemLp.toLp_congr induction_stronglyMeasurable_aux
induction_stronglyMeasurable_aux 📖	—	MeasurableSpace MeasurableSpace.instLE MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp AddSubgroup.toAddGroup simpleFunc simpleFunc.indicatorConst LT.lt.ne ENNReal PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike Top.top instTopENNReal AddSubgroup.add MeasureTheory.MemLp.toLp MeasureTheory.AEStronglyMeasurable MeasureTheory.AEEqFun.cast	—	—	SeminormedAddCommGroup.toIsTopologicalAddGroup LT.lt.ne NormedSpace.toIsBoundedSMul RingHomInvPair.ids LinearIsometryEquiv.symm_apply_apply induction simpleFunc.coe_indicatorConst LE.le.trans_lt MeasureTheory.le_trim Ne.lt_top MeasureTheory.lpMeasToLpTrimLie_symm_indicator LinearIsometryEquiv.map_add MeasureTheory.memLp_of_memLp_trim MeasureTheory.lpMeasToLpTrimLie_symm_toLp MeasureTheory.AEStronglyMeasurable.of_trim MeasureTheory.MemLp.aestronglyMeasurable IsClosed.preimage LinearIsometryEquiv.continuous

MeasureTheory.MemLp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
induction_stronglyMeasurable 📖	—	MeasurableSpace MeasurableSpace.instLE Set.indicator NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid MeasureTheory.MemLp ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddGroup.toContinuousENorm MeasureTheory.AEStronglyMeasurable	—	—	SeminormedAddCommGroup.toIsTopologicalAddGroup NormedSpace.toIsBoundedSMul MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.AEStronglyMeasurable.congr Filter.EventuallyEq.symm coeFn_toLp MeasureTheory.Lp.memLp MeasureTheory.Lp.induction_stronglyMeasurable LT.lt.ne MeasureTheory.Lp.simpleFunc.coe_indicatorConst MeasureTheory.indicatorConstLp_coeFn MeasureTheory.memLp_indicator_const Filter.EventuallyEq.trans Filter.EventuallyEq.add MeasureTheory.Lp.coeFn_add add IsTopologicalAddGroup.toContinuousAdd

MeasureTheory.lpMeas

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_fin_strongly_measurable' 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	MeasureTheory.FinStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup MeasureTheory.Measure.trim Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.AEEqFun.cast MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp SeminormedAddCommGroup.toIsTopologicalAddGroup Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup MeasureTheory.AEEqFun.instAddCommGroup MeasureTheory.Lp.instModule NormedCommRing.toNormedRing NormedField.toNormedCommRing NormedSpace.toModule NormedSpace.toIsBoundedSMul Submodule.setLike MeasureTheory.lpMeas	—	SeminormedAddCommGroup.toIsTopologicalAddGroup NormedSpace.toIsBoundedSMul MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Lp.finStronglyMeasurable Filter.EventuallyEq.symm MeasureTheory.lpMeasSubgroupToLpTrim_ae_eq
aestronglyMeasurable 📖	mathematical	—	MeasureTheory.AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.AEEqFun.cast MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup MeasureTheory.AEEqFun.instAddCommGroup NormedAddCommGroup.toAddCommGroup MeasureTheory.Lp.instModule NormedCommRing.toNormedRing NormedField.toNormedCommRing NormedSpace.toModule NormedSpace.toIsBoundedSMul Submodule.setLike MeasureTheory.lpMeas	—	SeminormedAddCommGroup.toIsTopologicalAddGroup NormedSpace.toIsBoundedSMul MeasureTheory.mem_lpMeas_iff_aestronglyMeasurable Subtype.mem

---

← Back to Index