CompareExp

📁 Source: Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean

Statistics

Metric	Count
Definitions	0
Theorems mono_exponent, mono_exponent_of_measure_support_ne_top, mul, mul', of_bilin, prod, prod', smul, eLpNorm'_le_eLpNorm'_mul_eLpNorm', eLpNorm'_le_eLpNorm'_mul_rpow_measure_univ, eLpNorm'_le_eLpNorm'_of_exponent_le, eLpNorm'_le_eLpNormEssSup, eLpNorm'_le_eLpNormEssSup_mul_rpow_measure_univ, eLpNorm'_lt_top_of_eLpNorm'_lt_top_of_exponent_le, eLpNorm'_smul_le_mul_eLpNorm', eLpNorm_le_eLpNorm_mul_eLpNorm'_of_norm, eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm, eLpNorm_le_eLpNorm_mul_eLpNorm_top, eLpNorm_le_eLpNorm_mul_rpow_measure_univ, eLpNorm_le_eLpNorm_of_exponent_le, eLpNorm_le_eLpNorm_top_mul_eLpNorm, eLpNorm_smul_le_eLpNorm_mul_eLpNorm_top, eLpNorm_smul_le_eLpNorm_top_mul_eLpNorm, eLpNorm_smul_le_mul_eLpNorm	24
Total	24

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eLpNorm'_le_eLpNorm'_mul_eLpNorm' 📖	mathematical	AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Filter.Eventually NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal ae Measure Measure.instFunLike Measure.instOuterMeasureClass Real Real.instLT Real.instZero DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne Real.instAdd	ENNReal ENNReal.instPartialOrder eLpNorm' ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddGroup.toContinuousENorm CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofNNReal	—	Measure.instOuterMeasureClass ENNReal.rpow_le_rpow lintegral_mono_ae Filter.Eventually.mono nnnorm_mul NormedDivisionRing.toNormMulClass NNReal.nnnorm_eq nnnorm_norm le_of_lt div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one smul_mul_assoc IsScalarTower.right eLpNorm'_const_smul NormedSpace.toNormSMulClass Real.enorm_eq_ofReal NNReal.coe_nonneg ENNReal.ofReal_coe_nnreal mul_assoc mul_le_mul_right IsOrderedMonoid.toMulLeftMono ENNReal.instIsOrderedMonoid enorm_mul enorm_norm ENNReal.lintegral_Lp_mul_le_Lq_mul_Lr AEStronglyMeasurable.enorm
eLpNorm'_le_eLpNorm'_mul_rpow_measure_univ 📖	mathematical	Real Real.instLT Real.instZero Real.instLE AEStronglyMeasurable	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder eLpNorm' ContinuousENorm.toENorm Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instPowReal DFunLike.coe Measure Set Measure.instFunLike Set.univ Real.instSub DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne	—	lt_of_lt_of_le sub_self ENNReal.rpow_zero mul_one le_refl lt_of_le_of_ne lintegral_congr eLpNorm'_eq_lintegral_enorm one_div Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg ne_of_gt Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial add_sub_cancel ENNReal.lintegral_Lp_mul_le_Lq_mul_Lr AEStronglyMeasurable.enorm aemeasurable_const ENNReal.one_rpow lintegral_const inv_div add_sub_cancel_left
eLpNorm'_le_eLpNorm'_of_exponent_le 📖	mathematical	Real Real.instLT Real.instZero Real.instLE AEStronglyMeasurable	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder eLpNorm' ContinuousENorm.toENorm	—	eLpNorm'_le_eLpNorm'_mul_rpow_measure_univ mul_one ENNReal.one_rpow IsProbabilityMeasure.measure_univ
eLpNorm'_le_eLpNormEssSup 📖	mathematical	Real Real.instLT Real.instZero	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder eLpNorm' ContinuousENorm.toENorm eLpNormEssSup	—	LE.le.trans_eq eLpNorm'_le_eLpNormEssSup_mul_rpow_measure_univ IsProbabilityMeasure.measure_univ one_div ENNReal.one_rpow mul_one
eLpNorm'_le_eLpNormEssSup_mul_rpow_measure_univ 📖	mathematical	Real Real.instLT Real.instZero	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder eLpNorm' ContinuousENorm.toENorm Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring eLpNormEssSup ENNReal.instPowReal DFunLike.coe Measure Set Measure.instFunLike Set.univ DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne	—	lintegral_mono_ae Measure.instOuterMeasureClass enorm_ae_le_eLpNormEssSup Filter.Eventually.mono ENNReal.rpow_le_rpow le_of_lt eLpNorm'.eq_1 ENNReal.rpow_one mul_inv_cancel₀ ne_of_lt ENNReal.rpow_mul one_div ENNReal.mul_rpow_of_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing LT.lt.le lintegral_const inv_pos_of_pos
eLpNorm'_lt_top_of_eLpNorm'_lt_top_of_exponent_le 📖	—	AEStronglyMeasurable ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder eLpNorm' ContinuousENorm.toENorm Top.top instTopENNReal Real Real.instLE Real.instZero	—	—	le_or_gt le_antisymm eLpNorm'_exponent_zero lt_of_lt_of_le eLpNorm'_le_eLpNorm'_mul_rpow_measure_univ ENNReal.mul_lt_top_iff ENNReal.rpow_lt_top_of_nonneg le_sub_comm IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid sub_zero one_div inv_le_inv₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono measure_ne_top
eLpNorm'_smul_le_mul_eLpNorm' 📖	mathematical	AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing Real Real.instLT Real.instZero DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne Real.instAdd	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder eLpNorm' ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddGroup.toContinuousENorm Pi.smul' SMulZeroClass.toSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup SMulWithZero.toSMulZeroClass MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing MulActionWithZero.toSMulWithZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing	—	one_mul eLpNorm'_le_eLpNorm'_mul_eLpNorm' Filter.Eventually.of_forall Measure.instOuterMeasureClass nnnorm_smul_le
eLpNorm_le_eLpNorm_mul_eLpNorm'_of_norm 📖	mathematical	AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Filter.Eventually Real Real.instLE Norm.norm NormedAddCommGroup.toNorm Real.instMul NNReal.toReal ae Measure Measure.instFunLike Measure.instOuterMeasureClass	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder eLpNorm ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddGroup.toContinuousENorm Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofNNReal	—	Measure.instOuterMeasureClass eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm
eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm 📖	mathematical	AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Filter.Eventually NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal ae Measure Measure.instFunLike Measure.instOuterMeasureClass	ENNReal ENNReal.instPartialOrder eLpNorm ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddGroup.toContinuousENorm CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofNNReal	—	Measure.instOuterMeasureClass ENNReal.HolderTriple.one_div_eq ENNReal.trichotomy one_div ENNReal.inv_zero top_add eLpNorm_exponent_zero MulZeroClass.mul_zero MulZeroClass.zero_mul ENNReal.inv_top zero_add eLpNorm_le_eLpNorm_top_mul_eLpNorm add_top add_zero eLpNorm_le_eLpNorm_mul_eLpNorm_top ENNReal.toReal_pos_iff ENNReal.toReal_inv ENNReal.toReal_add LT.lt.ne' one_div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing add_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid div_pos Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one lt_of_one_div_lt_one_div lt_add_of_pos_right IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd eLpNorm_eq_eLpNorm' ne_of_gt ne_top_of_lt eLpNorm'_le_eLpNorm'_mul_eLpNorm'
eLpNorm_le_eLpNorm_mul_eLpNorm_top 📖	mathematical	AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Filter.Eventually NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal ae Measure Measure.instFunLike Measure.instOuterMeasureClass	ENNReal ENNReal.instPartialOrder eLpNorm ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddGroup.toContinuousENorm CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofNNReal Top.top instTopENNReal	—	Measure.instOuterMeasureClass eLpNorm_le_eLpNorm_top_mul_eLpNorm mul_assoc mul_comm
eLpNorm_le_eLpNorm_mul_rpow_measure_univ 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder AEStronglyMeasurable	eLpNorm ContinuousENorm.toENorm Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Real ENNReal.instPowReal DFunLike.coe Measure Set Measure.instFunLike Set.univ Real.instSub DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne ENNReal.toReal	—	eLpNorm_exponent_zero div_zero one_div zero_sub ENNReal.instCanonicallyOrderedAdd lt_of_le_of_ne zero_le lt_of_lt_of_le eLpNorm_exponent_top sub_zero inv_zero ENNReal.rpow_zero mul_one eLpNorm_eq_eLpNorm' ENNReal.toReal_pos LT.lt.ne' LE.le.trans eLpNorm'_le_eLpNormEssSup_mul_rpow_measure_univ le_of_eq LE.le.trans_lt lt_top_iff_ne_top LT.lt.ne ENNReal.toReal_mono eLpNorm'_le_eLpNorm'_mul_rpow_measure_univ
eLpNorm_le_eLpNorm_of_exponent_le 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder AEStronglyMeasurable	eLpNorm ContinuousENorm.toENorm	—	LE.le.trans eLpNorm_le_eLpNorm_mul_rpow_measure_univ le_of_eq IsProbabilityMeasure.measure_univ one_div ENNReal.one_rpow mul_one
eLpNorm_le_eLpNorm_top_mul_eLpNorm 📖	mathematical	AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Filter.Eventually NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal ae Measure Measure.instFunLike Measure.instOuterMeasureClass	ENNReal ENNReal.instPartialOrder eLpNorm ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddGroup.toContinuousENorm CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofNNReal Top.top instTopENNReal	—	Measure.instOuterMeasureClass eLpNorm_mono_ae_real smul_mul_assoc IsScalarTower.right eLpNorm_const_smul NormedSpace.toNormSMulClass Real.enorm_eq_ofReal NNReal.coe_nonneg ENNReal.ofReal_coe_nnreal mul_assoc mul_le_mul_right IsOrderedMonoid.toMulLeftMono ENNReal.instIsOrderedMonoid ENNReal.trichotomy eLpNorm_exponent_zero eLpNorm_exponent_top MulZeroClass.mul_zero eLpNorm_norm enorm_mul NormedDivisionRing.toNormMulClass enorm_norm ENNReal.essSup_mul_le ENNReal.toReal_pos_iff eLpNorm_eq_lintegral_rpow_enorm_toReal LT.lt.ne' LT.lt.ne one_div ENNReal.rpow_inv_le_iff ENNReal.mul_rpow_of_nonneg LT.lt.le ENNReal.rpow_inv_rpow lintegral_const_mul'' AEMeasurable.pow_const ENNReal.hasMeasurablePow AEStronglyMeasurable.enorm lintegral_mono_ae Filter.mp_mem enorm_ae_le_eLpNormEssSup Filter.univ_mem' ENNReal.rpow_le_rpow mul_le_mul_left covariant_swap_mul_of_covariant_mul le_of_lt
eLpNorm_smul_le_eLpNorm_mul_eLpNorm_top 📖	mathematical	AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder eLpNorm ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm Pi.smul' SMulZeroClass.toSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup SMulWithZero.toSMulZeroClass MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing MulActionWithZero.toSMulWithZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing Top.top instTopENNReal	—	eLpNorm_exponent_top one_mul eLpNorm_le_eLpNorm_mul_eLpNorm_top Filter.Eventually.of_forall Measure.instOuterMeasureClass nnnorm_smul_le
eLpNorm_smul_le_eLpNorm_top_mul_eLpNorm 📖	mathematical	AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder eLpNorm ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddGroup.toContinuousENorm Pi.smul' SMulZeroClass.toSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup SMulWithZero.toSMulZeroClass MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing MulActionWithZero.toSMulWithZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing Top.top instTopENNReal	—	eLpNorm_exponent_top one_mul eLpNorm_le_eLpNorm_top_mul_eLpNorm Filter.Eventually.of_forall Measure.instOuterMeasureClass nnnorm_smul_le
eLpNorm_smul_le_mul_eLpNorm 📖	mathematical	AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder eLpNorm ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddGroup.toContinuousENorm Pi.smul' SMulZeroClass.toSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup SMulWithZero.toSMulZeroClass MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing MulActionWithZero.toSMulWithZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing	—	one_mul eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm Filter.Eventually.of_forall Measure.instOuterMeasureClass nnnorm_smul_le

