Documentation Verification Report

Convergence

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

Statistics

Metric	Count
Definitions	0
Theorems `tendsto_ae_condExp`, `tendsto_eLpNorm_condExp`, `ae_eq_condExp_limitProcess`, `eq_condExp_of_tendsto_eLpNorm`, `ae_tendsto_limitProcess`, `ae_tendsto_limitProcess_of_uniformIntegrable`, `exists_ae_tendsto_of_bdd`, `exists_ae_trim_tendsto_of_bdd`, `memLp_limitProcess`, `tendsto_eLpNorm_one_limitProcess`, `upcrossings_ae_lt_top`, `upcrossings_ae_lt_top'`, `not_frequently_of_upcrossings_lt_top`, `tendsto_ae_condExp`, `tendsto_eLpNorm_condExp`, `tendsto_of_uncrossing_lt_top`, `upcrossings_eq_top_of_frequently_lt`	17
Total	17

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`not_frequently_of_upcrossings_lt_top` 📖	mathematical	`Real` `Real.instLT`	`Filter.Frequently` `Filter.atTop` `Nat.instPreorder`	—	`upcrossings_lt_top_iff` `lt_top_iff_ne_top` `lt_of_le_of_lt` `Mathlib.Tactic.Push.not_forall_eq` `Nat.instCanonicallyOrderedAdd` `Filter.frequently_atTop` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `upcrossingsBefore_lt_of_exists_upcrossing`
`tendsto_ae_condExp` 📖	mathematical	—	`Filter.Eventually` `Filter.Tendsto` `Real` `condExp` `Filtration.seq` `Nat.instPreorder` `Real.normedAddCommGroup` `Real.instCompleteSpace` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Filter.atTop` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `iSup` `MeasurableSpace` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `MeasurableSpace.instCompleteLattice` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass`	—	`Real.instCompleteSpace` `Measure.instOuterMeasureClass` `Integrable.tendsto_ae_condExp` `integrable_condExp` `stronglyMeasurable_condExp` `condExp_condExp_of_le` `le_iSup` `iSup_le` `Filtration.le` `IsFiniteMeasure.toSigmaFinite` `isFiniteMeasure_trim` `Filter.mp_mem` `ae_all_iff` `instCountableNat` `Filter.univ_mem'` `Filter.Tendsto.congr`
`tendsto_eLpNorm_condExp` 📖	mathematical	—	`Filter.Tendsto` `ENNReal` `eLpNorm` `Real` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `SeminormedAddGroup.toContinuousENorm` `Pi.instSub` `Real.instSub` `condExp` `Filtration.seq` `Nat.instPreorder` `Real.normedAddCommGroup` `Real.instCompleteSpace` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `iSup` `MeasurableSpace` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `MeasurableSpace.instCompleteLattice` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Filter.atTop` `nhds` `ENNReal.instTopologicalSpace` `instZeroENNReal`	—	`Real.instCompleteSpace` `Integrable.tendsto_eLpNorm_condExp` `integrable_condExp` `stronglyMeasurable_condExp` `Measure.instOuterMeasureClass` `condExp_condExp_of_le` `le_iSup` `iSup_le` `Filtration.le` `IsFiniteMeasure.toSigmaFinite` `isFiniteMeasure_trim` `Filter.Tendsto.congr` `eLpNorm_congr_ae` `Filter.mp_mem` `Filter.univ_mem'`
`tendsto_of_uncrossing_lt_top` 📖	mathematical	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Filter.liminf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `ENNReal.ofNNReal` `NNNorm.nnnorm` `Real` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Filter.atTop` `Nat.instPreorder` `Top.top` `instTopENNReal` `upcrossings` `Nat.instOrderBot` `Nat.instInfSet` `Real.instRatCast`	`Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	—	`tendsto_of_no_upcrossings` `instOrderTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Rat.denseRange_cast` `Real.instArchimedean` `not_frequently_of_upcrossings_lt_top` `LT.lt.ne` `Rat.cast_lt` `Filter.isBoundedUnder_le_abs` `Real.instIsOrderedAddMonoid` `ENNReal.exists_upcrossings_of_not_bounded_under` `upcrossings_eq_top_of_frequently_lt`
`upcrossings_eq_top_of_frequently_lt` 📖	mathematical	`Real` `Real.instLT` `Filter.Frequently` `Filter.atTop` `Nat.instPreorder`	`upcrossings` `Nat.instOrderBot` `Nat.instInfSet` `Top.top` `ENNReal` `instTopENNReal`	—	`by_contradiction` `not_frequently_of_upcrossings_lt_top`

