Upcrossing

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

Statistics

Metric	Count
Definitions `lowerCrossingTime`, `lowerCrossingTimeAux`, `upcrossingStrat`, `upcrossings`, `upcrossingsBefore`, `upperCrossingTime`	6
Theorems `integrable_upcrossingsBefore`, `isStoppingTime_crossing`, `isStoppingTime_lowerCrossingTime`, `isStoppingTime_upperCrossingTime`, `measurable_upcrossings`, `measurable_upcrossingsBefore`, `upcrossingStrat`, `mul_integral_upcrossingsBefore_le_integral_pos_part`, `mul_lintegral_upcrossings_le_lintegral_pos_part`, `sum_mul_upcrossingStrat_le`, `sum_sub_upcrossingStrat_mul`, `sum_upcrossingStrat_mul`, `crossing_eq_crossing_of_lowerCrossingTime_lt`, `crossing_eq_crossing_of_upperCrossingTime_lt`, `crossing_pos_eq`, `exists_upperCrossingTime_eq`, `integral_mul_upcrossingsBefore_le_integral`, `le_sub_of_le_upcrossingsBefore`, `lowerCrossingTime_le`, `lowerCrossingTime_le_upperCrossingTime_succ`, `lowerCrossingTime_lt_of_lt_upcrossingsBefore`, `lowerCrossingTime_lt_upperCrossingTime`, `lowerCrossingTime_mono`, `lowerCrossingTime_stabilize`, `lowerCrossingTime_stabilize'`, `lowerCrossingTime_zero`, `mul_integral_upcrossingsBefore_le_integral_pos_part_aux`, `mul_upcrossingsBefore_le`, `stoppedValue_lowerCrossingTime`, `stoppedValue_upperCrossingTime`, `sub_eq_zero_of_upcrossingsBefore_lt`, `upcrossingStrat_le_one`, `upcrossingStrat_nonneg`, `upcrossingsBefore_bot`, `upcrossingsBefore_eq_sum`, `upcrossingsBefore_le`, `upcrossingsBefore_lt_of_exists_upcrossing`, `upcrossingsBefore_mono`, `upcrossingsBefore_pos_eq`, `upcrossingsBefore_zero`, `upcrossingsBefore_zero'`, `upcrossings_lt_top_iff`, `upperCrossingTime_bound_eq`, `upperCrossingTime_eq_of_bound_le`, `upperCrossingTime_eq_of_upcrossingsBefore_lt`, `upperCrossingTime_eq_upperCrossingTime_of_lt`, `upperCrossingTime_le`, `upperCrossingTime_le_lowerCrossingTime`, `upperCrossingTime_lt_bddAbove`, `upperCrossingTime_lt_lowerCrossingTime`, `upperCrossingTime_lt_nonempty`, `upperCrossingTime_lt_of_le_upcrossingsBefore`, `upperCrossingTime_lt_succ`, `upperCrossingTime_mono`, `upperCrossingTime_stabilize`, `upperCrossingTime_stabilize'`, `upperCrossingTime_succ`, `upperCrossingTime_succ_eq`, `upperCrossingTime_zero`, `upperCrossingTime_zero'`	60
Total	66

MeasureTheory

Definitions

