BorelCantelli

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

Statistics

Metric	Count
Definitions process, leastGE, stoppedAbove	3
Theorems integrable_process, martingalePart_process_ae_eq, predictablePart_process_ae_eq, process_difference_le, process_zero, stronglyAdapted_process, ae_not_tendsto_atTop_atBot, ae_not_tendsto_atTop_atTop, bddAbove_range_iff_bddBelow_range, isStoppingTime_leastGE, bddAbove_iff_exists_tendsto, bddAbove_iff_exists_tendsto_aux, eLpNorm_stoppedAbove_le, eLpNorm_stoppedAbove_le', exists_tendsto_of_abs_bddAbove_aux, stoppedAbove, stoppedValue_leastGE, stoppedValue_leastGE_eLpNorm_le, stoppedValue_leastGE_eLpNorm_le', ae_mem_limsup_atTop_iff, norm_stoppedValue_leastGE_le, stoppedAbove_le, tendsto_sum_indicator_atTop_iff, tendsto_sum_indicator_atTop_iff'	24
Total	27

MeasureTheory

Definitions

Name	Category	Theorems
leastGE 📖	CompOp	1 math math: StronglyAdapted.isStoppingTime_leastGE
stoppedAbove 📖	CompOp	8 math math: Submartingale.stoppedValue_leastGE, Submartingale.eLpNorm_stoppedAbove_le, Submartingale.eLpNorm_stoppedAbove_le', Submartingale.stoppedValue_leastGE_eLpNorm_le, norm_stoppedValue_leastGE_le, Submartingale.stoppedAbove, stoppedAbove_le, Submartingale.stoppedValue_leastGE_eLpNorm_le'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_mem_limsup_atTop_iff 📖	mathematical	MeasurableSet Filtration.seq Nat.instPreorder	Filter.Eventually Set Set.instMembership Filter.limsup CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Filter.atTop Filter.Tendsto Real Finset.sum Real.instAddCommMonoid Finset.range condExp Real.normedAddCommGroup Real.instCompleteSpace InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Set.indicator Real.instZero Pi.instOne Real.instOne Real.instPreorder ae Measure Measure.instFunLike Measure.instOuterMeasureClass	—	Real.instCompleteSpace Measure.instOuterMeasureClass Filter.limsup_nat_add Set.limsup_eq_tendsto_sum_indicator_atTop Real.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instArchimedean zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike tendsto_sum_indicator_atTop_iff'
norm_stoppedValue_leastGE_le 📖	mathematical	Real Real.instLE Real.instZero Pi.instZero Filter.Eventually ae Measure Measure.instFunLike Measure.instOuterMeasureClass	stoppedAbove Nat.instLinearOrder Nat.instOrderBot Nat.instInfSet Real.instPreorder Real.instAdd NNReal.toReal	—	stoppedAbove_le
stoppedAbove_le 📖	mathematical	Real Real.instLE Real.instZero Pi.instZero Filter.Eventually ae Measure Measure.instFunLike Measure.instOuterMeasureClass	stoppedAbove Nat.instLinearOrder Nat.instOrderBot Nat.instInfSet Real.instPreorder Real.instAdd NNReal.toReal	—	Measure.instOuterMeasureClass Filter.mp_mem Filter.univ_mem' stoppedAbove.eq_1 stoppedProcess.eq_1 ENat.some_eq_coe add_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid NNReal.coe_nonneg add_comm sub_le_iff_le_add covariant_swap_add_of_covariant_add notMem_of_lt_hittingAfter ne_top_of_le_ne_top min_le_left CanLift.prf ENat.canLift LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass WithTop.untopA.congr_simp LT.lt.trans_le min_le_right LE.le.trans LT.lt.le sub_lt_sub_left IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd bot_eq_zero Nat.instCanonicallyOrderedAdd le_abs_self
tendsto_sum_indicator_atTop_iff 📖	mathematical	Filter.Eventually ae Measure Measure.instFunLike Measure.instOuterMeasureClass 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	Filter.Tendsto Filter.atTop Real.instPreorder predictablePart Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instCompleteSpace	—	Measure.instOuterMeasureClass Real.instCompleteSpace Martingale.ae_not_tendsto_atTop_atTop Nat.instAtLeastTwoHAddOfNat martingale_martingalePart IsFiniteMeasure.sigmaFiniteFiltration martingalePart_bdd_difference Martingale.ae_not_tendsto_atTop_atBot ae_all_iff instCountableNat condExp_nonneg instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing Filter.mp_mem Filter.univ_mem' sub_nonneg covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Filter.tendsto_atTop_atTop_of_monotone' Finset.sum_apply Finset.sum_mono_set_of_nonneg Finset.range_mono sub_eq_add_neg Filter.tendsto_atTop_add_right_of_le Filter.tendsto_neg_atBot_iff neg_le_neg monotone_nat_of_le_succ Filter.tendsto_atBot_add_left_of_ge
tendsto_sum_indicator_atTop_iff' 📖	mathematical	MeasurableSet Filtration.seq Nat.instPreorder	Filter.Eventually Filter.Tendsto Real Finset.sum Real.instAddCommMonoid Finset.range Set.indicator Real.instZero Pi.instOne Real.instOne Filter.atTop Real.instPreorder condExp Real.normedAddCommGroup Real.instCompleteSpace InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal ae Measure Measure.instFunLike Measure.instOuterMeasureClass	—	Real.instCompleteSpace Measure.instOuterMeasureClass tendsto_sum_indicator_atTop_iff Filter.Eventually.of_forall BorelCantelli.process.eq_1 sub_nonneg covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Finset.sum_apply Finset.sum_range_succ_sub_sum Set.indicator_nonneg zero_le_one Real.instZeroLEOneClass BorelCantelli.stronglyAdapted_process BorelCantelli.integrable_process BorelCantelli.process_difference_le BorelCantelli.predictablePart_process_ae_eq