MeasureTheory.Integrable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tendsto_ae_condExp` 📖	mathematical	`MeasureTheory.Integrable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `MeasureTheory.StronglyMeasurable` `iSup` `MeasurableSpace` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `MeasurableSpace.instCompleteLattice` `MeasureTheory.Filtration.seq` `Nat.instPreorder`	`Filter.Eventually` `Filter.Tendsto` `MeasureTheory.condExp` `Real.normedAddCommGroup` `Real.instCompleteSpace` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Filter.atTop` `nhds` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`sSup_le` `MeasureTheory.Filtration.le` `Real.instCompleteSpace` `uniformIntegrable_condExp_filtration` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.MemLp.integrable` `le_rfl` `MeasureTheory.Filtration.memLp_limitProcess_of_eLpNorm_bdd` `MeasureTheory.setIntegral_condExp` `MeasureTheory.sigmaFinite_of_sigmaFiniteFiltration` `MeasureTheory.IsFiniteMeasure.sigmaFiniteFiltration` `MeasureTheory.setIntegral_congr_ae` `Filter.mp_mem` `MeasureTheory.Martingale.ae_eq_condExp_limitProcess` `MeasureTheory.martingale_condExp` `Filter.univ_mem'` `MeasureTheory.ae_eq_of_forall_setIntegral_eq_of_sigmaFinite'` `MeasureTheory.IsFiniteMeasure.toSigmaFinite` `MeasureTheory.isFiniteMeasure_trim` `integrableOn` `Set.setOf_exists` `isPiSystem_iUnion_of_monotone` `MeasurableSpace.isPiSystem_measurableSet` `MeasureTheory.Filtration.mono` `MeasurableSpace.induction_on_inter` `MeasurableSpace.measurableSpace_iSup_eq` `MeasureTheory.Measure.restrict_empty` `MeasureTheory.integral_zero_measure` `MeasureTheory.setIntegral_compl` `trim` `MeasureTheory.Filtration.stronglyMeasurable_limitProcess` `MeasureTheory.setIntegral_trim` `MeasurableSet.compl` `MeasureTheory.integral_trim` `MeasureTheory.setIntegral_univ` `MeasurableSet.univ` `MeasureTheory.measure_lt_top` `MeasureTheory.integral_iUnion` `instCountableNat` `tsum_congr` `MeasureTheory.StronglyMeasurable.aestronglyMeasurable` `MeasureTheory.Submartingale.ae_tendsto_limitProcess` `MeasureTheory.Martingale.submartingale`
`tendsto_eLpNorm_condExp` 📖	mathematical	`MeasureTheory.Integrable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `MeasureTheory.StronglyMeasurable` `iSup` `MeasurableSpace` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `MeasurableSpace.instCompleteLattice` `MeasureTheory.Filtration.seq` `Nat.instPreorder`	`Filter.Tendsto` `ENNReal` `MeasureTheory.eLpNorm` `ContinuousENorm.toENorm` `SeminormedAddGroup.toPseudoMetricSpace` `Pi.instSub` `Real.instSub` `MeasureTheory.condExp` `Real.normedAddCommGroup` `Real.instCompleteSpace` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Filter.atTop` `nhds` `ENNReal.instTopologicalSpace` `instZeroENNReal`	—	`MeasureTheory.tendsto_Lp_finite_of_tendstoInMeasure` `Real.instCompleteSpace` `le_rfl` `ENNReal.one_ne_top` `MeasureTheory.StronglyMeasurable.aestronglyMeasurable` `MeasureTheory.StronglyMeasurable.mono` `MeasureTheory.stronglyMeasurable_condExp` `MeasureTheory.Filtration.le` `MeasureTheory.memLp_one_iff_integrable` `uniformIntegrable_condExp_filtration` `MeasureTheory.tendstoInMeasure_of_tendsto_ae` `tendsto_ae_condExp`

