OptionalStopping

📁 Source: Mathlib/Probability/Martingale/OptionalStopping.lean

Statistics

Metric	Count
Definitions	0
Theorems expected_stoppedValue_mono, stoppedProcess, maximal_ineq, smul_le_stoppedValue_hitting, smul_le_stoppedValue_hittingBtwn, submartingale_iff_expected_stoppedValue_mono, submartingale_of_expected_stoppedValue_mono	7
Total	7

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
maximal_ineq 📖	mathematical	Submartingale Real Nat.instPreorder Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instCompleteSpace Real.instLE Pi.hasLe Pi.instZero Real.instZero	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder NNReal Algebra.toSMul instCommSemiringNNReal CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id DFunLike.coe Measure Set Measure.instFunLike setOf NNReal.toReal Finset.sup' Real.instSemilatticeSup Finset.range Finset.nonempty_range_add_one ENNReal.ofReal integral Measure.restrict	—	Real.instCompleteSpace Finset.nonempty_range_add_one add_le_add IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add smul_le_stoppedValue_hittingBtwn ENNReal.ofReal_le_ofReal setIntegral_mono_on₀ Real.instIsOrderedAddMonoid IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Integrable.integrableOn Submartingale.integrable Submartingale.integrable_stoppedValue Adapted.isStoppingTime_hittingBtwn instWellFoundedLTNat instCountableNat StronglyAdapted.adapted Real.borelSpace PseudoEMetricSpace.pseudoMetrizableSpace Submartingale.stronglyAdapted measurableSet_Ici BorelSpace.opensMeasurable IsOrderedRing.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass hittingBtwn_le nullMeasurableSet_lt instSecondCountableTopologyReal Measurable.aemeasurable Finset.measurable_range_sup'' ContinuousSup.measurableSup₂ TopologicalLattice.toContinuousSup HasSolidNorm.toTopologicalLattice Measurable.le Filtration.le StronglyMeasurable.measurable Submartingale.stronglyMeasurable aemeasurable_const not_le Set.mem_setOf_eq Finset.le_sup'_iff Finset.mem_range WithTop.untopA.congr_simp le_of_eq ENNReal.ofReal_add integral_nonneg setIntegral_union disjoint_iff_inf_le measurableSet_lt measurable_const setIntegral_univ Set.ext stoppedValue_const Submartingale.expected_stoppedValue_mono IsFiniteMeasure.sigmaFiniteFiltration isStoppingTime_const le_rfl ENNReal.add_le_add_iff_right ENNReal.ofReal_ne_top
smul_le_stoppedValue_hitting 📖	mathematical	Submartingale Real Nat.instPreorder Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instCompleteSpace Real.instLE	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder NNReal Algebra.toSMul instCommSemiringNNReal CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id DFunLike.coe Measure Set Measure.instFunLike setOf NNReal.toReal Finset.sup' Real.instSemilatticeSup Finset.range Finset.nonempty_range_add_one ENNReal.ofReal integral Measure.restrict stoppedValue WithTop AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne Nat.instAddMonoidWithOne hittingBtwn Nat.instInfSet	—	smul_le_stoppedValue_hittingBtwn
smul_le_stoppedValue_hittingBtwn 📖	mathematical	Submartingale Real Nat.instPreorder Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instCompleteSpace Real.instLE	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder NNReal Algebra.toSMul instCommSemiringNNReal CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id DFunLike.coe Measure Set Measure.instFunLike setOf NNReal.toReal Finset.sup' Real.instSemilatticeSup Finset.range Finset.nonempty_range_add_one ENNReal.ofReal integral Measure.restrict stoppedValue WithTop AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne Nat.instAddMonoidWithOne hittingBtwn Nat.instInfSet	—	Real.instCompleteSpace Set.ext Nat.instCanonicallyOrderedAdd Finset.nonempty_range_add_one stoppedValue_hittingBtwn_mem instWellFoundedLTNat setIntegral_ge_of_const_le_real measurableSet_le BorelSpace.opensMeasurable Real.borelSpace HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid instSecondCountableTopologyReal measurable_const Finset.measurable_range_sup'' ContinuousSup.measurableSup₂ TopologicalLattice.toContinuousSup HasSolidNorm.toTopologicalLattice Measurable.le Filtration.le StronglyMeasurable.measurable PseudoEMetricSpace.pseudoMetrizableSpace Submartingale.stronglyMeasurable measure_ne_top Integrable.integrableOn Submartingale.integrable_stoppedValue Adapted.isStoppingTime_hittingBtwn instCountableNat StronglyAdapted.adapted Submartingale.stronglyAdapted measurableSet_Ici instClosedIciTopology IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass hittingBtwn_le ENNReal.le_ofReal_iff_toReal_le ENNReal.mul_ne_top le_trans mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing NNReal.coe_nonneg ENNReal.toReal_nonneg ENNReal.toReal_smul
submartingale_iff_expected_stoppedValue_mono 📖	mathematical	StronglyAdapted Nat.instPreorder Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing	Submartingale Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instCompleteSpace Real.instLE integral stoppedValue	—	Real.instCompleteSpace Submartingale.expected_stoppedValue_mono Real.instIsOrderedAddMonoid IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal submartingale_of_expected_stoppedValue_mono
submartingale_of_expected_stoppedValue_mono 📖	mathematical	StronglyAdapted Nat.instPreorder Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Real.instLE integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal stoppedValue	Submartingale Real.instCompleteSpace	—	submartingale_of_setIntegral_le add_le_add_iff_right covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le integral_add_compl Filtration.le integral_piecewise Integrable.integrableOn stoppedValue_piecewise_const ENat.some_eq_coe stoppedValue_const isStoppingTime_piecewise_const isStoppingTime_const IsOrderedRing.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass le_refl le_rfl

MeasureTheory.Submartingale

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
expected_stoppedValue_mono 📖	mathematical	MeasureTheory.Submartingale Nat.instPreorder Preorder.toLE PartialOrder.toPreorder MeasureTheory.IsStoppingTime Pi.hasLe ENat OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat ENat.instNatCast	MeasureTheory.integral MeasureTheory.stoppedValue	—	sub_nonneg covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono MeasureTheory.integral_sub' integrable_stoppedValue le_trans MeasureTheory.stoppedValue_sub_eq_sum' Finset.sum_apply MeasurableSet.inter Set.ext MeasurableSet.compl MeasureTheory.integral_finset_sum MeasureTheory.Integrable.indicator MeasureTheory.Integrable.sub integrable MeasureTheory.Filtration.le Finset.sum_nonneg MeasureTheory.integral_indicator MeasureTheory.Integrable.integrableOn setIntegral_le
stoppedProcess 📖	mathematical	MeasureTheory.Submartingale Real Nat.instPreorder Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instCompleteSpace Real.instLE MeasureTheory.IsStoppingTime	MeasureTheory.stoppedProcess Nat.instLinearOrder	—	Real.instCompleteSpace MeasureTheory.submartingale_iff_expected_stoppedValue_mono MeasureTheory.StronglyAdapted.stoppedProcess_of_discrete PseudoEMetricSpace.pseudoMetrizableSpace TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace Countable.LindelofSpace instCountableNat OrderTopology.of_linearLocallyFinite instDiscreteTopologyNat Nat.borelSpace stronglyAdapted integrable_stoppedValue MeasureTheory.IsStoppingTime.min MeasureTheory.isStoppingTime_const min_le_left MeasureTheory.stoppedValue_stoppedProcess ne_top_of_le_ne_top expected_stoppedValue_mono Real.instIsOrderedAddMonoid IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal min_le_min le_rfl LE.le.trans

---

← Back to Index