MeasureTheory.BorelCantelli

Definitions

Name	Category	Theorems
process 📖	CompOp	6 math math: martingalePart_process_ae_eq, predictablePart_process_ae_eq, process_zero, integrable_process, stronglyAdapted_process, process_difference_le

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integrable_process 📖	mathematical	MeasurableSet MeasureTheory.Filtration.seq Nat.instPreorder	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing process	—	MeasureTheory.integrable_finset_sum' IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal MeasureTheory.IntegrableOn.integrable_indicator MeasureTheory.integrable_const MeasureTheory.isFiniteMeasureRestrict MeasureTheory.Filtration.le
martingalePart_process_ae_eq 📖	mathematical	—	MeasureTheory.martingalePart Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instCompleteSpace process Finset.sum Pi.addCommMonoid Real.instAddCommMonoid Finset.range Pi.instSub Real.instSub Set.indicator Real.instZero Pi.instOne Real.instOne MeasureTheory.condExp MeasureTheory.Filtration.seq Nat.instPreorder	—	Real.instCompleteSpace MeasureTheory.martingalePart_eq_sum process_zero zero_add Finset.sum_congr Finset.sum_range_succ_sub_sum
predictablePart_process_ae_eq 📖	mathematical	—	MeasureTheory.predictablePart Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instCompleteSpace process Finset.sum Pi.addCommMonoid Real.instAddCommMonoid Finset.range MeasureTheory.condExp MeasureTheory.Filtration.seq Nat.instPreorder Set.indicator Real.instZero Pi.instOne Real.instOne	—	Real.instCompleteSpace martingalePart_process_ae_eq sub_right_injective Finset.sum_sub_distrib
process_difference_le 📖	mathematical	—	Real Real.instLE abs Real.lattice Real.instAddGroup Real.instSub process NNReal.toReal NNReal instOneNNReal	—	Nat.cast_one process.eq_1 Finset.sum_apply Finset.sum_range_succ_sub_sum Real.norm_eq_abs norm_indicator_eq_indicator_norm Set.indicator_le' Pi.one_apply NormOneClass.norm_one NormedDivisionRing.to_normOneClass le_refl zero_le_one Real.instZeroLEOneClass
process_zero 📖	mathematical	—	process Pi.instZero Real Real.instZero	—	process.eq_1 Finset.range_zero Finset.sum_empty
stronglyAdapted_process 📖	mathematical	MeasurableSet MeasureTheory.Filtration.seq Nat.instPreorder	MeasureTheory.StronglyAdapted Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace process	—	Finset.stronglyMeasurable_sum IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal MeasureTheory.StronglyMeasurable.indicator MeasureTheory.stronglyMeasurable_one MeasureTheory.Filtration.mono Finset.mem_range