MeasureTheory.Martingale

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ae_eq_condExp_limitProcess` 📖	mathematical	`MeasureTheory.Martingale` `Real` `Nat.instPreorder` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Real.instCompleteSpace` `MeasureTheory.UniformIntegrable` `ENNReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.condExp` `MeasureTheory.Filtration.seq` `MeasureTheory.Filtration.limitProcess` `Real.instZero` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	—	`Real.instCompleteSpace` `MeasureTheory.Measure.instOuterMeasureClass` `eq_condExp_of_tendsto_eLpNorm` `MeasureTheory.MemLp.integrable` `le_rfl` `MeasureTheory.Filtration.memLp_limitProcess_of_eLpNorm_bdd` `MeasureTheory.Submartingale.tendsto_eLpNorm_one_limitProcess` `submartingale`
`eq_condExp_of_tendsto_eLpNorm` 📖	mathematical	`MeasureTheory.Martingale` `Real` `Nat.instPreorder` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Real.instCompleteSpace` `MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Filter.Tendsto` `ENNReal` `MeasureTheory.eLpNorm` `ContinuousENorm.toENorm` `SeminormedAddGroup.toPseudoMetricSpace` `Pi.instSub` `Real.instSub` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Filter.atTop` `nhds` `ENNReal.instTopologicalSpace` `instZeroENNReal`	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.condExp` `MeasureTheory.Filtration.seq`	—	`Real.instCompleteSpace` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.sub_ae_eq_zero` `MeasureTheory.eLpNorm_eq_zero_iff` `MeasureTheory.StronglyMeasurable.aestronglyMeasurable` `MeasureTheory.StronglyMeasurable.sub` `IsTopologicalAddGroup.to_continuousSub` `instIsTopologicalAddGroupReal` `MeasureTheory.StronglyMeasurable.mono` `stronglyMeasurable` `MeasureTheory.Filtration.le` `MeasureTheory.stronglyMeasurable_condExp` `one_ne_zero` `NeZero.charZero_one` `ENNReal.instCharZero` `tendsto_of_tendsto_of_tendsto_of_le_of_le` `ENNReal.instOrderTopology` `tendsto_const_nhds` `zero_le` `ENNReal.instCanonicallyOrderedAdd` `MeasureTheory.eLpNorm_one_condExp_le_eLpNorm` `MeasureTheory.eLpNorm_congr_ae` `Filter.EventuallyEq.trans` `MeasureTheory.condExp_sub` `integrable` `Filter.mp_mem` `Filter.univ_mem'` `tendsto_nhds_unique` `ENNReal.instT2Space` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `tendsto_atTop_of_eventually_const`

