Markov

📁 Source: Mathlib/MeasureTheory/Integral/Lebesgue/Markov.lean

Statistics

Metric	Count
Definitions	0
Theorems ae_eq_of_ae_le_of_lintegral_le, ae_lt_top, ae_lt_top', lintegral_add_mul_meas_add_le_le_lintegral, lintegral_eq_top_of_measure_eq_top_ne_zero, lintegral_le_meas, lintegral_strict_mono, lintegral_strict_mono_of_ae_le_of_ae_lt_on, lintegral_strict_mono_of_ae_le_of_frequently_ae_lt, meas_ge_le_lintegral_div, meas_le_lintegral₀, measure_eq_top_of_lintegral_ne_top, measure_eq_top_of_setLIntegral_ne_top, mul_meas_ge_le_lintegral, mul_meas_ge_le_lintegral₀, setLIntegral_eq_top_of_measure_eq_top_ne_zero, setLIntegral_le_meas, setLIntegral_strict_mono	18
Total	18

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_eq_of_ae_le_of_lintegral_le 📖	mathematical	Filter.EventuallyLE ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ae Measure Measure.instFunLike Measure.instOuterMeasureClass AEMeasurable ENNReal.measurableSpace lintegral	Filter.EventuallyEq	—	Measure.instOuterMeasureClass LE.le.trans lintegral_add_mul_meas_add_le_le_lintegral mul_eq_zero ENNReal.instNoZeroDivisors nonpos_iff_eq_zero ENNReal.instCanonicallyOrderedAdd AddLECancellable.add_le_iff_nonpos_right IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid ENNReal.cancel_of_ne ENNReal.inv_ne_zero ENNReal.natCast_ne_top Filter.Eventually.mp Filter.Eventually.mono ae_all_iff instCountableNat LE.le.antisymm ENNReal.inv_top add_zero Filter.Tendsto.add ENNReal.instContinuousAdd tendsto_const_nhds tendsto_inv_iff ENNReal.instContinuousInv ENNReal.tendsto_nat_nhds_top ge_of_tendsto' instClosedIciTopology OrderTopology.to_orderClosedTopology ENNReal.instOrderTopology Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat LT.lt.le
ae_lt_top 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	Filter.Eventually Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder Top.top instTopENNReal ae Measure Measure.instFunLike Measure.instOuterMeasureClass	—	ae_lt_top' Measurable.aemeasurable
ae_lt_top' 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	Filter.Eventually Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder Top.top instTopENNReal ae Measure Measure.instFunLike Measure.instOuterMeasureClass	—	Measure.instOuterMeasureClass measure_eq_top_of_lintegral_ne_top
lintegral_add_mul_meas_add_le_le_lintegral 📖	mathematical	Filter.EventuallyLE ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ae Measure Measure.instFunLike Measure.instOuterMeasureClass AEMeasurable ENNReal.measurableSpace	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring lintegral Distrib.toMul DFunLike.coe Set setOf	—	Measure.instOuterMeasureClass exists_measurable_le_lintegral_eq add_le_add_right IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid mul_le_mul_right IsOrderedMonoid.toMulLeftMono ENNReal.instIsOrderedMonoid measure_mono Set.setOf_subset_setOf_of_imp le_imp_le_of_le_of_le add_le_add_left covariant_swap_add_of_covariant_add le_refl lintegral_add_left lintegral_indicator₀ measurableSet_le BorelSpace.opensMeasurable ENNReal.borelSpace OrderTopology.to_orderClosedTopology ENNReal.instOrderTopology ENNReal.instSecondCountableTopology Measurable.add_const ContinuousAdd.measurableAdd ENNReal.instContinuousAdd NullMeasurable.measurable' Measurable.nullMeasurable AEMeasurable.nullMeasurable setLIntegral_const lintegral_mono_ae Filter.Eventually.mono Set.indicator_apply Eq.trans_le add_zero LE.le.trans
lintegral_eq_top_of_measure_eq_top_ne_zero 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	lintegral Top.top instTopENNReal	—	eq_top_iff ENNReal.top_mul mul_meas_ge_le_lintegral₀
lintegral_le_meas 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal instZeroENNReal	lintegral DFunLike.coe Measure Set Measure.instFunLike	—	LE.le.trans lintegral_mono Set.indicator_of_mem Set.indicator_of_notMem ENNReal.instCanonicallyOrderedAdd lintegral_indicator_one_le
lintegral_strict_mono 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace Filter.Eventually Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder ae Measure Measure.instFunLike Measure.instOuterMeasureClass	lintegral	—	Measure.instOuterMeasureClass lintegral_strict_mono_of_ae_le_of_ae_lt_on ae_le_of_ae_lt Measure.measure_univ_eq_zero
lintegral_strict_mono_of_ae_le_of_ae_lt_on 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace Filter.EventuallyLE Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ae Measure Measure.instFunLike Measure.instOuterMeasureClass Filter.Eventually	Preorder.toLT lintegral	—	Measure.instOuterMeasureClass lintegral_strict_mono_of_ae_le_of_frequently_ae_lt Filter.Frequently.mono Filter.Frequently.and_eventually frequently_ae_mem_iff LT.lt.ne
lintegral_strict_mono_of_ae_le_of_frequently_ae_lt 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace Filter.EventuallyLE Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ae Measure Measure.instFunLike Measure.instOuterMeasureClass Filter.Frequently	Preorder.toLT lintegral	—	Measure.instOuterMeasureClass Mathlib.Tactic.Contrapose.contrapose₁ ae_eq_of_ae_le_of_lintegral_le
meas_ge_le_lintegral_div 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Measure Set Measure.instFunLike setOf DivInvMonoid.toDiv ENNReal.instDivInvMonoid lintegral	—	ENNReal.le_div_iff_mul_le mul_comm mul_meas_ge_le_lintegral₀
meas_le_lintegral₀ 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	DFunLike.coe Measure Set Measure.instFunLike lintegral	—	le_trans one_mul measure_mono Measure.instOuterMeasureClass mul_meas_ge_le_lintegral₀
measure_eq_top_of_lintegral_ne_top 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	DFunLike.coe Measure Set Measure.instFunLike setOf Top.top instTopENNReal instZeroENNReal	—	of_not_not lintegral_eq_top_of_measure_eq_top_ne_zero
measure_eq_top_of_setLIntegral_ne_top 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace Measure.restrict	DFunLike.coe Measure Set Measure.instFunLike setOf Set.instMembership Top.top instTopENNReal instZeroENNReal	—	of_not_not setLIntegral_eq_top_of_measure_eq_top_ne_zero
mul_meas_ge_le_lintegral 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	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 lintegral	—	mul_meas_ge_le_lintegral₀ Measurable.aemeasurable
mul_meas_ge_le_lintegral₀ 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	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 lintegral	—	lintegral_zero zero_add lintegral_add_mul_meas_add_le_le_lintegral ae_of_all Measure.instOuterMeasureClass zero_le ENNReal.instCanonicallyOrderedAdd
setLIntegral_eq_top_of_measure_eq_top_ne_zero 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace Measure.restrict	lintegral Top.top instTopENNReal	—	lintegral_eq_top_of_measure_eq_top_ne_zero eq_bot_mono Set.setOf_inter_eq_sep Measure.le_restrict_apply
setLIntegral_le_meas 📖	mathematical	MeasurableSet ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal instZeroENNReal	lintegral Measure.restrict DFunLike.coe Measure Set Measure.instFunLike	—	lintegral_indicator lintegral_le_meas Set.indicator_of_mem ENNReal.instCanonicallyOrderedAdd Set.indicator_of_notMem
setLIntegral_strict_mono 📖	mathematical	MeasurableSet Measurable ENNReal ENNReal.measurableSpace Filter.Eventually ae Measure Measure.instFunLike Measure.instOuterMeasureClass	Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder lintegral Measure.restrict	—	Measure.instOuterMeasureClass lintegral_strict_mono Measurable.aemeasurable ae_restrict_iff'

---

← Back to Index