MeasureTheory.Martingale

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_not_tendsto_atTop_atBot 📖	mathematical	MeasureTheory.Martingale Real Nat.instPreorder Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instCompleteSpace Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	Filter.Tendsto Filter.atTop Filter.atBot Real.instPreorder	—	Real.instCompleteSpace MeasureTheory.Measure.instOuterMeasureClass Filter.mp_mem bddAbove_range_iff_bddBelow_range Filter.univ_mem' Filter.not_bddBelow_of_tendsto_atBot Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat instNoMinOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial Filter.bddAbove_range_of_tendsto_atTop_atBot Real.instArchimedean
ae_not_tendsto_atTop_atTop 📖	mathematical	MeasureTheory.Martingale Real Nat.instPreorder Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instCompleteSpace Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	Filter.Tendsto Filter.atTop Real.instPreorder	—	Real.instCompleteSpace MeasureTheory.Measure.instOuterMeasureClass Filter.mp_mem bddAbove_range_iff_bddBelow_range Filter.univ_mem' Filter.not_bddAbove_of_tendsto_atTop Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial Filter.bddBelow_range_of_tendsto_atTop_atTop instIsCodirectedOrder Real.instArchimedean
bddAbove_range_iff_bddBelow_range 📖	mathematical	MeasureTheory.Martingale Real Nat.instPreorder Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instCompleteSpace Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	BddAbove Real.instLE Set.range BddBelow	—	Real.instCompleteSpace MeasureTheory.Measure.instOuterMeasureClass Filter.mp_mem Filter.univ_mem' MeasureTheory.Submartingale.bddAbove_iff_exists_tendsto submartingale neg Filter.Tendsto.neg IsTopologicalRing.toContinuousNeg instIsTopologicalRingReal neg_neg neg_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add mem_upperBounds le_neg mem_lowerBounds

MeasureTheory.StronglyAdapted

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isStoppingTime_leastGE 📖	mathematical	MeasureTheory.StronglyAdapted PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder	MeasureTheory.IsStoppingTime MeasureTheory.leastGE ConditionallyCompleteLinearOrderBot.toOrderBot ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	MeasureTheory.Adapted.isStoppingTime_hittingAfter adapted measurableSet_Ici BorelSpace.opensMeasurable

