Basic

📁 Source: Mathlib/MeasureTheory/Function/LpSpace/Basic.lean

Statistics

Metric	Count
Definitions compLp, compLpL, compLpₗ, compLp, LpSubmodule, compMeasurePreserving, compMeasurePreservingₗ, compMeasurePreservingₗᵢ, instCoeFun, instDist, instEDist, instInvolutiveStarSubtypeAEEqFunMemAddSubgroup, instModule, instNNNorm, instNorm, instNormedAddCommGroup, instNormedSpace, instStarSubtypeAEEqFunMemAddSubgroup, negPart, posPart, toLp, «term_→₁[_]_», «term_→₂[_]_»	23
Theorems add_compLp, add_compLpL, coeFn_compLp, coeFn_compLp', coeFn_compLpL, comp_memLp, comp_memLp', norm_compLpL_le, norm_compLp_le, smul_compLp, smul_compLpL, coeFn_compLp, compLp_zero, comp_memLp, continuous_compLp, lipschitzWith_compLp, memLp_comp_iff_of_antilipschitz, norm_compLp_le, norm_compLp_sub_le, compMeasurePreserving_mem_Lp, aestronglyMeasurable, antitone, coeFn_add, coeFn_compMeasurePreserving, coeFn_mk, coeFn_neg, coeFn_negPart, coeFn_negPart_eq_max, coeFn_posPart, coeFn_smul, coeFn_star, coeFn_sub, coeFn_zero, coe_LpSubmodule, coe_mk, coe_nnnorm, coe_posPart, compMeasurePreserving_val, compMeasurePreservingₗ_apply, compMeasurePreservingₗᵢ_apply_coe, const_mem_Lp, const_smul_mem_Lp, continuous_negPart, continuous_posPart, dist_def, dist_edist, dist_eq_norm, eLpNorm_lt_top, eLpNorm_ne_top, edist_def, edist_dist, edist_toLp_toLp, edist_toLp_zero, enorm_def, enorm_toLp, eq_zero_iff_ae_eq_zero, ext, ext_iff, instIsBoundedSMul, instIsCentralScalar, instIsScalarTower, instSMulCommClass, instTrivialStarSubtypeAEEqFunMemAddSubgroup, isometry_compMeasurePreserving, lipschitzWith_pos_part, meas_ge_le_mul_pow_enorm, memLp, mem_Lp_iff_eLpNorm_lt_top, mem_Lp_iff_memLp, mem_Lp_of_ae_bound, mem_Lp_of_ae_le, mem_Lp_of_ae_le_mul, mem_Lp_of_ae_nnnorm_bound, mem_Lp_of_nnnorm_ae_le, mem_Lp_of_nnnorm_ae_le_mul, mul_meas_ge_le_pow_enorm, mul_meas_ge_le_pow_enorm', nnnorm_def, nnnorm_eq_zero_iff, nnnorm_le_mul_nnnorm_of_ae_le_mul, nnnorm_le_of_ae_bound, nnnorm_neg, nnnorm_toLp, nnnorm_zero, norm_compMeasurePreserving, norm_def, norm_eq_zero_iff, norm_exponent_zero, norm_le_mul_norm_of_ae_le_mul, norm_le_norm_of_ae_le, norm_le_of_ae_bound, norm_measure_zero, norm_neg, norm_toLp, norm_zero, pow_mul_meas_ge_le_enorm, stronglyMeasurable, toLp_coeFn, toLp_compMeasurePreserving, coeFn_toLp, continuousLinearMap_comp, eLpNorm_mk_lt_top, enorm_rpow, enorm_rpow_div, neg_part, norm_rpow, norm_rpow_div, ofReal, of_comp_antilipschitzWith, pos_part, toLp_add, toLp_congr, toLp_const_smul, toLp_eq_toLp_iff, toLp_neg, toLp_sub, toLp_val, toLp_zero, eLpNorm_aeeqFun, memLp_enorm_rpow_iff, memLp_norm_rpow_iff, memLp_re_im_iff	122
Total	145

ContinuousLinearMap

Definitions

Name	Category	Theorems
compLp 📖	CompOp	10 math math: integral_compLp, norm_compLp_le, smul_compLp, setIntegral_compLp, MeasureTheory.condExpL2_indicator_eq_toSpanSingleton_comp, add_compLp, coeFn_compLp, MeasureTheory.indicatorConstLp_eq_toSpanSingleton_compLp, MeasureTheory.condExpL2_comp_continuousLinearMap, coeFn_compLp'
compLpL 📖	CompOp	4 math math: coeFn_compLpL, add_compLpL, smul_compLpL, norm_compLpL_le
compLpₗ 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_compLp 📖	mathematical	—	compLp ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule add IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp AddSubgroup.add	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.Lp.ext IsTopologicalAddGroup.toContinuousAdd Mathlib.Tactic.GCongr.rel_imp_rel MeasureTheory.Measure.instOuterMeasureClass instIsTransOfTrans Filter.EventuallyEq.refl Filter.EventuallyEq.symm MeasureTheory.Lp.coeFn_add coeFn_compLp' Filter.EventuallyEq.trans Filter.univ_mem' coe_add' Pi.add_def Filter.EventuallyEq.fun_add
add_compLpL 📖	mathematical	—	compLpL ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule add IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp MeasureTheory.Lp.instNormedAddCommGroup MeasureTheory.Lp.instModule NormedCommRing.toNormedRing NormedField.toNormedCommRing NormedSpace.toIsBoundedSMul AddSubgroup.toAddGroup	—	ext SeminormedAddCommGroup.toIsTopologicalAddGroup NormedSpace.toIsBoundedSMul IsTopologicalAddGroup.toContinuousAdd add_compLp
coeFn_compLp 📖	mathematical	—	Filter.Eventually MeasureTheory.AEEqFun.cast UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp compLp DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule funLike MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	SeminormedAddCommGroup.toIsTopologicalAddGroup LipschitzWith.coeFn_compLp
coeFn_compLp' 📖	mathematical	—	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.AEEqFun.cast UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp compLp DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule funLike	—	SeminormedAddCommGroup.toIsTopologicalAddGroup coeFn_compLp
coeFn_compLpL 📖	mathematical	—	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.AEEqFun.cast UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.Lp.instNormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid MeasureTheory.Lp.instModule NormedCommRing.toNormedRing NormedField.toNormedCommRing NormedSpace.toModule NormedSpace.toIsBoundedSMul funLike compLpL	—	SeminormedAddCommGroup.toIsTopologicalAddGroup coeFn_compLp
comp_memLp 📖	mathematical	—	MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule funLike MeasureTheory.AEEqFun.cast MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.MemLp.ae_eq coeFn_compLp' MeasureTheory.Lp.memLp
comp_memLp' 📖	mathematical	MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule funLike	—	MeasureTheory.MemLp.ae_eq SeminormedAddCommGroup.toIsTopologicalAddGroup Filter.EventuallyEq.fun_comp MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.MemLp.coeFn_toLp comp_memLp
norm_compLpL_le 📖	mathematical	—	Real Real.instLE Norm.norm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField 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 MeasureTheory.Lp.instNormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid MeasureTheory.Lp.instModule NormedCommRing.toNormedRing NormedField.toNormedCommRing NormedSpace.toModule NormedSpace.toIsBoundedSMul hasOpNorm MeasureTheory.Lp.instNormedSpace compLpL	—	LinearMap.mkContinuous_norm_le norm_nonneg norm_compLp_le
norm_compLp_le 📖	mathematical	—	Real Real.instLE Norm.norm 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 MeasureTheory.Lp.instNorm compLp Real.instMul ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule hasOpNorm	—	SeminormedAddCommGroup.toIsTopologicalAddGroup LipschitzWith.norm_compLp_le
smul_compLp 📖	mathematical	—	compLp ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing AddCommMonoid.toAddMonoid Module.toDistribMulAction UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup MeasureTheory.AEEqFun.instAddCommGroup MeasureTheory.Lp.instModule	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.Lp.ext UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul Mathlib.Tactic.GCongr.rel_imp_rel MeasureTheory.Measure.instOuterMeasureClass instIsTransOfTrans Filter.EventuallyEq.refl Filter.EventuallyEq.symm MeasureTheory.Lp.coeFn_smul coeFn_compLp' Filter.Eventually.mono Pi.smul_apply coe_smul' Pi.smul_def
smul_compLpL 📖	mathematical	—	compLpL ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing AddCommMonoid.toAddMonoid Module.toDistribMulAction UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp MeasureTheory.Lp.instNormedAddCommGroup MeasureTheory.Lp.instModule NormedCommRing.toNormedRing NormedField.toNormedCommRing NormedSpace.toIsBoundedSMul MeasureTheory.Lp.instSMulCommClass AddSubgroup.zero MeasureTheory.Lp.instIsBoundedSMul	—	ext SeminormedAddCommGroup.toIsTopologicalAddGroup NormedSpace.toIsBoundedSMul UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul MeasureTheory.Lp.instSMulCommClass MeasureTheory.Lp.instIsBoundedSMul smul_compLp

LipschitzWith

Definitions