Name	Category	Theorems
`lowerCrossingTime` 📖	CompOp	19 math math: `upperCrossingTime_succ_eq`, `crossing_eq_crossing_of_lowerCrossingTime_lt`, `lowerCrossingTime_lt_upperCrossingTime`, `lowerCrossingTime_le`, `lowerCrossingTime_zero`, `lowerCrossingTime_le_upperCrossingTime_succ`, `crossing_pos_eq`, `stoppedValue_lowerCrossingTime`, `upperCrossingTime_le_lowerCrossingTime`, `lowerCrossingTime_stabilize`, `upperCrossingTime_lt_lowerCrossingTime`, `lowerCrossingTime_lt_of_lt_upcrossingsBefore`, `lowerCrossingTime_stabilize'`, `StronglyAdapted.isStoppingTime_crossing`, `crossing_eq_crossing_of_upperCrossingTime_lt`, `le_sub_of_le_upcrossingsBefore`, `lowerCrossingTime_mono`, `StronglyAdapted.isStoppingTime_lowerCrossingTime`, `sub_eq_zero_of_upcrossingsBefore_lt`
`lowerCrossingTimeAux` 📖	CompOp	1 math math: `upperCrossingTime_succ`
`upcrossingStrat` 📖	CompOp	7 math math: `upcrossingStrat_nonneg`, `Submartingale.sum_sub_upcrossingStrat_mul`, `Submartingale.sum_upcrossingStrat_mul`, `upcrossingStrat_le_one`, `Submartingale.sum_mul_upcrossingStrat_le`, `StronglyAdapted.upcrossingStrat`, `mul_upcrossingsBefore_le`
`upcrossings` 📖	CompOp	5 math math: `StronglyAdapted.measurable_upcrossings`, `upcrossings_eq_top_of_frequently_lt`, `Submartingale.mul_lintegral_upcrossings_le_lintegral_pos_part`, `Submartingale.upcrossings_ae_lt_top'`, `upcrossings_lt_top_iff`
`upcrossingsBefore` 📖	CompOp	15 math math: `Submartingale.mul_integral_upcrossingsBefore_le_integral_pos_part`, `upcrossingsBefore_zero'`, `integral_mul_upcrossingsBefore_le_integral`, `mul_integral_upcrossingsBefore_le_integral_pos_part_aux`, `upcrossingsBefore_lt_of_exists_upcrossing`, `upcrossingsBefore_le`, `StronglyAdapted.measurable_upcrossingsBefore`, `upcrossingsBefore_eq_sum`, `upcrossingsBefore_zero`, `StronglyAdapted.integrable_upcrossingsBefore`, `upcrossingsBefore_mono`, `mul_upcrossingsBefore_le`, `upcrossings_lt_top_iff`, `upcrossingsBefore_bot`, `upcrossingsBefore_pos_eq`
`upperCrossingTime` 📖	CompOp	30 math math: `upperCrossingTime_succ_eq`, `upperCrossingTime_eq_upperCrossingTime_of_lt`, `crossing_eq_crossing_of_lowerCrossingTime_lt`, `StronglyAdapted.isStoppingTime_upperCrossingTime`, `lowerCrossingTime_lt_upperCrossingTime`, `upperCrossingTime_lt_of_le_upcrossingsBefore`, `upperCrossingTime_bound_eq`, `upperCrossingTime_mono`, `lowerCrossingTime_le_upperCrossingTime_succ`, `crossing_pos_eq`, `upperCrossingTime_le_lowerCrossingTime`, `upperCrossingTime_lt_lowerCrossingTime`, `StronglyAdapted.isStoppingTime_crossing`, `stoppedValue_upperCrossingTime`, `upperCrossingTime_lt_bddAbove`, `crossing_eq_crossing_of_upperCrossingTime_lt`, `upperCrossingTime_stabilize`, `upperCrossingTime_lt_nonempty`, `upperCrossingTime_zero`, `le_sub_of_le_upcrossingsBefore`, `upcrossingsBefore_eq_sum`, `upperCrossingTime_eq_of_bound_le`, `upperCrossingTime_zero'`, `upperCrossingTime_stabilize'`, `upperCrossingTime_le`, `upperCrossingTime_succ`, `sub_eq_zero_of_upcrossingsBefore_lt`, `upperCrossingTime_lt_succ`, `upperCrossingTime_eq_of_upcrossingsBefore_lt`, `exists_upperCrossingTime_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`crossing_eq_crossing_of_lowerCrossingTime_lt` 📖	mathematical	`lowerCrossingTime` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet`	`upperCrossingTime` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet` `lowerCrossingTime`	—	`lt_of_le_of_lt` `upperCrossingTime_le_lowerCrossingTime` `bot_eq_zero'` `Nat.instCanonicallyOrderedAdd` `hittingBtwn_eq_hittingBtwn_of_exists` `hittingBtwn_lt_iff` `le_rfl` `lowerCrossingTime.eq_1` `LT.lt.le` `upperCrossingTime_succ_eq` `lowerCrossingTime_mono` `upperCrossingTime_mono`
`crossing_eq_crossing_of_upperCrossingTime_lt` 📖	mathematical	`upperCrossingTime` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet`	`upperCrossingTime` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet` `lowerCrossingTime`	—	`crossing_eq_crossing_of_lowerCrossingTime_lt` `lt_of_le_of_lt` `lowerCrossingTime_le_upperCrossingTime_succ` `upperCrossingTime_succ_eq` `hittingBtwn_eq_hittingBtwn_of_exists` `hittingBtwn_lt_iff` `le_rfl` `LT.lt.le`
`crossing_pos_eq` 📖	mathematical	`Real` `Real.instLT`	`upperCrossingTime` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet` `Real` `Real.instZero` `Real.instSub` `PosPart.posPart` `instPosPart` `Real.lattice` `Real.instAddGroup` `lowerCrossingTime`	—	`sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Real.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `sub_le_sub_iff_right` `posPart_eq_of_posPart_pos` `lt_of_lt_of_le` `posPart_eq_self` `le_trans` `LT.lt.le` `posPart_nonpos` `sub_nonpos` `Nat.instCanonicallyOrderedAdd` `upperCrossingTime_succ_eq` `AddGroup.toOrderedSub`
`exists_upperCrossingTime_eq` 📖	mathematical	`Real` `Real.instLT`	`upperCrossingTime` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet`	—	`strictMono_nat_of_lt_succ` `upperCrossingTime_lt_succ` `lt_of_lt_of_le` `StrictMono.id_le` `instWellFoundedLTNat` `not_le` `upperCrossingTime_le`
`integral_mul_upcrossingsBefore_le_integral` 📖	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` `Real.instLT`	`Real` `Real.instLE` `Real.instMul` `Real.instSub` `integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Real.instNatCast` `upcrossingsBefore` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet`	—	`Real.instCompleteSpace` `integral_const_mul` `integral_mono_of_nonneg` `Real.instIsOrderedAddMonoid` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Filter.Eventually.of_forall` `Measure.instOuterMeasureClass` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `sub_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `LT.lt.le` `Nat.cast_nonneg` `Submartingale.integrable` `Submartingale.sum_upcrossingStrat_mul` `Filter.univ_mem'` `Finset.sum_apply` `Finset.sum_congr` `mul_upcrossingsBefore_le` `Submartingale.sum_mul_upcrossingStrat_le` `sub_le_self_iff` `integral_nonneg`
`le_sub_of_le_upcrossingsBefore` 📖	mathematical	`Real` `Real.instLT` `upcrossingsBefore` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet`	`Real` `Real.instLE` `Real.instSub` `stoppedValue` `WithTop` `WithTop.natCast` `upperCrossingTime` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet` `lowerCrossingTime`	—	`sub_le_sub` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `stoppedValue_upperCrossingTime` `LT.lt.ne` `upperCrossingTime_lt_of_le_upcrossingsBefore` `stoppedValue_lowerCrossingTime` `lowerCrossingTime_lt_of_lt_upcrossingsBefore`
`lowerCrossingTime_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `lowerCrossingTime` `ConditionallyCompleteLinearOrderBot.toOrderBot` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf`	—	`hittingBtwn_le`
`lowerCrossingTime_le_upperCrossingTime_succ` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `lowerCrossingTime` `ConditionallyCompleteLinearOrderBot.toOrderBot` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `upperCrossingTime`	—	`upperCrossingTime_succ` `le_hittingBtwn` `lowerCrossingTime_le`
`lowerCrossingTime_lt_of_lt_upcrossingsBefore` 📖	mathematical	`Real` `Real.instLT` `upcrossingsBefore` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet`	`lowerCrossingTime` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet`	—	`lt_of_le_of_lt` `lowerCrossingTime_le_upperCrossingTime_succ` `upperCrossingTime_lt_of_le_upcrossingsBefore`
`lowerCrossingTime_lt_upperCrossingTime` 📖	mathematical	`Real` `Real.instLT`	`lowerCrossingTime` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet` `upperCrossingTime`	—	`lt_of_le_of_ne` `lowerCrossingTime_le_upperCrossingTime_succ` `not_le` `le_trans` `stoppedValue_upperCrossingTime` `stoppedValue_lowerCrossingTime`
`lowerCrossingTime_mono` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `lowerCrossingTime` `ConditionallyCompleteLinearOrderBot.toOrderBot` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf`	—	`monotone_nat_of_le_succ` `le_trans` `lowerCrossingTime_le_upperCrossingTime_succ` `upperCrossingTime_le_lowerCrossingTime`
`lowerCrossingTime_stabilize` 📖	mathematical	`lowerCrossingTime` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet`	`lowerCrossingTime` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet`	—	`le_antisymm` `lowerCrossingTime_le` `le_trans` `le_of_eq` `lowerCrossingTime_mono`
`lowerCrossingTime_stabilize'` 📖	mathematical	`lowerCrossingTime` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet`	`lowerCrossingTime` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet`	—	`lowerCrossingTime_stabilize` `le_antisymm` `lowerCrossingTime_le`
`lowerCrossingTime_zero` 📖	mathematical	—	`lowerCrossingTime` `hittingBtwn` `Real` `Set.Iic` `Real.instPreorder` `Bot.bot` `OrderBot.toBot` `Preorder.toLE`	—	—
`mul_integral_upcrossingsBefore_le_integral_pos_part_aux` 📖	mathematical	`Submartingale` `Real` `Nat.instPreorder` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Real.instCompleteSpace` `Real.instLE` `Real.instLT`	`Real` `Real.instLE` `Real.instMul` `Real.instSub` `integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Real.instNatCast` `upcrossingsBefore` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet`	—	`Real.instCompleteSpace` `le_trans` `le_of_eq` `sub_zero` `upcrossingsBefore_pos_eq` `integral_mul_upcrossingsBefore_le_integral` `Submartingale.pos` `TopologicalLattice.toContinuousSup` `HasSolidNorm.toTopologicalLattice` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `Submartingale.sub_martingale` `IsOrderedAddMonoid.toAddLeftMono` `martingale_const` `posPart_nonneg` `sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Real.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `covariant_swap_add_of_covariant_add`
`mul_upcrossingsBefore_le` 📖	mathematical	`Real` `Real.instLE` `Real.instLT`	`Real` `Real.instLE` `Real.instMul` `Real.instSub` `Real.instNatCast` `upcrossingsBefore` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet` `Finset.sum` `Real.instAddCommMonoid` `Finset.range` `upcrossingStrat` `Pi.instSub`	—	`upcrossingsBefore_zero'` `CharP.cast_eq_zero` `CharP.ofCharZero` `RCLike.charZero_rclike` `MulZeroClass.mul_zero` `Finset.sum_congr` `instReflLe` `Finset.sum_mul` `Set.indicator_mul_left` `one_mul` `Finset.sum_comm` `Finset.sum_indicator_eq_sum_filter` `Finset.ext` `Finset.filter.congr_simp` `lt_of_lt_of_le` `upperCrossingTime_le` `Finset.sum_Ico_eq_add_neg` `lowerCrossingTime_le_upperCrossingTime_succ` `Finset.sum_range_sub` `neg_sub` `sub_add_sub_cancel` `Finset.sum_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `le_sub_of_le_upcrossingsBefore` `zero_lt_iff` `Finset.mem_range` `Finset.sum_le_sum_of_subset_of_nonneg` `Finset.range_subset_range` `upcrossingsBefore_le` `upperCrossingTime_eq_of_upcrossingsBefore_lt` `sub_self` `le_refl` `sub_nonneg` `covariant_swap_add_of_covariant_add` `le_trans` `stoppedValue_lowerCrossingTime` `sub_eq_zero_of_upcrossingsBefore_lt` `lt_of_le_of_ne` `not_lt` `Finset.sum_const` `Finset.card_range` `nsmul_eq_mul` `mul_comm`
`stoppedValue_lowerCrossingTime` 📖	mathematical	—	`Real` `Real.instLE` `stoppedValue` `WithTop` `WithTop.natCast` `lowerCrossingTime` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet`	—	`hittingBtwn_le_iff_of_lt` `instWellFoundedLTNat` `lt_of_le_of_ne` `lowerCrossingTime_le` `le_rfl` `stoppedValue_hittingBtwn_mem` `le_trans`
`stoppedValue_upperCrossingTime` 📖	mathematical	—	`Real` `Real.instLE` `stoppedValue` `WithTop` `WithTop.natCast` `upperCrossingTime` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet`	—	`hittingBtwn_le_iff_of_lt` `instWellFoundedLTNat` `lt_of_le_of_ne` `upperCrossingTime_le` `le_rfl` `stoppedValue_hittingBtwn_mem` `le_trans` `hittingBtwn_le`
`sub_eq_zero_of_upcrossingsBefore_lt` 📖	mathematical	`Real` `Real.instLT` `upcrossingsBefore` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet`	`Real` `Real.instSub` `stoppedValue` `WithTop` `WithTop.natCast` `upperCrossingTime` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet` `lowerCrossingTime` `Real.instZero`	—	`not_lt` `not_le` `upcrossingsBefore.eq_1` `le_csSup` `upperCrossingTime_lt_bddAbove` `WithTop.untopA.congr_simp` `upperCrossingTime_stabilize'` `lowerCrossingTime_stabilize'` `le_rfl` `le_trans` `upperCrossingTime_le_lowerCrossingTime` `sub_self`
`upcrossingStrat_le_one` 📖	mathematical	—	`Real` `Real.instLE` `upcrossingStrat` `Real.instOne`	—	`upcrossingStrat.eq_1` `Finset.indicator_biUnion_apply` `lt_or_gt_of_ne` `min_eq_left` `upperCrossingTime_mono` `LT.lt.le` `max_eq_right` `lowerCrossingTime_mono` `le_trans` `upperCrossingTime_le_lowerCrossingTime` `min_eq_right` `max_eq_left` `Set.indicator_le_self'` `zero_le_one` `Real.instZeroLEOneClass`
`upcrossingStrat_nonneg` 📖	mathematical	—	`Real` `Real.instLE` `Real.instZero` `upcrossingStrat`	—	`Finset.sum_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Set.indicator_nonneg` `zero_le_one` `Real.instZeroLEOneClass`
`upcrossingsBefore_bot` 📖	mathematical	—	`upcrossingsBefore` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `Nat.instOrderBot`	—	`csSup_empty`
`upcrossingsBefore_eq_sum` 📖	mathematical	`Real` `Real.instLT`	`upcrossingsBefore` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet` `Finset.sum` `Nat.instAddCommMonoid` `Finset.Ico` `Nat.instLocallyFiniteOrder` `Set.indicator` `MulZeroClass.toZero` `Nat.instMulZeroClass` `setOf` `upperCrossingTime` `Pi.instOne` `Nat.instOne`	—	`upcrossingsBefore_zero'` `Finset.sum_congr` `zero_add` `Finset.Ico_eq_empty_of_le` `instReflLe` `Nat.instCanonicallyOrderedAdd` `Set.indicator_of_notMem` `Finset.sum_const_zero` `Finset.sum_Ico_consecutive` `zero_le'` `upcrossingsBefore_le` `Set.indicator_of_mem` `upperCrossingTime_lt_of_le_upcrossingsBefore` `zero_lt_iff` `Finset.mem_Ico` `Eq.le` `upperCrossingTime_eq_of_upcrossingsBefore_lt` `Finset.sum_const` `smul_eq_mul` `mul_one` `MulZeroClass.mul_zero` `Nat.card_Ico` `add_zero`
`upcrossingsBefore_le` 📖	mathematical	`Real` `Real.instLT`	`upcrossingsBefore` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet`	—	`upcrossingsBefore_zero` `le_refl` `csSup_le` `zero_lt_iff` `LT.lt.ne` `upperCrossingTime_eq_of_bound_le` `LT.lt.le` `not_le`
`upcrossingsBefore_lt_of_exists_upcrossing` 📖	mathematical	`Real` `Real.instLT`	`upcrossingsBefore` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet`	—	`lt_of_lt_of_le` `le_csSup` `upperCrossingTime_lt_bddAbove` `Set.mem_setOf_eq` `upperCrossingTime_succ_eq` `hittingBtwn_lt_iff` `le_rfl` `lowerCrossingTime.eq_1` `hittingBtwn_le_iff_of_lt` `instWellFoundedLTNat` `le_trans` `Nat.sSup_mem` `upperCrossingTime_lt_nonempty` `upperCrossingTime_eq_upperCrossingTime_of_lt` `LE.le.trans` `LT.lt.le` `upcrossingsBefore_zero` `upperCrossingTime_zero` `Pi.bot_apply` `bot_eq_zero'` `Nat.instCanonicallyOrderedAdd` `le_refl`
`upcrossingsBefore_mono` 📖	mathematical	`Real` `Real.instLT`	`Monotone` `Nat.instPreorder` `Pi.preorder` `upcrossingsBefore` `Nat.instOrderBot` `Nat.instInfSet`	—	`csSup_le_csSup'` `upperCrossingTime_lt_bddAbove` `Set.setOf_subset_setOf_of_imp` `upperCrossingTime_eq_upperCrossingTime_of_lt` `lt_of_lt_of_le`
`upcrossingsBefore_pos_eq` 📖	mathematical	`Real` `Real.instLT`	`upcrossingsBefore` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet` `Real` `Real.instZero` `Real.instSub` `PosPart.posPart` `instPosPart` `Real.lattice` `Real.instAddGroup`	—	`crossing_pos_eq`
`upcrossingsBefore_zero` 📖	mathematical	—	`upcrossingsBefore` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet`	—	`Nat.instCanonicallyOrderedAdd` `csSup_empty`
`upcrossingsBefore_zero'` 📖	mathematical	—	`upcrossingsBefore` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet` `Pi.instZero` `MulZeroClass.toZero` `Nat.instMulZeroClass`	—	`upcrossingsBefore_zero`
`upcrossings_lt_top_iff` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `upcrossings` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet` `Top.top` `instTopENNReal` `upcrossingsBefore`	—	`CanLift.prf` `ENNReal.canLift` `LT.lt.ne` `le_rfl` `lt_of_le_of_lt` `ENNReal.coe_lt_top` `exists_nat_ge` `Nat.cast_le` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `ENNReal.instIsOrderedRing` `ENNReal.instCharZero` `LE.le.trans` `ENNReal.coe_natCast` `ENNReal.coe_le_coe`
`upperCrossingTime_bound_eq` 📖	mathematical	`Real` `Real.instLT`	`upperCrossingTime` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet`	—	`exists_upperCrossingTime_eq` `le_antisymm` `upperCrossingTime_le` `strictMonoOn_Iic_of_lt_succ` `Nat.instIsSuccArchimedean` `upperCrossingTime_lt_succ` `Nat.find_min` `StrictMonoOn.Iic_id_le` `upperCrossingTime_stabilize` `not_lt` `Nat.find_spec`
`upperCrossingTime_eq_of_bound_le` 📖	mathematical	`Real` `Real.instLT`	`upperCrossingTime` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet`	—	`le_antisymm` `upperCrossingTime_le` `le_trans` `Eq.le` `upperCrossingTime_bound_eq` `upperCrossingTime_mono`
`upperCrossingTime_eq_of_upcrossingsBefore_lt` 📖	mathematical	`Real` `Real.instLT` `upcrossingsBefore` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet`	`upperCrossingTime` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet`	—	`le_antisymm` `upperCrossingTime_le` `not_lt` `notMem_of_csSup_lt` `upperCrossingTime_lt_bddAbove`
`upperCrossingTime_eq_upperCrossingTime_of_lt` 📖	mathematical	`upperCrossingTime` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet`	`upperCrossingTime` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet`	—	`crossing_eq_crossing_of_upperCrossingTime_lt`
`upperCrossingTime_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `upperCrossingTime` `ConditionallyCompleteLinearOrderBot.toOrderBot` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf`	—	`upperCrossingTime_succ`
`upperCrossingTime_le_lowerCrossingTime` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `upperCrossingTime` `ConditionallyCompleteLinearOrderBot.toOrderBot` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `lowerCrossingTime`	—	`le_hittingBtwn` `upperCrossingTime_le`
`upperCrossingTime_lt_bddAbove` 📖	mathematical	`Real` `Real.instLT`	`BddAbove` `setOf` `upperCrossingTime` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet`	—	`exists_upperCrossingTime_eq` `LT.lt.ne` `upperCrossingTime_stabilize` `LT.lt.le` `not_le`
`upperCrossingTime_lt_lowerCrossingTime` 📖	mathematical	`Real` `Real.instLT`	`upperCrossingTime` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet` `lowerCrossingTime`	—	`lt_of_le_of_ne` `upperCrossingTime_le_lowerCrossingTime` `not_le` `le_trans` `stoppedValue_upperCrossingTime` `stoppedValue_lowerCrossingTime`
`upperCrossingTime_lt_nonempty` 📖	mathematical	—	`Set.Nonempty` `setOf` `upperCrossingTime` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet`	—	—
`upperCrossingTime_lt_of_le_upcrossingsBefore` 📖	mathematical	`Real` `Real.instLT` `upcrossingsBefore` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet`	`upperCrossingTime` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet`	—	`lt_of_le_of_lt` `upperCrossingTime_mono` `Set.Nonempty.csSup_mem` `upperCrossingTime_lt_nonempty` `BddBelow.finite_of_bddAbove` `OrderBot.bddBelow` `upperCrossingTime_lt_bddAbove`
`upperCrossingTime_lt_succ` 📖	mathematical	`Real` `Real.instLT`	`upperCrossingTime` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet`	—	`lt_of_le_of_lt` `upperCrossingTime_le_lowerCrossingTime` `lowerCrossingTime_lt_upperCrossingTime`
`upperCrossingTime_mono` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `upperCrossingTime` `ConditionallyCompleteLinearOrderBot.toOrderBot` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf`	—	`monotone_nat_of_le_succ` `le_trans` `upperCrossingTime_le_lowerCrossingTime` `lowerCrossingTime_le_upperCrossingTime_succ`
`upperCrossingTime_stabilize` 📖	mathematical	`upperCrossingTime` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet`	`upperCrossingTime` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet`	—	`le_antisymm` `upperCrossingTime_le` `le_trans` `le_of_eq` `upperCrossingTime_mono`
`upperCrossingTime_stabilize'` 📖	mathematical	`upperCrossingTime` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet`	`upperCrossingTime` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet`	—	`upperCrossingTime_stabilize` `le_antisymm` `upperCrossingTime_le`
`upperCrossingTime_succ` 📖	mathematical	—	`upperCrossingTime` `hittingBtwn` `Real` `Set.Ici` `Real.instPreorder` `lowerCrossingTimeAux`	—	`upperCrossingTime.eq_2`
`upperCrossingTime_succ_eq` 📖	mathematical	—	`upperCrossingTime` `hittingBtwn` `Real` `Set.Ici` `Real.instPreorder` `lowerCrossingTime`	—	`upperCrossingTime_succ`
`upperCrossingTime_zero` 📖	mathematical	—	`upperCrossingTime` `Bot.bot` `Pi.instBotForall` `OrderBot.toBot` `Preorder.toLE`	—	—
`upperCrossingTime_zero'` 📖	mathematical	—	`upperCrossingTime` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `ConditionallyCompleteLinearOrderBot.toOrderBot` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice`	—	`eq_bot_iff` `upperCrossingTime_le`

MeasureTheory.StronglyAdapted

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`integrable_upcrossingsBefore` 📖	mathematical	`MeasureTheory.StronglyAdapted` `Nat.instPreorder` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instLT`	`MeasureTheory.Integrable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Real.instNatCast` `MeasureTheory.upcrossingsBefore` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet`	—	`Measurable.aestronglyMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `instSecondCountableTopologyReal` `BorelSpace.opensMeasurable` `Real.borelSpace` `Measurable.comp` `measurable_from_top` `measurable_upcrossingsBefore` `MeasureTheory.HasFiniteIntegral.of_bounded` `Filter.univ_mem'` `MeasureTheory.Measure.instOuterMeasureClass` `Real.norm_eq_abs` `Nat.abs_cast` `Real.instIsOrderedRing` `Nat.cast_le` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `RCLike.charZero_rclike` `MeasureTheory.upcrossingsBefore_le`
`isStoppingTime_crossing` 📖	mathematical	`MeasureTheory.StronglyAdapted` `Nat.instPreorder` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	`MeasureTheory.IsStoppingTime` `Nat.instPreorder` `WithTop` `WithTop.natCast` `MeasureTheory.upperCrossingTime` `Nat.instOrderBot` `Nat.instInfSet` `MeasureTheory.lowerCrossingTime`	—	`MeasureTheory.isStoppingTime_const` `MeasureTheory.Adapted.isStoppingTime_hittingBtwn` `instWellFoundedLTNat` `instCountableNat` `adapted` `Real.borelSpace` `PseudoEMetricSpace.pseudoMetrizableSpace` `measurableSet_Iic` `BorelSpace.opensMeasurable` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `MeasureTheory.upperCrossingTime_succ_eq` `MeasureTheory.Adapted.isStoppingTime_hittingBtwn_isStoppingTime` `OrderTopology.of_linearLocallyFinite` `instDiscreteTopologyNat` `AlexandrovDiscrete.toFirstCountable` `DiscreteTopology.toAlexandrovDiscrete` `WithTop.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `WithTop.zeroLEOneClass` `Nat.instZeroLEOneClass` `WithTop.charZero` `Nat.instCharZero` `measurableSet_Ici` `instClosedIciTopology`
`isStoppingTime_lowerCrossingTime` 📖	mathematical	`MeasureTheory.StronglyAdapted` `Nat.instPreorder` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	`MeasureTheory.IsStoppingTime` `Nat.instPreorder` `WithTop` `WithTop.natCast` `MeasureTheory.lowerCrossingTime` `Nat.instOrderBot` `Nat.instInfSet`	—	`isStoppingTime_crossing`
`isStoppingTime_upperCrossingTime` 📖	mathematical	`MeasureTheory.StronglyAdapted` `Nat.instPreorder` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	`MeasureTheory.IsStoppingTime` `Nat.instPreorder` `WithTop` `WithTop.natCast` `MeasureTheory.upperCrossingTime` `Nat.instOrderBot` `Nat.instInfSet`	—	`isStoppingTime_crossing`
`measurable_upcrossings` 📖	mathematical	`MeasureTheory.StronglyAdapted` `Nat.instPreorder` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instLT`	`Measurable` `ENNReal` `ENNReal.measurableSpace` `MeasureTheory.upcrossings` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet`	—	`Measurable.iSup` `ENNReal.borelSpace` `ENNReal.instOrderTopology` `ENNReal.instSecondCountableTopology` `instCountableNat` `Measurable.comp` `measurable_from_top` `measurable_upcrossingsBefore`
`measurable_upcrossingsBefore` 📖	mathematical	`MeasureTheory.StronglyAdapted` `Nat.instPreorder` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instLT`	`Measurable` `Nat.instMeasurableSpace` `MeasureTheory.upcrossingsBefore` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet`	—	`MeasureTheory.upcrossingsBefore_eq_sum` `Finset.measurable_fun_sum` `ContinuousAdd.measurableMul₂` `Nat.borelSpace` `TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace` `Countable.LindelofSpace` `instCountableNat` `PseudoEMetricSpace.pseudoMetrizableSpace` `IsSemitopologicalSemiring.toContinuousAdd` `IsTopologicalSemiring.toIsSemitopologicalSemiring` `DiscreteTopology.topologicalSemiring` `instDiscreteTopologyNat` `Measurable.indicator` `measurable_const` `MeasureTheory.Filtration.le` `WithTop.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `WithTop.zeroLEOneClass` `Nat.instZeroLEOneClass` `WithTop.charZero` `Nat.instCharZero` `MeasureTheory.IsStoppingTime.measurableSet_lt_of_pred` `isStoppingTime_upperCrossingTime`
`upcrossingStrat` 📖	mathematical	`MeasureTheory.StronglyAdapted` `Nat.instPreorder` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	`MeasureTheory.StronglyAdapted` `Nat.instPreorder` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `MeasureTheory.upcrossingStrat`	—	`Finset.stronglyMeasurable_fun_sum` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `MeasureTheory.StronglyMeasurable.indicator` `MeasureTheory.stronglyMeasurable_const` `isStoppingTime_lowerCrossingTime` `isStoppingTime_upperCrossingTime` `MeasurableSet.inter` `WithTop.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `WithTop.zeroLEOneClass` `Nat.instZeroLEOneClass` `WithTop.charZero` `Nat.instCharZero` `MeasurableSet.compl`

MeasureTheory.Submartingale

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mul_integral_upcrossingsBefore_le_integral_pos_part` 📖	mathematical	`MeasureTheory.Submartingale` `Real` `Nat.instPreorder` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Real.instCompleteSpace` `Real.instLE`	`Real` `Real.instLE` `Real.instMul` `Real.instSub` `MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Real.instNatCast` `MeasureTheory.upcrossingsBefore` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet`	—	`Real.instCompleteSpace` `MeasureTheory.mul_integral_upcrossingsBefore_le_integral_pos_part_aux` `le_trans` `mul_nonpos_of_nonpos_of_nonneg` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `sub_nonpos` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `MeasureTheory.integral_nonneg` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Nat.cast_nonneg'` `Real.instZeroLEOneClass` `posPart_nonneg`
`mul_lintegral_upcrossings_le_lintegral_pos_part` 📖	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` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofReal` `Real` `Real.instSub` `MeasureTheory.lintegral` `MeasureTheory.upcrossings` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instInfSet` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `PosPart.posPart` `instPosPart` `Real.lattice` `Real.instAddGroup`	—	`Real.instCompleteSpace` `MeasureTheory.ofReal_integral_eq_lintegral_ofReal` `integrable` `pos` `TopologicalLattice.toContinuousSup` `HasSolidNorm.toTopologicalLattice` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `sub_martingale` `IsOrderedAddMonoid.toAddLeftMono` `MeasureTheory.martingale_const` `Filter.Eventually.of_forall` `MeasureTheory.Measure.instOuterMeasureClass` `posPart_nonneg` `MeasureTheory.lintegral_iSup'` `Measurable.comp_aemeasurable` `measurable_from_top` `Measurable.aemeasurable` `MeasureTheory.StronglyAdapted.measurable_upcrossingsBefore` `stronglyAdapted` `Filter.univ_mem'` `Nat.cast_le` `ENNReal.instIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `ENNReal.instIsOrderedRing` `ENNReal.instCharZero` `MeasureTheory.upcrossingsBefore_mono` `ENNReal.mul_iSup` `MeasureTheory.lintegral_coe_eq_integral` `NNReal.coe_natCast` `MeasureTheory.StronglyAdapted.integrable_upcrossingsBefore` `ENNReal.ofReal_mul` `LT.lt.le` `sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Real.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `covariant_swap_add_of_covariant_add` `LE.le.trans` `ENNReal.ofReal_le_ofReal` `mul_integral_upcrossingsBefore_le_integral_pos_part` `le_iSup` `ENNReal.ofReal_of_nonpos` `sub_nonpos` `MulZeroClass.zero_mul` `zero_le` `ENNReal.instCanonicallyOrderedAdd`
`sum_mul_upcrossingStrat_le` 📖	mathematical	`MeasureTheory.Submartingale` `Real` `Nat.instPreorder` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Real.instCompleteSpace` `Real.instLE`	`Real` `Real.instLE` `MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Finset.sum` `Pi.addCommMonoid` `Real.instAddCommMonoid` `Finset.range` `Pi.instMul` `Real.instMul` `MeasureTheory.upcrossingStrat` `Pi.instSub` `Real.instSub`	—	`Real.instCompleteSpace` `setIntegral_le` `Real.instIsOrderedAddMonoid` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `MeasureTheory.IsFiniteMeasure.sigmaFiniteFiltration` `sum_sub_upcrossingStrat_mul` `zero_le` `Nat.instCanonicallyOrderedAdd` `MeasurableSet.univ` `le_trans` `MeasureTheory.integral_zero'` `MeasureTheory.setIntegral_univ` `Finset.sum_congr` `sub_mul` `one_mul` `Finset.sum_apply` `Finset.sum_sub_distrib` `MeasureTheory.integral_sub` `MeasureTheory.Integrable.sub` `MeasureTheory.integrable_finset_sum` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `integrable` `sum_upcrossingStrat_mul` `sub_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Finset.sum_range_sub` `MeasureTheory.integral_sub'`
`sum_sub_upcrossingStrat_mul` 📖	mathematical	`MeasureTheory.Submartingale` `Real` `Nat.instPreorder` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Real.instCompleteSpace` `Real.instLE`	`MeasureTheory.Submartingale` `Real` `Nat.instPreorder` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Real.instCompleteSpace` `Real.instLE` `Finset.sum` `Pi.addCommMonoid` `Real.instAddCommMonoid` `Finset.range` `Pi.instMul` `Real.instMul` `Pi.instSub` `Real.instSub` `Pi.instOne` `Real.instOne` `MeasureTheory.upcrossingStrat`	—	`Real.instCompleteSpace` `sum_mul_sub` `MeasureTheory.StronglyMeasurable.sub` `IsTopologicalAddGroup.to_continuousSub` `instIsTopologicalAddGroupReal` `MeasureTheory.stronglyAdapted_const` `MeasureTheory.StronglyAdapted.upcrossingStrat` `stronglyAdapted` `sub_le_self` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `MeasureTheory.upcrossingStrat_nonneg` `covariant_swap_add_of_covariant_add`
`sum_upcrossingStrat_mul` 📖	mathematical	`MeasureTheory.Submartingale` `Real` `Nat.instPreorder` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Real.instCompleteSpace` `Real.instLE`	`MeasureTheory.Submartingale` `Real` `Nat.instPreorder` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Real.instCompleteSpace` `Real.instLE` `Finset.sum` `Pi.addCommMonoid` `Real.instAddCommMonoid` `Finset.range` `Pi.instMul` `Real.instMul` `MeasureTheory.upcrossingStrat` `Pi.instSub` `Real.instSub`	—	`Real.instCompleteSpace` `sum_mul_sub` `MeasureTheory.StronglyAdapted.upcrossingStrat` `stronglyAdapted` `MeasureTheory.upcrossingStrat_le_one` `MeasureTheory.upcrossingStrat_nonneg`

---

← Back to Index