MeasureTheory.Submartingale

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bddAbove_iff_exists_tendsto 📖	mathematical	MeasureTheory.Submartingale Real Nat.instPreorder Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instCompleteSpace Real.instLE Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	BddAbove Set.range Filter.Tendsto Filter.atTop nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	Real.instCompleteSpace MeasureTheory.Measure.instOuterMeasureClass sub_martingale IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid MeasureTheory.martingale_const_fun MeasureTheory.IsFiniteMeasure.sigmaFiniteFiltration stronglyAdapted integrable sub_self sub_sub_sub_cancel_right Filter.mp_mem bddAbove_iff_exists_tendsto_aux Filter.univ_mem' sub_eq_add_neg add_le_add covariant_swap_add_of_covariant_add neg_le_abs sub_le_iff_le_add le_trans sub_le_sub_left le_abs_self Filter.Tendsto.sub_const IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal Filter.Tendsto.add_const IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal sub_add_cancel
bddAbove_iff_exists_tendsto_aux 📖	mathematical	MeasureTheory.Submartingale Real Nat.instPreorder Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instCompleteSpace Real.instLE Pi.instZero Real.instZero Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	BddAbove Set.range Filter.Tendsto Filter.atTop nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	Real.instCompleteSpace MeasureTheory.Measure.instOuterMeasureClass Filter.mp_mem exists_tendsto_of_abs_bddAbove_aux Filter.univ_mem' Filter.Tendsto.bddAbove_range BoundedLENhdsClass.of_closedIciTopology instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid instIsDirectedOrder Real.instIsOrderedRing Real.instArchimedean
eLpNorm_stoppedAbove_le 📖	mathematical	MeasureTheory.Submartingale Real Nat.instPreorder Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instCompleteSpace Real.instLE Real.instZero Pi.instZero Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder MeasureTheory.eLpNorm ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SeminormedAddGroup.toContinuousENorm MeasureTheory.stoppedAbove Nat.instLinearOrder Nat.instOrderBot Nat.instInfSet Real.instPreorder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring instOfNatAtLeastTwo AddMonoidWithOne.toNatCast Nat.instAtLeastTwoHAddOfNat DFunLike.coe Set Set.univ ENNReal.ofReal Real.instAdd NNReal.toReal	—	Real.instCompleteSpace MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.eLpNorm_one_le_of_le' integrable stoppedAbove MeasureTheory.setIntegral_univ le_trans MeasureTheory.Measure.restrict_univ WithTop.untopA.congr_simp inf_of_le_left WithTop.canonicallyOrderedAdd Nat.instCanonicallyOrderedAdd MeasureTheory.integral_zero setIntegral_le Real.instIsOrderedAddMonoid IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal MeasureTheory.IsFiniteMeasure.sigmaFiniteFiltration zero_le MeasurableSet.univ MeasureTheory.stoppedAbove_le
eLpNorm_stoppedAbove_le' 📖	mathematical	MeasureTheory.Submartingale Real Nat.instPreorder Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instCompleteSpace Real.instLE Real.instZero Pi.instZero Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder MeasureTheory.eLpNorm ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SeminormedAddGroup.toContinuousENorm MeasureTheory.stoppedAbove Nat.instLinearOrder Nat.instOrderBot Nat.instInfSet Real.instPreorder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal ENNReal.ofNNReal ENNReal.toNNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring instOfNatAtLeastTwo AddMonoidWithOne.toNatCast Nat.instAtLeastTwoHAddOfNat DFunLike.coe Set Set.univ ENNReal.ofReal Real.instAdd NNReal.toReal	—	Real.instCompleteSpace MeasureTheory.Measure.instOuterMeasureClass LE.le.trans Nat.instAtLeastTwoHAddOfNat eLpNorm_stoppedAbove_le ENNReal.toNNReal_mul ENNReal.coe_toNNReal MeasureTheory.measure_ne_top
exists_tendsto_of_abs_bddAbove_aux 📖	—	MeasureTheory.Submartingale Real Nat.instPreorder Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instCompleteSpace Real.instLE Pi.instZero Real.instZero Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	—	Real.instCompleteSpace MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_all_iff instCountableNat exists_ae_tendsto_of_bdd Nat.instAtLeastTwoHAddOfNat stoppedAbove eLpNorm_stoppedAbove_le' Nat.cast_nonneg Real.instIsOrderedRing Filter.mp_mem Filter.univ_mem' BddAbove.eq_1 exists_nat_gt Real.instIsStrictOrderedRing Real.instArchimedean lt_of_le_of_lt mem_upperBounds Set.Nonempty.some_mem MeasureTheory.stoppedAbove.eq_1 MeasureTheory.stoppedProcess.eq_1 MeasureTheory.leastGE.eq_1 MeasureTheory.hittingAfter_eq_top_iff Nat.instCanonicallyOrderedAdd WithTop.untopA.congr_simp inf_of_le_left
stoppedAbove 📖	mathematical	MeasureTheory.Submartingale Real Nat.instPreorder Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instCompleteSpace Real.instLE	MeasureTheory.stoppedAbove Nat.instLinearOrder Nat.instOrderBot Nat.instInfSet Real.instPreorder	—	Real.instCompleteSpace stoppedProcess MeasureTheory.IsFiniteMeasure.sigmaFiniteFiltration MeasureTheory.StronglyAdapted.isStoppingTime_leastGE instWellFoundedLTNat instCountableNat instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid PseudoEMetricSpace.pseudoMetrizableSpace Real.borelSpace stronglyAdapted
stoppedValue_leastGE 📖	mathematical	MeasureTheory.Submartingale Real Nat.instPreorder Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instCompleteSpace Real.instLE	MeasureTheory.stoppedAbove Nat.instLinearOrder Nat.instOrderBot Nat.instInfSet Real.instPreorder	—	stoppedAbove
stoppedValue_leastGE_eLpNorm_le 📖	mathematical	MeasureTheory.Submartingale Real Nat.instPreorder Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instCompleteSpace Real.instLE Real.instZero Pi.instZero Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder MeasureTheory.eLpNorm ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SeminormedAddGroup.toContinuousENorm MeasureTheory.stoppedAbove Nat.instLinearOrder Nat.instOrderBot Nat.instInfSet Real.instPreorder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring instOfNatAtLeastTwo AddMonoidWithOne.toNatCast Nat.instAtLeastTwoHAddOfNat DFunLike.coe Set Set.univ ENNReal.ofReal Real.instAdd NNReal.toReal	—	eLpNorm_stoppedAbove_le
stoppedValue_leastGE_eLpNorm_le' 📖	mathematical	MeasureTheory.Submartingale Real Nat.instPreorder Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instCompleteSpace Real.instLE Real.instZero Pi.instZero Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder MeasureTheory.eLpNorm ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SeminormedAddGroup.toContinuousENorm MeasureTheory.stoppedAbove Nat.instLinearOrder Nat.instOrderBot Nat.instInfSet Real.instPreorder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal ENNReal.ofNNReal ENNReal.toNNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring instOfNatAtLeastTwo AddMonoidWithOne.toNatCast Nat.instAtLeastTwoHAddOfNat DFunLike.coe Set Set.univ ENNReal.ofReal Real.instAdd NNReal.toReal	—	eLpNorm_stoppedAbove_le'

---

← Back to Index