MeasureTheory.Submartingale

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ae_tendsto_limitProcess` 📖	mathematical	`MeasureTheory.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` `MeasureTheory.eLpNorm` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `SeminormedAddGroup.toContinuousENorm` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `ENNReal.ofNNReal`	`Filter.Eventually` `Filter.Tendsto` `Filter.atTop` `nhds` `Real.pseudoMetricSpace` `MeasureTheory.Filtration.limitProcess` `Real.instZero` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`Real.instCompleteSpace` `MeasureTheory.Measure.instOuterMeasureClass` `sSup_le` `MeasureTheory.Filtration.le` `Filter.mp_mem` `exists_ae_trim_tendsto_of_bdd` `Filter.univ_mem'` `AEMeasurable.aestronglyMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `BorelSpace.opensMeasurable` `Real.borelSpace` `instSecondCountableTopologyReal` `aemeasurable_of_tendsto_metrizable_ae'` `Measurable.aemeasurable` `Measurable.mono` `MeasureTheory.StronglyMeasurable.measurable` `stronglyMeasurable` `le_sSup` `le_rfl` `MeasureTheory.measure_eq_zero_of_trim_eq_zero` `MeasureTheory.Filtration.limitProcess.eq_1`
`ae_tendsto_limitProcess_of_uniformIntegrable` 📖	mathematical	`MeasureTheory.Submartingale` `Real` `Nat.instPreorder` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Real.instCompleteSpace` `Real.instLE` `MeasureTheory.UniformIntegrable` `ENNReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	`Filter.Eventually` `Filter.Tendsto` `Filter.atTop` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `MeasureTheory.Filtration.limitProcess` `Real.instZero` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`Real.instCompleteSpace` `MeasureTheory.Measure.instOuterMeasureClass` `ae_tendsto_limitProcess`
`exists_ae_tendsto_of_bdd` 📖	mathematical	`MeasureTheory.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` `MeasureTheory.eLpNorm` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `SeminormedAddGroup.toContinuousENorm` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `ENNReal.ofNNReal`	`Filter.Eventually` `Filter.Tendsto` `Filter.atTop` `nhds` `Real.pseudoMetricSpace` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`Real.instCompleteSpace` `Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.ae_bdd_liminf_atTop_of_eLpNorm_bdd` `BorelSpace.opensMeasurable` `Real.borelSpace` `one_ne_zero` `NeZero.charZero_one` `ENNReal.instCharZero` `Measurable.mono` `MeasureTheory.StronglyMeasurable.measurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `stronglyMeasurable` `MeasureTheory.Filtration.le` `le_rfl` `upcrossings_ae_lt_top` `Filter.univ_mem'` `MeasureTheory.tendsto_of_uncrossing_lt_top`
`exists_ae_trim_tendsto_of_bdd` 📖	mathematical	`MeasureTheory.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` `MeasureTheory.eLpNorm` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `SeminormedAddGroup.toContinuousENorm` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `ENNReal.ofNNReal`	`Filter.Eventually` `Filter.Tendsto` `Filter.atTop` `nhds` `Real.pseudoMetricSpace` `MeasureTheory.ae` `MeasureTheory.Measure` `SupSet.sSup` `MeasurableSpace` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `MeasurableSpace.instCompleteLattice` `Set.range` `MeasureTheory.Filtration.seq` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.trim` `sSup_le` `CompleteSemilatticeSup.toPartialOrder` `MeasureTheory.Filtration.le`	—	`Real.instCompleteSpace` `MeasureTheory.Measure.instOuterMeasureClass` `sSup_le` `MeasureTheory.Filtration.le` `MeasureTheory.ae_iff` `MeasureTheory.trim_measurableSet_eq` `MeasurableSet.compl` `MeasureTheory.measurableSet_exists_tendsto` `instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instSecondCountableTopologyReal` `TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable` `EMetric.instIsCountablyGeneratedUniformity` `T6Space.toT0Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `BorelSpace.opensMeasurable` `Real.borelSpace` `instCountableNat` `instIsCountablyGenerated_atTop` `OrderTopology.of_linearLocallyFinite` `instDiscreteTopologyNat` `TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace` `Countable.LindelofSpace` `PseudoEMetricSpace.pseudoMetrizableSpace` `Measurable.mono` `MeasureTheory.StronglyMeasurable.measurable` `stronglyMeasurable` `le_sSup` `le_rfl` `exists_ae_tendsto_of_bdd`
`memLp_limitProcess` 📖	mathematical	`MeasureTheory.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` `MeasureTheory.eLpNorm` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `SeminormedAddGroup.toContinuousENorm` `ENNReal.ofNNReal`	`MeasureTheory.MemLp` `Real.pseudoMetricSpace` `MeasureTheory.Filtration.limitProcess` `Real.instZero`	—	`Real.instCompleteSpace` `MeasureTheory.Filtration.memLp_limitProcess_of_eLpNorm_bdd` `MeasureTheory.StronglyMeasurable.aestronglyMeasurable` `MeasureTheory.StronglyMeasurable.mono` `stronglyMeasurable` `MeasureTheory.Filtration.le`
`tendsto_eLpNorm_one_limitProcess` 📖	mathematical	`MeasureTheory.Submartingale` `Real` `Nat.instPreorder` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Real.instCompleteSpace` `Real.instLE` `MeasureTheory.UniformIntegrable` `ENNReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	`Filter.Tendsto` `MeasureTheory.eLpNorm` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `SeminormedAddGroup.toContinuousENorm` `Pi.instSub` `Real.instSub` `MeasureTheory.Filtration.limitProcess` `Real.instZero` `Real.pseudoMetricSpace` `Filter.atTop` `nhds` `ENNReal.instTopologicalSpace` `instZeroENNReal`	—	`Real.instCompleteSpace` `MeasureTheory.StronglyMeasurable.aestronglyMeasurable` `MeasureTheory.StronglyMeasurable.mono` `stronglyMeasurable` `MeasureTheory.Filtration.le` `MeasureTheory.tendsto_Lp_finite_of_tendstoInMeasure` `le_rfl` `ENNReal.one_ne_top` `MeasureTheory.Filtration.memLp_limitProcess_of_eLpNorm_bdd` `MeasureTheory.tendstoInMeasure_of_tendsto_ae` `ae_tendsto_limitProcess`
`upcrossings_ae_lt_top` 📖	mathematical	`MeasureTheory.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` `MeasureTheory.eLpNorm` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `SeminormedAddGroup.toContinuousENorm` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `ENNReal.ofNNReal`	`Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`Real.instCompleteSpace` `MeasureTheory.Measure.instOuterMeasureClass` `Encodable.countable` `upcrossings_ae_lt_top'` `Rat.cast_lt` `Real.instIsStrictOrderedRing`
`upcrossings_ae_lt_top'` 📖	mathematical	`MeasureTheory.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` `MeasureTheory.eLpNorm` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `SeminormedAddGroup.toContinuousENorm` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `ENNReal.ofNNReal` `Real.instLT`	`Filter.Eventually` `Preorder.toLT` `MeasureTheory.upcrossings` `Nat.instOrderBot` `Nat.instInfSet` `Top.top` `instTopENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`Real.instCompleteSpace` `MeasureTheory.ae_lt_top` `MeasureTheory.StronglyAdapted.measurable_upcrossings` `stronglyAdapted` `mul_lintegral_upcrossings_le_lintegral_pos_part` `LT.lt.ne` `lt_of_le_of_lt` `ENNReal.le_div_iff_mul_le` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `ENNReal.ofReal_ne_top` `mul_comm` `ENNReal.div_lt_top` `LE.le.trans` `MeasureTheory.lintegral_mono` `sub_eq_add_neg` `nnnorm_neg` `nnnorm_add_le` `MeasureTheory.lintegral_add_right` `measurable_const` `MeasureTheory.lintegral_const` `add_le_add` `ENNReal.instIsOrderedAddMonoid` `MeasureTheory.eLpNorm_one_eq_lintegral_enorm` `le_rfl` `ne_of_lt` `iSup_lt_iff` `ENNReal.add_lt_top` `ENNReal.coe_lt_top` `Ne.lt_top` `ENNReal.mul_ne_top` `ENNReal.coe_ne_top` `MeasureTheory.measure_ne_top` `le_trans` `ENNReal.ofReal_le_iff_le_toReal` `ENNReal.coe_toReal` `coe_nnnorm` `posPart_eq_self` `Real.norm_eq_abs` `abs_of_nonneg` `le_refl` `posPart_eq_zero` `LT.lt.le` `norm_nonneg`

---

← Back to Index