Name	Category	Theorems
compLp 📖	CompOp	6 math math: lipschitzWith_compLp, coeFn_compLp, continuous_compLp, compLp_zero, norm_compLp_le, norm_compLp_sub_le

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeFn_compLp 📖	mathematical	LipschitzWith EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.AEEqFun.cast UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp compLp	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.AEEqFun.coeFn_comp continuous
compLp_zero 📖	mathematical	LipschitzWith EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	compLp 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.zero	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Lp.eq_zero_iff_ae_eq_zero Filter.EventuallyEq.trans coeFn_compLp Filter.mp_mem MeasureTheory.Lp.coeFn_zero Filter.univ_mem'
comp_memLp 📖	—	LipschitzWith EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace	—	—	sub_zero norm_sub_le MeasureTheory.MemLp.of_le_mul Continuous.comp_aestronglyMeasurable continuous Filter.Eventually.of_forall MeasureTheory.Measure.instOuterMeasureClass
continuous_compLp 📖	mathematical	LipschitzWith EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	Continuous 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 MeasureTheory.Lp.instNormedAddCommGroup compLp	—	continuous SeminormedAddCommGroup.toIsTopologicalAddGroup lipschitzWith_compLp
lipschitzWith_compLp 📖	mathematical	LipschitzWith EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	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 MeasureTheory.Lp.instNormedAddCommGroup compLp	—	of_dist_le_mul SeminormedAddCommGroup.toIsTopologicalAddGroup dist_eq_norm
memLp_comp_iff_of_antilipschitz 📖	mathematical	LipschitzWith EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace AntilipschitzWith NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace	—	MeasureTheory.MemLp.of_comp_antilipschitzWith uniformContinuous comp_memLp
norm_compLp_le 📖	mathematical	LipschitzWith EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	Real Real.instLE Norm.norm 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 MeasureTheory.Lp.instNorm compLp Real.instMul NNReal.toReal	—	SeminormedAddCommGroup.toIsTopologicalAddGroup compLp_zero sub_zero norm_compLp_sub_le
norm_compLp_sub_le 📖	mathematical	LipschitzWith EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	Real Real.instLE Norm.norm 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 MeasureTheory.Lp.instNorm AddSubgroup.sub compLp Real.instMul NNReal.toReal	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.Lp.norm_le_mul_norm_of_ae_le_mul Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Lp.coeFn_sub coeFn_compLp Filter.univ_mem' dist_le_mul

MeasureTheory

Definitions

Name	Category	Theorems
«term_→₁[_]_» 📖	CompOp	—
«term_→₂[_]_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eLpNorm_aeeqFun 📖	mathematical	AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	eLpNorm ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddGroup.toContinuousENorm AEEqFun.cast	—	eLpNorm_congr_ae
memLp_enorm_rpow_iff 📖	mathematical	AEStronglyMeasurable	MemLp ENNReal instENormENNReal ENNReal.instTopologicalSpace Real ENNReal.instPowReal ENorm.enorm ContinuousENorm.toENorm ENNReal.toReal DivInvMonoid.toDiv ENNReal.instDivInvMonoid	—	memLp_enorm_iff CommGroupWithZero.mul_inv_cancel ENNReal.toReal_ne_zero ENNReal.toReal_inv ENNReal.rpow_one div_eq_mul_inv inv_inv mul_assoc ENNReal.inv_mul_cancel mul_one MemLp.enorm_rpow_div
memLp_norm_rpow_iff 📖	mathematical	AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	MemLp Real ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SeminormedAddGroup.toContinuousENorm Real.pseudoMetricSpace Real.instPow Norm.norm NormedAddCommGroup.toNorm ENNReal.toReal ENNReal DivInvMonoid.toDiv ENNReal.instDivInvMonoid	—	memLp_norm_iff Real.norm_eq_abs Real.abs_rpow_of_nonneg norm_nonneg Real.rpow_mul abs_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add ENNReal.toReal_inv mul_inv_cancel₀ abs_of_nonneg Real.rpow_one div_eq_mul_inv inv_inv mul_assoc ENNReal.inv_mul_cancel mul_one MemLp.norm_rpow_div
memLp_re_im_iff 📖	mathematical	—	MemLp Real ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SeminormedAddGroup.toContinuousENorm Real.pseudoMetricSpace DFunLike.coe AddMonoidHom AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.re RCLike.im NormedField.toNormedCommRing SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing	—	Pi.add_apply mul_comm RCLike.re_add_im MemLp.add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing MemLp.ofReal MemLp.const_mul MemLp.re MemLp.im

MeasureTheory.AEEqFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compMeasurePreserving_mem_Lp 📖	mathematical	MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp MeasureTheory.MeasurePreserving	compMeasurePreserving	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.Lp.mem_Lp_iff_eLpNorm_lt_top eLpNorm_compMeasurePreserving

MeasureTheory.Lp

Definitions

