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	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Measure Set Measure.instFunLike setOf ENorm.enorm ContinuousENorm.toENorm 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 instReflLe 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 NNReal.instPartialOrder NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup 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 SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup 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	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike setOf Preorder.toLE ENorm.enorm ContinuousENorm.toENorm Top.top instTopENNReal	—	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 ContinuousENorm.toENorm Top.top instTopENNReal	—	meas_ge_lt_top'_enorm instIsEmptyFalse

---

← Back to Index