MeasureTheory.MemLp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mono_exponent 📖	—	MeasureTheory.MemLp ContinuousENorm.toENorm ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder	—	—	MeasureTheory.memLp_zero_iff_aestronglyMeasurable top_le_iff ENNReal.toReal_pos MeasureTheory.eLpNorm_eq_eLpNorm' lt_of_le_of_lt MeasureTheory.eLpNorm'_le_eLpNormEssSup_mul_rpow_measure_univ ENNReal.mul_lt_top MeasureTheory.eLpNorm_exponent_top ENNReal.rpow_lt_top_of_nonneg one_div PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing LT.lt.le MeasureTheory.measure_ne_top le_antisymm zero_le ENNReal.instCanonicallyOrderedAdd lt_irrefl ENNReal.toReal_zero ENNReal.toReal_mono MeasureTheory.eLpNorm'_lt_top_of_eLpNorm'_lt_top_of_exponent_le
mono_exponent_of_measure_support_ne_top 📖	—	MeasureTheory.MemLp ContinuousENorm.toENorm ESeminormedAddMonoid.toContinuousENorm AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder	—	—	Set.indicator_eq_self Function.support_subset_iff' Mathlib.Tactic.Contrapose.contrapose₄ MeasureTheory.subset_toMeasurable MeasureTheory.memLp_indicator_iff_restrict MeasureTheory.measurableSet_toMeasurable MeasureTheory.measure_toMeasurable mono_exponent MeasureTheory.Restrict.isFiniteMeasure
mul 📖	mathematical	MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing SeminormedAddGroup.toContinuousENorm SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing	Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing	—	smul NonUnitalSeminormedRing.isBoundedSMul
mul' 📖	mathematical	MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing SeminormedAddGroup.toContinuousENorm SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing	—	smul NonUnitalSeminormedRing.isBoundedSMul
of_bilin 📖	—	MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace MeasureTheory.AEStronglyMeasurable Filter.Eventually NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	—	MeasureTheory.Measure.instOuterMeasureClass LE.le.trans_lt MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm Ne.lt_top ENNReal.mul_ne_top ENNReal.coe_ne_top eLpNorm_ne_top
prod 📖	mathematical	MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing SeminormedAddGroup.toContinuousENorm SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing	Finset.prod Pi.commMonoid CommRing.toCommMonoid NormedCommRing.toCommRing ENNReal ENNReal.instInv Finset.sum ENNReal.instAddCommMonoid	—	Finset.cons_induction ENNReal.inv_zero MeasureTheory.eLpNorm_measure_zero MeasureTheory.eLpNorm_exponent_top MeasureTheory.eLpNormEssSup_const Finset.prod_cons mul Finset.forall_of_forall_cons Finset.mem_cons_self inv_inv Finset.sum_cons
prod' 📖	mathematical	MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing SeminormedAddGroup.toContinuousENorm SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing	Finset.prod CommRing.toCommMonoid NormedCommRing.toCommRing ENNReal ENNReal.instInv Finset.sum ENNReal.instAddCommMonoid	—	Finset.prod_fn prod
smul 📖	mathematical	MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing	Pi.smul' SMulZeroClass.toSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup SMulWithZero.toSMulZeroClass MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing MulActionWithZero.toSMulWithZero	—	MeasureTheory.AEStronglyMeasurable.smul IsBoundedSMul.continuousSMul LE.le.trans_lt MeasureTheory.eLpNorm_smul_le_mul_eLpNorm ENNReal.mul_lt_top eLpNorm_lt_top

---

← Back to Index