ChebyshevMarkov

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

Statistics

Metric	Count
Definitions	0
Theorems meas_ge_lt_top, meas_ge_lt_top', meas_ge_lt_top'_enorm, meas_ge_lt_top_enorm, meas_ge_le_mul_pow_eLpNorm_enorm, mul_meas_ge_le_pow_eLpNorm, mul_meas_ge_le_pow_eLpNorm', pow_mul_meas_ge_le_eLpNorm	8
Total	8

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
meas_ge_le_mul_pow_eLpNorm_enorm 📖	mathematical	AEStronglyMeasurable DFunLike.coe Measure Set ENNReal Measure.instFunLike setOf ENorm.enorm ContinuousENorm.toENorm Top.top instTopENNReal instZeroENNReal	Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Real ENNReal.instPowReal ENNReal.instInv ENNReal.toReal eLpNorm	—	ENNReal.zero_rpow_of_pos ENNReal.toReal_pos ENNReal.inv_top MulZeroClass.zero_mul LT.lt.ne ENNReal.rpow_pos pos_iff_ne_zero ENNReal.instCanonicallyOrderedAdd ENNReal.rpow_ne_top_of_nonneg' lt_of_le_of_ne' zero_le ENNReal.inv_rpow ENNReal.mul_le_mul_iff_right mul_assoc ENNReal.mul_inv_cancel one_mul mul_meas_ge_le_pow_eLpNorm'
mul_meas_ge_le_pow_eLpNorm 📖	mathematical	AEStronglyMeasurable	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring DFunLike.coe Measure Set Measure.instFunLike setOf Real ENNReal.instPowReal ENorm.enorm ContinuousENorm.toENorm ENNReal.toReal eLpNorm	—	one_div_mul_cancel ENNReal.toReal_eq_zero_iff ENNReal.rpow_one ENNReal.rpow_mul ENNReal.rpow_le_rpow pow_mul_meas_ge_le_eLpNorm ENNReal.toReal_nonneg
mul_meas_ge_le_pow_eLpNorm' 📖	mathematical	AEStronglyMeasurable	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 Measure Set Measure.instFunLike setOf ENorm.enorm ContinuousENorm.toENorm eLpNorm	—	ENNReal.rpow_le_rpow_iff ENNReal.toReal_pos mul_meas_ge_le_pow_eLpNorm
pow_mul_meas_ge_le_eLpNorm 📖	mathematical	AEStronglyMeasurable	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder Real ENNReal.instPowReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring DFunLike.coe Measure Set Measure.instFunLike setOf ENorm.enorm ContinuousENorm.toENorm ENNReal.toReal DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne eLpNorm	—	eLpNorm_eq_lintegral_rpow_enorm_toReal ENNReal.rpow_le_rpow mul_meas_ge_le_lintegral₀ AEMeasurable.pow_const ENNReal.hasMeasurablePow AEStronglyMeasurable.enorm Mathlib.Meta.Positivity.div_nonneg_of_pos_of_nonneg 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 ENNReal.toReal_nonneg

MeasureTheory.MemLp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
meas_ge_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 DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike setOf NNReal Preorder.toLE instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm Top.top instTopENNReal	—	meas_ge_lt_top'
meas_ge_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 DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike setOf Preorder.toLE ENNReal.ofNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm Top.top instTopENNReal	—	MeasureTheory.measure_empty MeasureTheory.Measure.instOuterMeasureClass meas_ge_lt_top'_enorm
meas_ge_lt_top'_enorm 📖	mathematical	MeasureTheory.MemLp ContinuousENorm.toENorm DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike setOf ENorm.enorm Top.top instTopENNReal instZeroENNReal	Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder Preorder.toLE	—	LE.le.trans_lt MeasureTheory.meas_ge_le_mul_pow_eLpNorm_enorm aestronglyMeasurable ENNReal.mul_lt_top LT.lt.ne eLpNorm_lt_top
meas_ge_lt_top_enorm 📖	mathematical	MeasureTheory.MemLp ContinuousENorm.toENorm	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike setOf Preorder.toLE ENNReal.ofNNReal ENorm.enorm Top.top instTopENNReal	—	meas_ge_lt_top'_enorm instIsEmptyFalse

---

← Back to Index