Name	Category	Theorems
LpSubmodule 📖	CompOp	1 math math: coe_LpSubmodule
compMeasurePreserving 📖	CompOp	13 math math: indicatorConstLp_compMeasurePreserving, compMeasurePreservingₗ_apply, ContinuousAt.compMeasurePreservingLp, coeFn_compMeasurePreserving, ContinuousWithinAt.compMeasurePreservingLp, Filter.Tendsto.compMeasurePreservingLp, toLp_compMeasurePreserving, compMeasurePreserving_continuous, Continuous.compMeasurePreservingLp, ContinuousOn.compMeasurePreservingLp, isometry_compMeasurePreserving, compMeasurePreserving_val, norm_compMeasurePreserving
compMeasurePreservingₗ 📖	CompOp	1 math math: compMeasurePreservingₗ_apply
compMeasurePreservingₗᵢ 📖	CompOp	1 math math: compMeasurePreservingₗᵢ_apply_coe
instCoeFun 📖	CompOp	—
instDist 📖	CompOp	9 math math: dist_def, dist_edist, MeasureTheory.L1.dist_eq_integral_dist, dist_eq_norm, DomMulAct.dist_smul_Lp, MeasureTheory.L1.dist_def, DomAddAct.dist_vadd_Lp, edist_dist, MeasureTheory.dist_indicatorConstLp_eq_norm
instEDist 📖	CompOp	11 math math: edist_def, MeasureTheory.Integrable.edist_toL1_zero, dist_edist, edist_toLp_toLp, edist_toLp_zero, MeasureTheory.edist_indicatorConstLp_eq_enorm, DomMulAct.edist_smul_Lp, DomAddAct.edist_vadd_Lp, MeasureTheory.L1.edist_def, edist_dist, MeasureTheory.Integrable.edist_toL1_toL1
instInvolutiveStarSubtypeAEEqFunMemAddSubgroup 📖	CompOp	—
instModule 📖	CompOp	173 math math: MeasureTheory.L1.setToL1_eq_setToL1', ContinuousMap.toLp_inj, toTemperedDistributionCLM_apply, MeasureTheory.LpToLpRestrictCLM_coeFn, MeasureTheory.condExpInd_of_measurable, MeasureTheory.condExpL1_smul, instIsScalarTower, MeasureTheory.aestronglyMeasurable_condExpInd, MeasureTheory.condExpInd_ae_eq_condExpIndSMul, MeasureTheory.L1.setToL1_indicatorConstLp, DomMulAct.instSMulCommClassSubtypeAEEqFunMemAddSubgroupLp_1, MeasureTheory.norm_condExpL2_le, MeasureTheory.L1.norm_setToL1_le, MeasureTheory.inner_condExpL2_left_eq_right, ContinuousMap.toLp_denseRange, MeasureTheory.condExpL2_ae_eq_zero_of_ae_eq_zero, ContinuousMap.range_toLp, MeasureTheory.condExpIndL1Fin_smul, MeasureTheory.L1.norm_setToL1_le_norm_setToL1SCLM, MeasureTheory.L1.integral_smul, instFourierInvSMul, ContinuousLinearMap.smul_compLp, SchwartzMap.toLpCLM_apply, compMeasurePreservingₗ_apply, ContinuousMap.toLp_norm_le, MeasureTheory.MemLp.condExpL2_ae_eq_condExp, MeasureTheory.dominatedFinMeasAdditive_condExpInd, MeasureTheory.aestronglyMeasurable_condExpL2, MeasureTheory.L1.setToL1_smul_left, MeasureTheory.L1.setToL1_zero_left, MeasureTheory.condExpInd_nonneg, MeasureTheory.condExpL2_indicator_ae_eq_smul, MeasureTheory.condExpL1CLM_of_aestronglyMeasurable', UnitAddTorus.mFourierCoeff_toLp, ContinuousLinearMap.holderₗ_apply_apply, MeasureTheory.integral_condExpL2_eq, MeasureTheory.setIntegral_condExpL2_indicator, MeasureTheory.L1.setToL1_mono_left', MeasureTheory.lintegral_nnnorm_condExpL2_indicator_le, MeasureTheory.setIntegral_condExpInd, MeasureTheory.L1.setToL1_eq_setToL1SCLM, MeasureTheory.norm_condExpL2_coe_le, MeasureTheory.setLIntegral_nnnorm_condExpL2_indicator_le, MeasureTheory.mem_lpMeas_iff_aestronglyMeasurable, MeasureTheory.L1.setToL1_nonneg, MeasureTheory.L1.integral_def, hasSum_fourier_series_L2, BoundedContinuousFunction.toLp_inj, MeasureTheory.mem_lpMeas_indicatorConstLp, BoundedContinuousFunction.toLp_injective, MeasureTheory.condExpIndSMul_smul, MeasureTheory.lintegral_nnnorm_condExpL2_le, StrongDual.toLp_of_not_memLp, compMeasurePreservingₗᵢ_apply_coe, MeasureTheory.L1.setToFun_eq_setToL1, MeasureTheory.L1.integral_eq_setToL1, MeasureTheory.Integrable.toL1_smul, ContinuousLinearMap.holder_smul_left, coeFn_smul, MeasureTheory.condExpL1CLM_indicatorConstLp, MeasureTheory.L1.setToL1_add_left', MeasureTheory.L1.setToL1_mono_left, MeasureTheory.condExpInd_disjoint_union, MeasureTheory.lpMeasToLpTrimLie_symm_indicator, ContinuousMap.toLp_def, MeasureTheory.L1.setToL1_smul_left', constₗ_apply, DomMulAct.instSMulCommClassSubtypeAEEqFunMemAddSubgroupLp_2, instFourierSMul, MeasureTheory.norm_condExpInd_apply_le, MeasureTheory.condExpIndL1_smul, ContinuousMap.toLp_norm_eq_toLp_norm_coe, fourierCoeff_toLp, MeasureTheory.integral_condExpL2_eq_of_fin_meas_real, MeasureTheory.condExpIndL1_smul', norm_constL_le, MeasureTheory.condExpL2_indicator_of_measurable, MeasureTheory.setIntegral_condExpL1CLM_of_measure_ne_top, MeasureTheory.condExp_ae_eq_condExpL1CLM, BoundedContinuousFunction.coeFn_toLp, MeasureTheory.Integrable.toL1_smul', UnitAddTorus.instContinuousSMulComplexSubtypeAEEqFunVolumeMemAddSubgroupLp, MeasureTheory.condExpL2_indicator_eq_toSpanSingleton_comp, MeasureTheory.L1.tendsto_setToL1, MeasureTheory.condExpL1CLM_indicatorConst, MeasureTheory.L1.nnnorm_Integral_le_one, UnitAddTorus.hasSum_mFourier_series_L2, MeasureTheory.instCompleteSpaceSubtypeAEEqFunMemAddSubgroupLpSubmoduleLpMeasOfFactLeMeasurableSpace, MeasureTheory.lintegral_nnnorm_condExpL2_indicator_le_real, ContinuousLinearMap.lpPairing_eq_integral, ContinuousLinearMap.holder_smul_right, MeasureTheory.condExpL1CLM_lpMeas, StrongDual.toLpₗ_apply, MeasureTheory.L1.setToL1_apply_coeToLp, MeasureTheory.L1.setToL1_congr_left', MeasureTheory.L1.SimpleFunc.integralCLM'_L1_eq_integral, MeasureTheory.L1.setToL1_congr_left, MeasureTheory.L1.setToL1_smul, ContinuousLinearMap.coeFn_compLpL, StrongDual.norm_toLpₗ_le, instIsCentralScalar, ContinuousMap.toLp_injective, StrongDual.toLpₗ_of_not_memLp, MeasureTheory.integrable_condExpL2_of_isFiniteMeasure, instIsBoundedSMul, ContinuousMap.coe_toLp, span_fourierLp_closure_eq_top, MeasureTheory.aestronglyMeasurable_condExpL1CLM, MeasureTheory.integrable_condExpL2_indicator, MeasureTheory.MemLp.condExpL2_ae_eq_condExp', simpleFunc.coe_smul, ContinuousMap.coeFn_toLp, MeasureTheory.L1.norm_setToL1_le_mul_norm', instSMulCommClass, MeasureTheory.lpTrimToLpMeas_ae_eq, ContinuousMap.toLp_comp_toContinuousMap, smul_comm, MeasureTheory.L1.norm_setToL1_le', MeasureTheory.withDensitySMulLI_apply, constL_apply, MeasureTheory.condExpInd_smul', MeasureTheory.L1.setToL1_add_left, BoundedContinuousFunction.toLp_norm_le, MeasureTheory.L1.norm_setToL1_le_mul_norm, MeasureTheory.norm_condExpInd_le, MeasureTheory.inner_condExpL2_eq_inner_fun, StrongDual.toLp_apply, MeasureTheory.mem_lpMeas_self, MeasureTheory.integrableOn_condExpL2_of_measure_ne_top, MeasureTheory.condExpInd_disjoint_union_apply, ContinuousLinearMap.add_compLpL, MeasureTheory.L1.setToL1_simpleFunc_indicatorConst, ker_toTemperedDistributionCLM_eq_bot, MeasureTheory.L1.setToL1_zero_left', MeasureTheory.BoundedContinuousFunction.inner_toLp, MeasureTheory.L1.norm_Integral_le_one, MeasureTheory.L1.setToL1_mono, smul_assoc, ContinuousLinearMap.smul_compLpL, ContinuousLinearMap.norm_compLpL_le, MeasureTheory.setIntegral_condExpL1CLM, MeasureTheory.lpMeasToLpTrim_ae_eq, MeasureTheory.eLpNorm_condExpL2_le, MeasureTheory.L1.integral_eq', MeasureTheory.lpMeasToLpTrim_smul, MeasureTheory.condExpIndSMul_ae_eq_smul, ContinuousLinearMap.norm_holderL_le, MeasureTheory.lpMeas.ae_fin_strongly_measurable', MeasureTheory.L1.setToL1'_eq_setToL1SCLM, MeasureTheory.condExpIndSMul_smul', MeasureTheory.ContinuousMap.inner_toLp, ContinuousLinearMap.holderL_apply_apply, MeasureTheory.condExpInd_empty, MeasureTheory.condExpL1CLM_smul, UnitAddTorus.span_mFourierLp_closure_eq_top, MeasureTheory.condExpIndL1Fin_smul', BoundedContinuousFunction.range_toLp, MeasureTheory.L1.integral_eq, MeasureTheory.L1.setToL1'_apply_coeToLp, SchwartzMap.denseRange_toLpCLM, MeasureTheory.L1.setToL1_const, MeasureTheory.lpMeasToLpTrimLie_symm_toLp, MeasureTheory.MemLp.toLp_const_smul, MeasureTheory.L1.setToL1_lipschitz, MeasureTheory.norm_condExpL2_le_one, MeasureTheory.setToFun_eq, MeasureTheory.condExpL2_comp_continuousLinearMap, BoundedContinuousFunction.toLp_denseRange, MeasureTheory.condExpL2_const_inner, MeasureTheory.Lp_toLp_restrict_smul, MeasureTheory.condExpL1_eq, MeasureTheory.condExpL2_indicator_nonneg, MeasureTheory.lpMeas.aestronglyMeasurable
instNNNorm 📖	CompOp	18 math math: nnnorm_le_of_ae_bound, nnnorm_def, enorm_toLp, nnnorm_eq_zero_iff, nnnorm_le_mul_nnnorm_of_ae_le_mul, MeasureTheory.edist_indicatorConstLp_eq_enorm, BoundedContinuousFunction.Lp_nnnorm_le, MeasureTheory.enorm_indicatorConstLp_le, nnnorm_neg, nnnorm_toLp, coe_nnnorm, ContinuousLinearMap.nnnorm_holder_apply_apply_le, MeasureTheory.L1.nnnorm_integral_le, MeasureTheory.nnnorm_indicatorConstLp_le, enorm_def, DomMulAct.nnnorm_smul_Lp, DomAddAct.nnnorm_vadd_Lp, nnnorm_zero
instNorm 📖	CompOp	62 math math: SchwartzMap.norm_toLp_le_seminorm, mul_meas_ge_le_pow_enorm', MeasureTheory.norm_indicatorConstLp_le, MeasureTheory.norm_condExpL2_le, ContinuousLinearMap.norm_compLp_le, MeasureTheory.norm_setToFun_le_mul_norm', MeasureTheory.norm_indicatorConstLp, MeasureTheory.L1.ofReal_norm_eq_lintegral, MeasureTheory.norm_indicatorConstLp_top, norm_zero, MeasureTheory.L1.norm_def, MeasureTheory.Integrable.norm_toL1, MeasureTheory.norm_condExpL2_coe_le, SchwartzMap.norm_fourier_toL2_eq, norm_toLp, SchwartzMap.norm_fourierTransformCLM_toL2_eq, norm_neg, dist_eq_norm, MeasureTheory.norm_setToFun_le', norm_const_le, norm_le_norm_of_ae_le, coe_nnnorm, norm_fourier_eq, norm_const', MeasureTheory.norm_condExpIndL1_le, SchwartzMap.norm_toLp, MeasureTheory.norm_condExpInd_apply_le, DomAddAct.norm_vadd_Lp, norm_smul_le, BoundedContinuousFunction.Lp_norm_le, DomMulAct.norm_smul_Lp, MeasureTheory.L1.integral_eq_norm_posPart_sub, norm_const, norm_le_of_ae_bound, StrongDual.norm_toLpₗ_le, MeasureTheory.L1.norm_integral_le, MeasureTheory.lpMeasSubgroupToLpTrim_norm_map, norm_exponent_zero, MeasureTheory.L1.norm_setToL1_le_mul_norm', MeasureTheory.L1.norm_of_fun_eq_integral_norm, MeasureTheory.Integrable.norm_toL1_eq_lintegral_norm, MeasureTheory.norm_setToFun_le_mul_norm, MeasureTheory.L1.norm_setToL1_le_mul_norm, MeasureTheory.norm_Lp_toLp_restrict_le, norm_measure_zero, norm_eq_zero_iff, meas_ge_le_mul_pow_enorm, MeasureTheory.L1.norm_sub_eq_lintegral, MeasureTheory.norm_indicatorConstLp', MeasureTheory.L1.ofReal_norm_sub_eq_lintegral, LipschitzWith.norm_compLp_le, pow_mul_meas_ge_le_enorm, ContinuousLinearMap.norm_holder_apply_apply_le, MeasureTheory.norm_condExpIndL1Fin_le, norm_le_mul_norm_of_ae_le_mul, MeasureTheory.dist_indicatorConstLp_eq_norm, LipschitzWith.norm_compLp_sub_le, MeasureTheory.norm_setToFun_le, norm_compMeasurePreserving, mul_meas_ge_le_pow_enorm, norm_def, MeasureTheory.L1.norm_eq_integral_norm
instNormedAddCommGroup 📖	CompOp	234 math math: MeasureTheory.L1.setToL1_eq_setToL1', instHasSolidNorm, ContinuousMap.toLp_inj, toTemperedDistributionCLM_apply, MeasureTheory.LpToLpRestrictCLM_coeFn, MeasureTheory.L1.SimpleFunc.norm_Integral_le_one, tendsto_Lp_iff_tendsto_eLpNorm'', MeasureTheory.condExpInd_of_measurable, MeasureTheory.condExpL1_smul, MeasureTheory.aestronglyMeasurable_condExpInd, MeasureTheory.condExpInd_ae_eq_condExpIndSMul, MeasureTheory.L1.setToL1_indicatorConstLp, MeasureTheory.L1.SimpleFunc.setToL1SCLM_add_left, UnitAddTorus.coe_mFourierBasis, MeasureTheory.tendsto_condExpL1_of_dominated_convergence, MeasureTheory.norm_condExpL2_le, cauchySeq_Lp_iff_cauchySeq_eLpNorm, ContinuousLinearMap.continuous_integral_comp_L1, MeasureTheory.L1.norm_setToL1_le, MeasureTheory.inner_condExpL2_left_eq_right, ContinuousMap.toLp_denseRange, MeasureTheory.condExpL2_ae_eq_zero_of_ae_eq_zero, LipschitzWith.lipschitzWith_compLp, ContinuousMap.range_toLp, MeasureTheory.condExpIndL1Fin_smul, MeasureTheory.L1.SimpleFunc.setToL1SCLM_const, simpleFunc.uniformContinuous, MeasureTheory.L1.norm_setToL1_le_norm_setToL1SCLM, MeasureTheory.L1.integral_smul, instFourierInvSMul, SchwartzMap.toLpCLM_apply, ContinuousMap.toLp_norm_le, simpleFunc.isDenseEmbedding, MeasureTheory.L1.SimpleFunc.norm_setToL1S_le, MeasureTheory.MemLp.condExpL2_ae_eq_condExp, MeasureTheory.continuous_condExpIndL1, MeasureTheory.dominatedFinMeasAdditive_condExpInd, MeasureTheory.aestronglyMeasurable_condExpL2, MeasureTheory.L1.setToL1_smul_left, MeasureTheory.L1.setToL1_zero_left, MeasureTheory.condExpInd_nonneg, MeasureTheory.L1.continuous_integral, MeasureTheory.condExpL2_indicator_ae_eq_smul, MeasureTheory.condExpL1CLM_of_aestronglyMeasurable', UnitAddTorus.mFourierCoeff_toLp, MeasureTheory.L1.SimpleFunc.setToL1SCLM_zero_left', MeasureTheory.continuous_setToFun, MeasureTheory.integral_condExpL2_eq, DomAddAct.instIsIsometricVAddSubtypeAEEqFunMemAddAddSubgroupLp, orthonormal_fourier, MeasureTheory.setIntegral_condExpL2_indicator, MeasureTheory.L1.SimpleFunc.integral_eq_norm_posPart_sub, MeasureTheory.L1.setToL1_mono_left', MeasureTheory.lintegral_nnnorm_condExpL2_indicator_le, MeasureTheory.setIntegral_condExpInd, MeasureTheory.L1.setToL1_eq_setToL1SCLM, MeasureTheory.norm_condExpL2_coe_le, MeasureTheory.setLIntegral_nnnorm_condExpL2_indicator_le, MeasureTheory.L1.setToL1_nonneg, boundedContinuousFunction_topologicalClosure, SecondCountableTopology, instCompleteSpace, MeasureTheory.L1.integral_def, hasSum_fourier_series_L2, MeasureTheory.L1.SimpleFunc.setToL1S_smul_real, BoundedContinuousFunction.range_toLpHom, BoundedContinuousFunction.toLp_inj, BoundedContinuousFunction.toLp_injective, MeasureTheory.condExpIndSMul_smul, MeasureTheory.lintegral_nnnorm_condExpL2_le, StrongDual.toLp_of_not_memLp, compMeasurePreservingₗᵢ_apply_coe, MeasureTheory.L1.setToFun_eq_setToL1, MeasureTheory.L1.integral_eq_setToL1, MeasureTheory.Integrable.toL1_smul, MeasureTheory.condExpL1CLM_indicatorConstLp, MeasureTheory.L1.setToL1_add_left', MeasureTheory.L1.setToL1_mono_left, MeasureTheory.condExpInd_disjoint_union, MeasureTheory.lpMeasToLpTrimLie_symm_indicator, MeasureTheory.Measure.MeasureDense.indicatorConstLp_subset_closure, ContinuousMap.toLp_def, MeasureTheory.L1.setToL1_smul_left', boundedContinuousFunction_dense, instFourierSMul, MeasureTheory.L1.SimpleFunc.setToL1SCLM_congr_left, MeasureTheory.L1.SimpleFunc.norm_eq_sum_mul, MeasureTheory.norm_condExpInd_apply_le, MeasureTheory.isClosed_aestronglyMeasurable, MeasureTheory.condExpIndL1_smul, UnitAddTorus.orthonormal_mFourier, ContinuousMap.toLp_norm_eq_toLp_norm_coe, MeasureTheory.Integrable.enorm_toL1, MeasureTheory.continuous_integral_integral, fourierCoeff_toLp, coe_fourierBasis, ProbabilityTheory.Kernel.continuous_integral_integral, MeasureTheory.integral_condExpL2_eq_of_fin_meas_real, simpleFunc.denseRange, MeasureTheory.condExpIndL1_smul', norm_constL_le, MeasureTheory.condExpL2_indicator_of_measurable, MeasureTheory.setIntegral_condExpL1CLM_of_measure_ne_top, MeasureTheory.condExp_ae_eq_condExpL1CLM, BoundedContinuousFunction.coeFn_toLp, MeasureTheory.Integrable.toL1_smul', UnitAddTorus.instContinuousSMulComplexSubtypeAEEqFunVolumeMemAddSubgroupLp, instContinuousVAddDomAddAct, MeasureTheory.condExpL2_indicator_eq_toSpanSingleton_comp, MeasureTheory.L1.SimpleFunc.norm_setToL1SCLM_le', MeasureTheory.condExpL1CLM_indicatorConst, MeasureTheory.L1.nnnorm_Integral_le_one, instContinuousFourierInv, UnitAddTorus.hasSum_mFourier_series_L2, MeasureTheory.instCompleteSpaceSubtypeAEEqFunMemAddSubgroupLpSubmoduleLpMeasOfFactLeMeasurableSpace, MeasureTheory.lintegral_nnnorm_condExpL2_indicator_le_real, MeasureTheory.L1.SimpleFunc.setToL1SCLM_smul_left, ContinuousLinearMap.lpPairing_eq_integral, simpleFunc.norm_toSimpleFunc, MeasureTheory.L1.SimpleFunc.setToL1SCLM_smul_left', MeasureTheory.condExpL1CLM_lpMeas, MeasureTheory.L1.setToL1_apply_coeToLp, MeasureTheory.L1.setToL1_congr_left', MeasureTheory.L1.SimpleFunc.integralCLM'_L1_eq_integral, MeasureTheory.L1.setToL1_congr_left, MeasureTheory.L1.setToL1_smul, ContinuousLinearMap.coeFn_compLpL, MeasureTheory.L1.SimpleFunc.setToL1SCLM_congr_left', ProbabilityTheory.Kernel.continuous_integral_integral_comp, ContinuousMap.toLp_injective, MeasureTheory.integrable_condExpL2_of_isFiniteMeasure, tendsto_Lp_of_tendsto_eLpNorm, instIsBoundedSMul, ContinuousMap.coe_toLp, DomMulAct.instIsIsometricSMulSubtypeAEEqFunMemAddSubgroupLp, span_fourierLp_closure_eq_top, MeasureTheory.aestronglyMeasurable_condExpL1CLM, MeasureTheory.continuous_integral, simpleFunc.isBoundedSMul, MeasureTheory.integrable_condExpL2_indicator, MeasureTheory.lpMeasSubgroupToLpTrim_norm_map, MeasureTheory.MemLp.condExpL2_ae_eq_condExp', completeSpace_lp_of_cauchy_complete_eLpNorm, ContinuousMap.coeFn_toLp, MeasureTheory.L1.norm_setToL1_le_mul_norm', MeasureTheory.L1.SimpleFunc.integral_smul, MeasureTheory.L1.SimpleFunc.norm_setToL1SCLM_le, ContinuousMap.toLp_comp_toContinuousMap, MeasureTheory.L1.SimpleFunc.setToL1SCLM_congr_measure, SchwartzMap.continuous_toLp, MeasureTheory.isComplete_aestronglyMeasurable, simpleFunc.isUniformEmbedding, MeasureTheory.continuous_indicatorConstLp_set, MeasureTheory.L1.norm_setToL1_le', MeasureTheory.withDensitySMulLI_apply, simpleFunc.isUniformInducing, constL_apply, MeasureTheory.condExpInd_smul', MeasureTheory.L1.setToL1_add_left, BoundedContinuousFunction.toLp_norm_le, continuous_negPart, MeasureTheory.L1.SimpleFunc.norm_eq_integral, MeasureTheory.L1.SimpleFunc.norm_integral_le_norm, MeasureTheory.L1.norm_setToL1_le_mul_norm, MeasureTheory.L1.SimpleFunc.setToL1SCLM_mono_left', instOrderClosedTopologySubtypeAEEqFunMemAddSubgroupOfClosedIciTopology, MeasureTheory.norm_condExpInd_le, MeasureTheory.inner_condExpL2_eq_inner_fun, StrongDual.toLp_apply, MeasureTheory.integrableOn_condExpL2_of_measure_ne_top, MeasureTheory.condExpInd_disjoint_union_apply, ContinuousLinearMap.add_compLpL, MeasureTheory.L1.setToL1_simpleFunc_indicatorConst, tendsto_Lp_iff_tendsto_eLpNorm', MeasureTheory.L1.SimpleFunc.setToL1SCLM_zero_left, UnitAddTorus.mFourierBasis_repr, MeasureTheory.tendsto_indicatorConstLp_set, ker_toTemperedDistributionCLM_eq_bot, fourierBasis_repr, MeasureTheory.L1.setToL1_zero_left', MeasureTheory.BoundedContinuousFunction.inner_toLp, MeasureTheory.L1.norm_Integral_le_one, MeasureTheory.L1.setToL1_mono, LipschitzWith.continuous_compLp, compMeasurePreserving_continuous, MeasureTheory.isometry_lpMeasSubgroupToLpTrim, ContinuousLinearMap.smul_compLpL, ContinuousLinearMap.norm_compLpL_le, MeasureTheory.L1.SimpleFunc.setToL1SCLM_mono_left, MeasureTheory.setIntegral_condExpL1CLM, MeasureTheory.eLpNorm_condExpL2_le, MeasureTheory.L1.integral_eq', simpleFunc.denseRange_coeSimpleFuncNonnegToLpNonneg, MeasureTheory.L1.SimpleFunc.setToL1SCLM_mono, MeasureTheory.condExpIndSMul_ae_eq_smul, simpleFunc.isDenseInducing, dense_hasCompactSupport_contDiff, ContinuousLinearMap.norm_holderL_le, MeasureTheory.L1.setToL1'_eq_setToL1SCLM, MeasureTheory.condExpIndSMul_smul', MeasureTheory.instCompleteSpaceSubtypeAEEqFunMemAddSubgroupLpLpMeasSubgroupOfFactLeMeasurableSpace, MeasureTheory.L1.SimpleFunc.setToL1SCLM_nonneg, MeasureTheory.ContinuousMap.inner_toLp, ContinuousLinearMap.holderL_apply_apply, instContinuousFourier, MeasureTheory.condExpInd_empty, MeasureTheory.condExpL1CLM_smul, MeasureTheory.continuous_setIntegral, UnitAddTorus.span_mFourierLp_closure_eq_top, MeasureTheory.condExpIndL1Fin_smul', BoundedContinuousFunction.range_toLp, MeasureTheory.L1.integral_eq, MeasureTheory.SimpleFunc.tendsto_approxOn_range_Lp, MeasureTheory.L1.setToL1'_apply_coeToLp, SchwartzMap.denseRange_toLpCLM, MeasureTheory.L1.setToL1_const, MeasureTheory.lpMeasToLpTrimLie_symm_toLp, MeasureTheory.continuous_L1_toL1, tendsto_Lp_iff_tendsto_eLpNorm, MeasureTheory.L1.setToL1_lipschitz, MeasureTheory.norm_condExpL2_le_one, MeasureTheory.setToFun_eq, MeasureTheory.condExpL2_comp_continuousLinearMap, BoundedContinuousFunction.toLp_denseRange, MeasureTheory.condExpL2_const_inner, isometry_compMeasurePreserving, simpleFunc.dense, MeasureTheory.condExpL1_eq, instContinuousSMulDomMulAct, MeasureTheory.condExpL2_indicator_nonneg, MeasureTheory.L1.SimpleFunc.setToL1SCLM_add_left', simpleFunc.norm_toLp, continuous_posPart, MeasureTheory.L1.SimpleFunc.setToL1S_smul
instNormedSpace 📖	CompOp	15 math math: MeasureTheory.L1.norm_setToL1_le, MeasureTheory.L1.norm_setToL1_le_norm_setToL1SCLM, ContinuousMap.toLp_norm_le, MeasureTheory.dominatedFinMeasAdditive_condExpInd, ContinuousMap.toLp_norm_eq_toLp_norm_coe, norm_constL_le, MeasureTheory.L1.nnnorm_Integral_le_one, MeasureTheory.L1.norm_setToL1_le', BoundedContinuousFunction.toLp_norm_le, MeasureTheory.norm_condExpInd_le, MeasureTheory.L1.norm_Integral_le_one, ContinuousLinearMap.norm_compLpL_le, ContinuousLinearMap.norm_holderL_le, ContinuousLinearMap.holderL_apply_apply, MeasureTheory.norm_condExpL2_le_one
instStarSubtypeAEEqFunMemAddSubgroup 📖	CompOp	2 math math: instTrivialStarSubtypeAEEqFunMemAddSubgroup, coeFn_star
negPart 📖	CompOp	5 math math: MeasureTheory.L1.SimpleFunc.coe_negPart, coeFn_negPart_eq_max, MeasureTheory.L1.integral_eq_norm_posPart_sub, continuous_negPart, coeFn_negPart
posPart 📖	CompOp	5 math math: MeasureTheory.L1.integral_eq_norm_posPart_sub, coe_posPart, coeFn_posPart, MeasureTheory.L1.SimpleFunc.coe_posPart, continuous_posPart

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
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 SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.AEEqFun.aestronglyMeasurable
antitone 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder	AddSubgroup MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup AddSubgroup.instPartialOrder MeasureTheory.Lp	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.MemLp.mono_exponent MeasureTheory.AEEqFun.aestronglyMeasurable
coeFn_add 📖	mathematical	—	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.AEEqFun.cast UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp SeminormedAddCommGroup.toIsTopologicalAddGroup AddSubgroup.add Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.AEEqFun.coeFn_add IsTopologicalAddGroup.toContinuousAdd
coeFn_compMeasurePreserving 📖	mathematical	MeasureTheory.MeasurePreserving	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.AEEqFun.cast UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp DFunLike.coe AddMonoidHom SeminormedAddCommGroup.toIsTopologicalAddGroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddMonoidHom.instFunLike compMeasurePreserving	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.AEEqFun.coeFn_compMeasurePreserving
coeFn_mk 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder MeasureTheory.eLpNorm ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm MeasureTheory.AEEqFun.cast SeminormedAddCommGroup.toPseudoMetricSpace Top.top instTopENNReal	MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp SeminormedAddCommGroup.toIsTopologicalAddGroup	—	SeminormedAddCommGroup.toIsTopologicalAddGroup
coeFn_neg 📖	mathematical	—	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.AEEqFun.cast UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp SeminormedAddCommGroup.toIsTopologicalAddGroup AddSubgroup.neg Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.AEEqFun.coeFn_neg
coeFn_negPart 📖	mathematical	—	Filter.Eventually Real MeasureTheory.AEEqFun.cast UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.normedAddCommGroup MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp negPart Real.instNeg Real.instMin Real.instZero MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Filter.Eventually.mono MeasureTheory.Measure.instOuterMeasureClass coeFn_negPart_eq_max max_neg_neg Real.instIsOrderedAddMonoid neg_zero
coeFn_negPart_eq_max 📖	mathematical	—	Filter.Eventually Real MeasureTheory.AEEqFun.cast UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.normedAddCommGroup MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp negPart Real.instMax Real.instNeg Real.instZero MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.Measure.instOuterMeasureClass negPart.eq_1 Filter.mp_mem coeFn_neg coeFn_posPart Filter.univ_mem' Pi.neg_apply
coeFn_posPart 📖	mathematical	—	Filter.EventuallyEq Real MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.AEEqFun.cast UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.normedAddCommGroup MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp posPart Real.instMax Real.instZero	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.AEEqFun.coeFn_posPart HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid
coeFn_smul 📖	mathematical	—	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.AEEqFun.cast UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp SeminormedAddCommGroup.toIsTopologicalAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup MeasureTheory.AEEqFun.instAddCommGroup NormedAddCommGroup.toAddCommGroup instModule Function.hasSMul ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.AEEqFun.coeFn_smul
coeFn_star 📖	mathematical	—	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.AEEqFun.cast UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp Star.star SeminormedAddCommGroup.toIsTopologicalAddGroup instStarSubtypeAEEqFunMemAddSubgroup Pi.instStarForall InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.AEEqFun.coeFn_star NormedStarGroup.to_continuousStar
coeFn_sub 📖	mathematical	—	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.AEEqFun.cast UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp SeminormedAddCommGroup.toIsTopologicalAddGroup AddSubgroup.sub Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.AEEqFun.coeFn_sub
coeFn_zero 📖	mathematical	—	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.AEEqFun.cast UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp SeminormedAddCommGroup.toIsTopologicalAddGroup AddSubgroup.zero Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	MeasureTheory.AEEqFun.coeFn_zero
coe_LpSubmodule 📖	mathematical	—	Submodule.toAddSubgroup MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NormedRing.toRing MeasureTheory.AEEqFun.instAddCommGroup NormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.AEEqFun.instModule Ring.toSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid LpSubmodule MeasureTheory.Lp	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul
coe_mk 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder MeasureTheory.eLpNorm ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm MeasureTheory.AEEqFun.cast SeminormedAddCommGroup.toPseudoMetricSpace Top.top instTopENNReal	MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp	—	SeminormedAddCommGroup.toIsTopologicalAddGroup
coe_nnnorm 📖	mathematical	—	NNReal.toReal NNNorm.nnnorm 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 instNNNorm Norm.norm instNorm	—	SeminormedAddCommGroup.toIsTopologicalAddGroup
coe_posPart 📖	mathematical	—	MeasureTheory.AEEqFun Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.normedAddCommGroup AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp posPart MeasureTheory.AEEqFun.posPart Real.linearOrder HasSolidNorm.orderClosedTopology DistribLattice.toLattice instDistribLatticeOfLinearOrder instHasSolidNormReal Real.instIsOrderedAddMonoid Real.instZero	—	SeminormedAddCommGroup.toIsTopologicalAddGroup
compMeasurePreserving_val 📖	mathematical	MeasureTheory.MeasurePreserving	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 DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddMonoidHom.instFunLike compMeasurePreserving MeasureTheory.AEEqFun.compMeasurePreserving	—	SeminormedAddCommGroup.toIsTopologicalAddGroup
compMeasurePreservingₗ_apply 📖	mathematical	MeasureTheory.MeasurePreserving	DFunLike.coe LinearMap Ring.toSemiring NormedRing.toRing RingHom.id Semiring.toNonAssocSemiring 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 AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup MeasureTheory.AEEqFun.instAddCommGroup NormedAddCommGroup.toAddCommGroup instModule LinearMap.instFunLike compMeasurePreservingₗ ZeroHom.toFun AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddMonoidHom.toZeroHom compMeasurePreserving	—	SeminormedAddCommGroup.toIsTopologicalAddGroup
compMeasurePreservingₗᵢ_apply_coe 📖	mathematical	MeasureTheory.MeasurePreserving	MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp DFunLike.coe LinearIsometry Ring.toSemiring NormedRing.toRing RingHom.id Semiring.toNonAssocSemiring SeminormedAddCommGroup.toIsTopologicalAddGroup instNormedAddCommGroup instModule LinearIsometry.instFunLike compMeasurePreservingₗᵢ MeasureTheory.AEEqFun.compMeasurePreserving	—	SeminormedAddCommGroup.toIsTopologicalAddGroup
const_mem_Lp 📖	mathematical	—	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 MeasureTheory.AEEqFun.const	—	MeasureTheory.MemLp.eLpNorm_mk_lt_top MeasureTheory.memLp_const
const_smul_mem_Lp 📖	mathematical	—	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 MeasureTheory.AEEqFun.instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul mem_Lp_iff_eLpNorm_lt_top MeasureTheory.eLpNorm_congr_ae MeasureTheory.AEEqFun.coeFn_smul LE.le.trans_lt MeasureTheory.eLpNorm_const_smul_le Ne.lt_top ENNReal.mul_ne_top enorm_ne_top eLpNorm_ne_top
continuous_negPart 📖	mathematical	—	Continuous MeasureTheory.AEEqFun Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.normedAddCommGroup AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp instNormedAddCommGroup negPart	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Continuous.comp continuous_posPart ContinuousNeg.continuous_neg IsTopologicalAddGroup.toContinuousNeg
continuous_posPart 📖	mathematical	—	Continuous MeasureTheory.AEEqFun Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.normedAddCommGroup AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp instNormedAddCommGroup posPart	—	LipschitzWith.continuous_compLp lipschitzWith_pos_part
dist_def 📖	mathematical	—	Dist.dist 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 instDist ENNReal.toReal MeasureTheory.eLpNorm ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddGroup.toContinuousENorm Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid MeasureTheory.AEEqFun.cast	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.eLpNorm_congr_ae coeFn_sub
dist_edist 📖	mathematical	—	Dist.dist 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 instDist ENNReal.toReal EDist.edist instEDist	—	SeminormedAddCommGroup.toIsTopologicalAddGroup dist_def
dist_eq_norm 📖	mathematical	—	Dist.dist 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 instDist Norm.norm instNorm AddSubgroup.sub	—	SeminormedAddCommGroup.toIsTopologicalAddGroup
eLpNorm_lt_top 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder MeasureTheory.eLpNorm ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm MeasureTheory.AEEqFun.cast SeminormedAddCommGroup.toPseudoMetricSpace MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp Top.top instTopENNReal	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Subtype.prop
eLpNorm_ne_top 📖	—	—	—	—	SeminormedAddCommGroup.toIsTopologicalAddGroup LT.lt.ne eLpNorm_lt_top
edist_def 📖	mathematical	—	EDist.edist 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 instEDist MeasureTheory.eLpNorm ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddGroup.toContinuousENorm Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid MeasureTheory.AEEqFun.cast	—	SeminormedAddCommGroup.toIsTopologicalAddGroup
edist_dist 📖	mathematical	—	EDist.edist 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 instEDist ENNReal.ofReal Dist.dist instDist	—	SeminormedAddCommGroup.toIsTopologicalAddGroup edist_def dist_def MeasureTheory.eLpNorm_congr_ae coeFn_sub ENNReal.ofReal_toReal eLpNorm_ne_top
edist_toLp_toLp 📖	mathematical	MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace	EDist.edist MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp instEDist MeasureTheory.MemLp.toLp MeasureTheory.eLpNorm Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	SeminormedAddCommGroup.toIsTopologicalAddGroup edist_def MeasureTheory.eLpNorm_congr_ae Filter.EventuallyEq.sub MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.MemLp.coeFn_toLp
edist_toLp_zero 📖	mathematical	MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace	EDist.edist MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp instEDist MeasureTheory.MemLp.toLp AddSubgroup.zero MeasureTheory.eLpNorm	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.MemLp.zero sub_zero edist_toLp_toLp
enorm_def 📖	mathematical	—	ENorm.enorm 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 NNNorm.toENorm instNNNorm MeasureTheory.eLpNorm ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddGroup.toContinuousENorm MeasureTheory.AEEqFun.cast	—	SeminormedAddCommGroup.toIsTopologicalAddGroup ENNReal.coe_toNNReal eLpNorm_ne_top
enorm_toLp 📖	mathematical	MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace	ENorm.enorm MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp NNNorm.toENorm instNNNorm MeasureTheory.MemLp.toLp MeasureTheory.eLpNorm	—	SeminormedAddCommGroup.toIsTopologicalAddGroup nnnorm_toLp ENNReal.coe_toNNReal LT.lt.ne
eq_zero_iff_ae_eq_zero 📖	mathematical	—	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.zero Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.AEEqFun.cast Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.Measure.instOuterMeasureClass memLp MeasureTheory.MemLp.zero MeasureTheory.MemLp.toLp_eq_toLp_iff MeasureTheory.MemLp.toLp_zero toLp_coeFn
ext 📖	—	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.AEEqFun.cast UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp	—	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.AEEqFun.ext
ext_iff 📖	mathematical	—	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.AEEqFun.cast UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.Measure.instOuterMeasureClass Filter.EventuallyEq.refl ext
instIsBoundedSMul 📖	mathematical	—	IsBoundedSMul 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 SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing instNormedAddCommGroup MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing AddSubgroup.zero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid instModule	—	IsBoundedSMul.of_enorm_smul_le SeminormedAddCommGroup.toIsTopologicalAddGroup enorm_def MeasureTheory.eLpNorm_congr_ae coeFn_smul MeasureTheory.eLpNorm_const_smul_le
instIsCentralScalar 📖	mathematical	—	IsCentralScalar 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 SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup MeasureTheory.AEEqFun.instAddCommGroup NormedAddCommGroup.toAddCommGroup instModule MulOpposite MulOpposite.instMonoid MulOpposite.instSemiring MulOpposite.instNormedRing	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsCentralScalar.op_smul_eq_smul UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul ContinuousConstSMul.op MeasureTheory.AEEqFun.instIsCentralScalar
instIsScalarTower 📖	mathematical	—	IsScalarTower 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 SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup MeasureTheory.AEEqFun.instAddCommGroup NormedAddCommGroup.toAddCommGroup instModule	—	SeminormedAddCommGroup.toIsTopologicalAddGroup smul_assoc UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul MeasureTheory.AEEqFun.instIsScalarTower
instSMulCommClass 📖	mathematical	—	SMulCommClass 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 SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup MeasureTheory.AEEqFun.instAddCommGroup NormedAddCommGroup.toAddCommGroup instModule	—	SeminormedAddCommGroup.toIsTopologicalAddGroup SMulCommClass.smul_comm UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul MeasureTheory.AEEqFun.instSMulCommClass
instTrivialStarSubtypeAEEqFunMemAddSubgroup 📖	mathematical	—	TrivialStar 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 instStarSubtypeAEEqFunMemAddSubgroup	—	SeminormedAddCommGroup.toIsTopologicalAddGroup TrivialStar.star_trivial MeasureTheory.AEEqFun.instTrivialStar
isometry_compMeasurePreserving 📖	mathematical	MeasureTheory.MeasurePreserving	Isometry 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 EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace instNormedAddCommGroup DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddMonoidHom.instFunLike compMeasurePreserving	—	AddMonoidHomClass.isometry_of_norm SeminormedAddCommGroup.toIsTopologicalAddGroup AddMonoidHom.instAddMonoidHomClass norm_compMeasurePreserving
lipschitzWith_pos_part 📖	mathematical	—	LipschitzWith Real EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace Real.metricSpace NNReal instOneNNReal Real.instMax Real.instZero	—	LipschitzWith.max_const LipschitzWith.id
meas_ge_le_mul_pow_enorm 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike setOf ENNReal.ofNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.AEEqFun.cast UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Real ENNReal.instPowReal ENNReal.instInv ENNReal.toReal ENNReal.ofReal Norm.norm SeminormedAddCommGroup.toIsTopologicalAddGroup instNorm	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.meas_ge_le_mul_pow_eLpNorm_enorm aestronglyMeasurable MeasureTheory.measure_empty MeasureTheory.Measure.instOuterMeasureClass ENNReal.ofReal_toReal eLpNorm_ne_top
memLp 📖	mathematical	—	MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace MeasureTheory.AEEqFun.cast MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp	—	SeminormedAddCommGroup.toIsTopologicalAddGroup aestronglyMeasurable Subtype.prop
mem_Lp_iff_eLpNorm_lt_top 📖	mathematical	—	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 ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder MeasureTheory.eLpNorm ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddGroup.toContinuousENorm MeasureTheory.AEEqFun.cast Top.top instTopENNReal	—	SeminormedAddCommGroup.toIsTopologicalAddGroup
mem_Lp_iff_memLp 📖	mathematical	—	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 MeasureTheory.MemLp ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddGroup.toContinuousENorm MeasureTheory.AEEqFun.cast	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.StronglyMeasurable.aestronglyMeasurable MeasureTheory.AEEqFun.stronglyMeasurable
mem_Lp_of_ae_bound 📖	mathematical	Filter.Eventually Real Real.instLE Norm.norm NormedAddCommGroup.toNorm MeasureTheory.AEEqFun.cast UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp	—	MeasureTheory.Measure.instOuterMeasureClass SeminormedAddCommGroup.toIsTopologicalAddGroup mem_Lp_iff_memLp MeasureTheory.MemLp.of_bound MeasureTheory.AEEqFun.aestronglyMeasurable
mem_Lp_of_ae_le 📖	mathematical	Filter.Eventually Real Real.instLE Norm.norm NormedAddCommGroup.toNorm MeasureTheory.AEEqFun.cast UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	SeminormedAddCommGroup.toIsTopologicalAddGroup	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.Measure.instOuterMeasureClass mem_Lp_of_nnnorm_ae_le
mem_Lp_of_ae_le_mul 📖	mathematical	Filter.Eventually Real Real.instLE Norm.norm NormedAddCommGroup.toNorm MeasureTheory.AEEqFun.cast UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.instMul MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	SeminormedAddCommGroup.toIsTopologicalAddGroup	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.Measure.instOuterMeasureClass mem_Lp_iff_memLp MeasureTheory.MemLp.of_le_mul memLp MeasureTheory.AEEqFun.aestronglyMeasurable
mem_Lp_of_ae_nnnorm_bound 📖	mathematical	Filter.Eventually NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.AEEqFun.cast UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp	—	MeasureTheory.Measure.instOuterMeasureClass SeminormedAddCommGroup.toIsTopologicalAddGroup mem_Lp_iff_memLp MeasureTheory.MemLp.of_bound MeasureTheory.AEEqFun.aestronglyMeasurable
mem_Lp_of_nnnorm_ae_le 📖	mathematical	Filter.Eventually NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.AEEqFun.cast UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	SeminormedAddCommGroup.toIsTopologicalAddGroup	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.Measure.instOuterMeasureClass mem_Lp_iff_memLp MeasureTheory.MemLp.of_le memLp MeasureTheory.AEEqFun.aestronglyMeasurable
mem_Lp_of_nnnorm_ae_le_mul 📖	mathematical	Filter.Eventually NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.AEEqFun.cast UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	SeminormedAddCommGroup.toIsTopologicalAddGroup	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.Measure.instOuterMeasureClass mem_Lp_iff_memLp MeasureTheory.MemLp.of_nnnorm_le_mul memLp MeasureTheory.AEEqFun.aestronglyMeasurable
mul_meas_ge_le_pow_enorm 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike setOf Real ENNReal.instPowReal ENorm.enorm ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm MeasureTheory.AEEqFun.cast SeminormedAddCommGroup.toPseudoMetricSpace MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp ENNReal.toReal ENNReal.ofReal Norm.norm SeminormedAddCommGroup.toIsTopologicalAddGroup instNorm	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.mul_meas_ge_le_pow_eLpNorm aestronglyMeasurable ENNReal.ofReal_toReal eLpNorm_ne_top
mul_meas_ge_le_pow_enorm' 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Real ENNReal.instPowReal ENNReal.toReal DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike setOf ENNReal.ofNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.AEEqFun.cast UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp ENNReal.ofReal Norm.norm SeminormedAddCommGroup.toIsTopologicalAddGroup instNorm	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.mul_meas_ge_le_pow_eLpNorm' aestronglyMeasurable ENNReal.ofReal_toReal eLpNorm_ne_top
nnnorm_def 📖	mathematical	—	NNNorm.nnnorm 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 instNNNorm ENNReal.toNNReal MeasureTheory.eLpNorm ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddGroup.toContinuousENorm MeasureTheory.AEEqFun.cast	—	SeminormedAddCommGroup.toIsTopologicalAddGroup
nnnorm_eq_zero_iff 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal	NNNorm.nnnorm 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 instNNNorm NNReal instZeroNNReal AddSubgroup.zero	—	SeminormedAddCommGroup.toIsTopologicalAddGroup ENNReal.toNNReal_eq_zero_iff nnnorm_def MeasureTheory.AEEqFun.ext Filter.EventuallyEq.trans MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.eLpNorm_eq_zero_iff aestronglyMeasurable LT.lt.ne Filter.EventuallyEq.symm MeasureTheory.AEEqFun.coeFn_zero eLpNorm_ne_top nnnorm_zero
nnnorm_le_mul_nnnorm_of_ae_le_mul 📖	mathematical	Filter.Eventually NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.AEEqFun.cast UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	SeminormedAddCommGroup.toIsTopologicalAddGroup instNNNorm	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul ENNReal.toNNReal_coe ENNReal.toNNReal_mul smul_eq_mul ENNReal.smul_def ENNReal.toNNReal_le_toNNReal eLpNorm_ne_top ENNReal.mul_ne_top ENNReal.coe_ne_top
nnnorm_le_of_ae_bound 📖	mathematical	Filter.Eventually NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.AEEqFun.cast UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	SeminormedAddCommGroup.toIsTopologicalAddGroup instNNNorm Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal Real NNReal.instPowReal MeasureTheory.measureUnivNNReal Real.instInv ENNReal.toReal	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.eLpNorm_measure_zero NNReal.rpow_zero one_mul NNReal.instCanonicallyOrderedAdd ENNReal.coe_le_coe nnnorm_def ENNReal.coe_toNNReal eLpNorm_ne_top LE.le.trans_eq MeasureTheory.eLpNorm_le_of_ae_nnnorm_bound MeasureTheory.coe_measureUnivNNReal ENNReal.coe_rpow_of_ne_zero LT.lt.ne' MeasureTheory.measureUnivNNReal_pos ENNReal.coe_mul mul_comm ENNReal.smul_def smul_eq_mul
nnnorm_neg 📖	mathematical	—	NNNorm.nnnorm 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 instNNNorm AddSubgroup.neg	—	SeminormedAddCommGroup.toIsTopologicalAddGroup nnnorm_def MeasureTheory.eLpNorm_congr_ae coeFn_neg MeasureTheory.eLpNorm_neg
nnnorm_toLp 📖	mathematical	MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace	NNNorm.nnnorm MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp instNNNorm MeasureTheory.MemLp.toLp ENNReal.toNNReal MeasureTheory.eLpNorm	—	NNReal.eq SeminormedAddCommGroup.toIsTopologicalAddGroup norm_toLp
nnnorm_zero 📖	mathematical	—	NNNorm.nnnorm 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 instNNNorm AddSubgroup.zero NNReal instZeroNNReal	—	SeminormedAddCommGroup.toIsTopologicalAddGroup nnnorm_def MeasureTheory.eLpNorm_congr_ae MeasureTheory.AEEqFun.coeFn_zero MeasureTheory.eLpNorm_zero
norm_compMeasurePreserving 📖	mathematical	MeasureTheory.MeasurePreserving	Norm.norm 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 instNorm DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddMonoidHom.instFunLike compMeasurePreserving	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.AEEqFun.eLpNorm_compMeasurePreserving
norm_def 📖	mathematical	—	Norm.norm 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 instNorm ENNReal.toReal MeasureTheory.eLpNorm ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddGroup.toContinuousENorm MeasureTheory.AEEqFun.cast	—	SeminormedAddCommGroup.toIsTopologicalAddGroup
norm_eq_zero_iff 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal	Norm.norm 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 instNorm Real Real.instZero AddSubgroup.zero	—	SeminormedAddCommGroup.toIsTopologicalAddGroup NNReal.coe_eq_zero nnnorm_eq_zero_iff
norm_exponent_zero 📖	mathematical	—	Norm.norm 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 ENNReal instZeroENNReal instNorm Real Real.instZero	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.eLpNorm_exponent_zero
norm_le_mul_norm_of_ae_le_mul 📖	mathematical	Filter.Eventually Real Real.instLE Norm.norm NormedAddCommGroup.toNorm MeasureTheory.AEEqFun.cast UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp Real.instMul MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	SeminormedAddCommGroup.toIsTopologicalAddGroup instNorm	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.Measure.instOuterMeasureClass le_or_gt CanLift.prf NNReal.canLift NNReal.coe_le_coe nnnorm_le_mul_nnnorm_of_ae_le_mul MeasureTheory.eLpNorm_eq_zero_and_zero_of_ae_le_mul_neg MulZeroClass.mul_zero
norm_le_norm_of_ae_le 📖	mathematical	Filter.Eventually Real Real.instLE Norm.norm NormedAddCommGroup.toNorm MeasureTheory.AEEqFun.cast UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	SeminormedAddCommGroup.toIsTopologicalAddGroup instNorm	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.Measure.instOuterMeasureClass norm_def ENNReal.toReal_mono eLpNorm_ne_top MeasureTheory.eLpNorm_mono_ae
norm_le_of_ae_bound 📖	mathematical	Real Real.instLE Real.instZero Filter.Eventually Norm.norm NormedAddCommGroup.toNorm MeasureTheory.AEEqFun.cast UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	SeminormedAddCommGroup.toIsTopologicalAddGroup instNorm Real.instMul Real.instPow NNReal.toReal MeasureTheory.measureUnivNNReal Real.instInv ENNReal.toReal	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.Measure.instOuterMeasureClass CanLift.prf NNReal.canLift nnnorm_le_of_ae_bound NNReal.coe_rpow NNReal.coe_mul NNReal.coe_le_coe
norm_measure_zero 📖	mathematical	—	Norm.norm MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.Measure MeasureTheory.Measure.instZero AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp instNorm Real Real.instZero	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.eLpNorm_measure_zero
norm_neg 📖	mathematical	—	Norm.norm 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 instNorm AddSubgroup.neg	—	SeminormedAddCommGroup.toIsTopologicalAddGroup nnnorm_neg
norm_toLp 📖	mathematical	MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace	Norm.norm MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp instNorm MeasureTheory.MemLp.toLp ENNReal.toReal MeasureTheory.eLpNorm	—	SeminormedAddCommGroup.toIsTopologicalAddGroup norm_def MeasureTheory.eLpNorm_congr_ae MeasureTheory.MemLp.coeFn_toLp
norm_zero 📖	mathematical	—	Norm.norm 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 instNorm AddSubgroup.zero Real Real.instZero	—	SeminormedAddCommGroup.toIsTopologicalAddGroup nnnorm_zero
pow_mul_meas_ge_le_enorm 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder Real ENNReal.instPowReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike setOf ENorm.enorm ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm MeasureTheory.AEEqFun.cast SeminormedAddCommGroup.toPseudoMetricSpace MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp ENNReal.toReal DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne ENNReal.ofReal Norm.norm SeminormedAddCommGroup.toIsTopologicalAddGroup instNorm	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.pow_mul_meas_ge_le_eLpNorm aestronglyMeasurable ENNReal.ofReal_toReal eLpNorm_ne_top
stronglyMeasurable 📖	mathematical	—	MeasureTheory.StronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.AEEqFun.cast MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.AEEqFun.stronglyMeasurable
toLp_coeFn 📖	mathematical	MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace MeasureTheory.AEEqFun.cast MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp	MeasureTheory.MemLp.toLp	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.MemLp.eLpNorm_mk_lt_top MeasureTheory.AEEqFun.mk_coeFn Subtype.coe_eta
toLp_compMeasurePreserving 📖	mathematical	MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace MeasureTheory.MeasurePreserving	DFunLike.coe AddMonoidHom MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddMonoidHom.instFunLike compMeasurePreserving MeasureTheory.MemLp.toLp MeasureTheory.MemLp.comp_measurePreserving	—	SeminormedAddCommGroup.toIsTopologicalAddGroup

MeasureTheory.MemLp

Definitions

Name	Category	Theorems
toLp 📖	CompOp	37 math math: MeasureTheory.Lp.tendsto_Lp_iff_tendsto_eLpNorm'', toLp_val, toLp_eq_toLp_iff, MeasureTheory.Lp.enorm_toLp, condExpL2_ae_eq_condExp, MeasureTheory.Lp.edist_toLp_toLp, MeasureTheory.Lp.edist_toLp_zero, MeasureTheory.Lp.norm_toLp, DomMulAct.mk_smul_toLp, MeasureTheory.Lp.nnnorm_toLp, MeasureTheory.Lp.simpleFunc.toLp_eq_toLp, MeasureTheory.Lp_toLp_restrict_add, toLp_neg, toLp_congr, MeasureTheory.mem_lpMeasSubgroup_toLp_of_trim, StrongDual.toLpₗ_apply, MeasureTheory.Lp.toLp_coeFn, MeasureTheory.Lp.tendsto_Lp_of_tendsto_eLpNorm, DomAddAct.mk_vadd_toLp, condExpL2_ae_eq_condExp', MeasureTheory.Lp.smul_def, MeasureTheory.withDensitySMulLI_apply, coeFn_toLp, toLp_add, StrongDual.toLp_apply, MeasureTheory.norm_Lp_toLp_restrict_le, MeasureTheory.Lp.toLp_compMeasurePreserving, toLp_zero, MeasureTheory.SimpleFunc.tendsto_approxOn_range_Lp, MeasureTheory.lpMeasToLpTrimLie_symm_toLp, MeasureTheory.Lp.tendsto_Lp_iff_tendsto_eLpNorm, toLp_const_smul, MeasureTheory.condExpL2_const_inner, MeasureTheory.Lp.toTemperedDistribution_smul_eq, MeasureTheory.Lp_toLp_restrict_smul, toLp_sub, toLp_const

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeFn_toLp 📖	mathematical	MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace	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 SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp toLp	—	—
continuousLinearMap_comp 📖	mathematical	MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.funLike	—	LipschitzWith.comp_memLp RingHomIsometric.ids ContinuousLinearMap.lipschitz map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass
eLpNorm_mk_lt_top 📖	mathematical	MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder MeasureTheory.eLpNorm MeasureTheory.AEEqFun.cast MeasureTheory.AEStronglyMeasurable Top.top instTopENNReal	—	MeasureTheory.eLpNorm_aeeqFun
enorm_rpow 📖	mathematical	MeasureTheory.MemLp ContinuousENorm.toENorm	ENNReal instENormENNReal ENNReal.instTopologicalSpace Real ENNReal.instPowReal ENorm.enorm ENNReal.toReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	div_eq_mul_inv ENNReal.mul_inv_cancel enorm_rpow_div
enorm_rpow_div 📖	mathematical	MeasureTheory.MemLp ContinuousENorm.toENorm	ENNReal instENormENNReal ENNReal.instTopologicalSpace Real ENNReal.instPowReal ENorm.enorm ENNReal.toReal DivInvMonoid.toDiv ENNReal.instDivInvMonoid	—	AEMeasurable.aestronglyMeasurable TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace ENNReal.instMetrizableSpace BorelSpace.opensMeasurable ENNReal.borelSpace ENNReal.instSecondCountableTopology AEMeasurable.pow_const ENNReal.hasMeasurablePow MeasureTheory.AEStronglyMeasurable.enorm ENNReal.rpow_zero ENNReal.div_top MeasureTheory.eLpNorm_exponent_zero ENNReal.zero_div ENNReal.div_zero MeasureTheory.eLpNorm_exponent_top MeasureTheory.memLp_top_const_enorm MeasureTheory.eLpNorm_enorm_rpow ENNReal.toReal_pos ENNReal.rpow_lt_top_of_nonneg ENNReal.toReal_nonneg ENNReal.ofReal_toReal div_eq_mul_inv mul_assoc ENNReal.inv_mul_cancel mul_one LT.lt.ne
neg_part 📖	mathematical	MeasureTheory.MemLp Real ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SeminormedAddGroup.toContinuousENorm Real.pseudoMetricSpace	Real.instMax Real.instNeg Real.instZero	—	LipschitzWith.comp_memLp MeasureTheory.Lp.lipschitzWith_pos_part max_eq_right le_rfl neg
norm_rpow 📖	mathematical	MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace	Real NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Real.pseudoMetricSpace Real.instPow Norm.norm NormedAddCommGroup.toNorm ENNReal.toReal ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	div_eq_mul_inv ENNReal.mul_inv_cancel norm_rpow_div
norm_rpow_div 📖	mathematical	MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace	Real NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Real.pseudoMetricSpace Real.instPow Norm.norm NormedAddCommGroup.toNorm ENNReal.toReal ENNReal DivInvMonoid.toDiv ENNReal.instDivInvMonoid	—	AEMeasurable.aestronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace BorelSpace.opensMeasurable Real.borelSpace instSecondCountableTopologyReal AEMeasurable.pow_const Real.hasMeasurablePow MeasureTheory.AEStronglyMeasurable.aemeasurable MeasureTheory.AEStronglyMeasurable.norm Real.rpow_zero ENNReal.div_top MeasureTheory.eLpNorm_exponent_zero ENNReal.zero_div ENNReal.div_zero MeasureTheory.memLp_top_const MeasureTheory.eLpNorm_norm_rpow ENNReal.toReal_pos ENNReal.rpow_lt_top_of_nonneg ENNReal.toReal_nonneg ENNReal.ofReal_toReal div_eq_mul_inv mul_assoc ENNReal.inv_mul_cancel mul_one LT.lt.ne
ofReal 📖	mathematical	MeasureTheory.MemLp Real ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SeminormedAddGroup.toContinuousENorm Real.pseudoMetricSpace	NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing RCLike.ofReal	—	ContinuousLinearMap.comp_memLp' RingHomIsometric.ids
of_comp_antilipschitzWith 📖	—	MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace UniformContinuous AntilipschitzWith EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	—	dist_zero_right AntilipschitzWith.le_mul_dist Topology.IsEmbedding.aestronglyMeasurable_comp_iff PseudoEMetricSpace.pseudoMetrizableSpace IsUniformEmbedding.isEmbedding AntilipschitzWith.isUniformEmbedding of_le_mul Filter.Eventually.of_forall MeasureTheory.Measure.instOuterMeasureClass
pos_part 📖	mathematical	MeasureTheory.MemLp Real ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SeminormedAddGroup.toContinuousENorm Real.pseudoMetricSpace	Real.instMax Real.instZero	—	LipschitzWith.comp_memLp MeasureTheory.Lp.lipschitzWith_pos_part max_eq_right le_rfl
toLp_add 📖	mathematical	MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace	toLp Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid add ESeminormedAddCommMonoid.toESeminormedAddMonoid IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp AddSubgroup.add	—	SeminormedAddCommGroup.toIsTopologicalAddGroup add IsTopologicalAddGroup.toContinuousAdd
toLp_congr 📖	mathematical	MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	toLp	—	MeasureTheory.Measure.instOuterMeasureClass eLpNorm_mk_lt_top
toLp_const_smul 📖	mathematical	MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace	toLp Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid const_smul Module.toMulActionWithZero MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup MeasureTheory.AEEqFun.instAddCommGroup NormedAddCommGroup.toAddCommGroup MeasureTheory.Lp.instModule	—	SeminormedAddCommGroup.toIsTopologicalAddGroup const_smul
toLp_eq_toLp_iff 📖	mathematical	MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace	toLp Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.Measure.instOuterMeasureClass eLpNorm_mk_lt_top
toLp_neg 📖	mathematical	MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace	toLp Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup neg MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp AddSubgroup.neg	—	SeminormedAddCommGroup.toIsTopologicalAddGroup neg
toLp_sub 📖	mathematical	MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace	toLp Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup sub MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp AddSubgroup.sub	—	SeminormedAddCommGroup.toIsTopologicalAddGroup sub
toLp_val 📖	mathematical	MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace	MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp toLp MeasureTheory.AEStronglyMeasurable ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder MeasureTheory.eLpNorm Top.top instTopENNReal	—	SeminormedAddCommGroup.toIsTopologicalAddGroup
toLp_zero 📖	mathematical	MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	toLp MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp AddSubgroup.zero	—	SeminormedAddCommGroup.toIsTopologicalAddGroup

---

← Back to Index