Basic

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

Statistics

Metric	Count
Definitions `Martingale`, `Submartingale`, `Supermartingale`	3
Theorems `add`, `condExp_ae_eq`, `eq_zero_of_predictable`, `eq_zero_of_predictable'`, `integrable`, `neg`, `setIntegral_eq`, `smul`, `stronglyAdapted`, `stronglyMeasurable`, `sub`, `submartingale`, `supermartingale`, `add`, `add_martingale`, `ae_le_condExp`, `condExp_sub_nonneg`, `integrable`, `integrable_stoppedValue`, `neg`, `pos`, `setIntegral_le`, `smul_nonneg`, `smul_nonpos`, `stronglyAdapted`, `stronglyMeasurable`, `sub_martingale`, `sub_supermartingale`, `sum_mul_sub`, `sum_mul_sub'`, `sum_smul_sub`, `sum_smul_sub'`, `sup`, `zero_le_of_predictable`, `zero_le_of_predictable'`, `add`, `add_martingale`, `condExp_ae_le`, `integrable`, `le_zero_of_predictable`, `le_zero_of_predictable'`, `neg`, `setIntegral_le`, `smul_nonneg`, `smul_nonpos`, `stronglyAdapted`, `stronglyMeasurable`, `sub_martingale`, `sub_submartingale`, `martingale_condExp`, `martingale_const`, `martingale_const_fun`, `martingale_iff`, `martingale_nat`, `martingale_of_condExp_sub_eq_zero_nat`, `martingale_of_setIntegral_eq_succ`, `martingale_zero`, `submartingale_iff_condExp_sub_nonneg`, `submartingale_nat`, `submartingale_of_condExp_sub_nonneg`, `submartingale_of_condExp_sub_nonneg_nat`, `submartingale_of_setIntegral_le`, `submartingale_of_setIntegral_le_succ`, `supermartingale_nat`, `supermartingale_of_condExp_sub_nonneg_nat`, `supermartingale_of_setIntegral_succ_le`	66
Total	69

MeasureTheory

Definitions

Name	Category	Theorems
`Martingale` 📖	MathDef	10 math math: `martingale_condExp`, `martingale_const`, `martingale_iff`, `ProbabilityTheory.Kernel.martingale_densityProcess`, `martingale_of_setIntegral_eq_succ`, `martingale_zero`, `martingale_of_condExp_sub_eq_zero_nat`, `martingale_nat`, `martingale_martingalePart`, `martingale_const_fun`
`Submartingale` 📖	MathDef	12 math math: `submartingale_iff_expected_stoppedValue_mono`, `Martingale.submartingale`, `martingale_iff`, `submartingale_nat`, `submartingale_of_setIntegral_le_succ`, `submartingale_of_setIntegral_le`, `submartingale_of_condExp_sub_nonneg_nat`, `Supermartingale.smul_nonpos`, `Supermartingale.neg`, `submartingale_of_expected_stoppedValue_mono`, `submartingale_of_condExp_sub_nonneg`, `submartingale_iff_condExp_sub_nonneg`
`Supermartingale` 📖	MathDef	7 math math: `supermartingale_of_setIntegral_succ_le`, `supermartingale_nat`, `martingale_iff`, `Submartingale.neg`, `Martingale.supermartingale`, `Submartingale.smul_nonpos`, `supermartingale_of_condExp_sub_nonneg_nat`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`martingale_condExp` 📖	mathematical	—	`Martingale` `condExp` `Filtration.seq`	—	`Measure.instOuterMeasureClass` `stronglyMeasurable_condExp` `condExp_condExp_of_le` `Filtration.mono` `Filtration.le` `sigmaFinite_of_sigmaFiniteFiltration`
`martingale_const` 📖	mathematical	—	`Martingale`	—	`Measure.instOuterMeasureClass` `stronglyAdapted_const` `condExp_const` `Filtration.le` `Filter.EventuallyEq.refl`
`martingale_const_fun` 📖	mathematical	`StronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Filtration.seq` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `Integrable` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`Martingale`	—	`Measure.instOuterMeasureClass` `StronglyMeasurable.mono` `Filtration.mono` `bot_le` `condExp_of_stronglyMeasurable` `Filtration.le` `sigmaFinite_of_sigmaFiniteFiltration` `Filter.EventuallyEq.refl`
`martingale_iff` 📖	mathematical	—	`Martingale` `Supermartingale` `Preorder.toLE` `PartialOrder.toPreorder` `Submartingale`	—	`Martingale.supermartingale` `Martingale.submartingale` `Measure.instOuterMeasureClass` `Filter.EventuallyLE.antisymm`
`martingale_nat` 📖	mathematical	`StronglyAdapted` `Nat.instPreorder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Integrable` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Filter.EventuallyEq` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `condExp` `Filtration.seq`	`Martingale`	—	`Measure.instOuterMeasureClass` `Nat.le_induction` `ae_of_all` `condExp_of_stronglyMeasurable` `Filtration.le` `sigmaFinite_of_sigmaFiniteFiltration` `IsFiniteMeasure.sigmaFiniteFiltration` `Filter.mp_mem` `Filtration.condExp_condExp` `condExp_congr_ae` `Filter.univ_mem'`
`martingale_of_condExp_sub_eq_zero_nat` 📖	mathematical	`StronglyAdapted` `Nat.instPreorder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Integrable` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Filter.EventuallyEq` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `condExp` `Filtration.seq` `Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Pi.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`Martingale`	—	`Measure.instOuterMeasureClass` `martingale_nat` `condExp_of_stronglyMeasurable` `Filtration.le` `sigmaFinite_of_sigmaFiniteFiltration` `IsFiniteMeasure.sigmaFiniteFiltration` `Filter.eventuallyEq_comm` `Filter.eventuallyEq_iff_sub` `Filter.EventuallyEq.trans` `Filter.EventuallyEq.symm` `condExp_sub`
`martingale_of_setIntegral_eq_succ` 📖	mathematical	`StronglyAdapted` `Nat.instPreorder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Integrable` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `integral` `Measure.restrict`	`Martingale`	—	`martingale_nat` `ae_eq_of_ae_eq_trim` `Filtration.le` `Integrable.ae_eq_of_forall_setIntegral_eq` `Integrable.trim` `integrable_condExp` `stronglyMeasurable_condExp` `setIntegral_trim` `setIntegral_condExp` `sigmaFinite_of_sigmaFiniteFiltration` `IsFiniteMeasure.sigmaFiniteFiltration`
`martingale_zero` 📖	mathematical	—	`Martingale` `Pi.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`Measure.instOuterMeasureClass` `stronglyAdapted_zero` `condExp_zero`
`submartingale_iff_condExp_sub_nonneg` 📖	mathematical	—	`Submartingale` `Preorder.toLE` `PartialOrder.toPreorder` `StronglyAdapted` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Integrable` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Filter.EventuallyLE` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Pi.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `condExp` `Filtration.seq` `Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`Measure.instOuterMeasureClass` `Submartingale.stronglyAdapted` `Submartingale.integrable` `Submartingale.condExp_sub_nonneg` `submartingale_of_condExp_sub_nonneg`
`submartingale_nat` 📖	mathematical	`StronglyAdapted` `Nat.instPreorder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Integrable` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Filter.EventuallyLE` `Preorder.toLE` `PartialOrder.toPreorder` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `condExp` `Filtration.seq`	`Submartingale`	—	`Measure.instOuterMeasureClass` `Nat.le_induction` `ae_of_all` `condExp_of_stronglyMeasurable` `Filtration.le` `sigmaFinite_of_sigmaFiniteFiltration` `IsFiniteMeasure.sigmaFiniteFiltration` `le_refl` `Filter.mp_mem` `Filtration.condExp_condExp` `condExp_mono` `integrable_condExp` `Filter.univ_mem'` `le_imp_le_of_le_of_le`
`submartingale_of_condExp_sub_nonneg` 📖	mathematical	`StronglyAdapted` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Integrable` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Filter.EventuallyLE` `Preorder.toLE` `PartialOrder.toPreorder` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Pi.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `condExp` `Filtration.seq` `Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	`Submartingale`	—	`Measure.instOuterMeasureClass` `condExp_of_stronglyMeasurable` `Filtration.le` `sigmaFinite_of_sigmaFiniteFiltration` `Filter.eventually_sub_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Filter.EventuallyLE.trans` `Filter.EventuallyEq.le` `condExp_sub`
`submartingale_of_condExp_sub_nonneg_nat` 📖	mathematical	`StronglyAdapted` `Nat.instPreorder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Integrable` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Filter.EventuallyLE` `Preorder.toLE` `PartialOrder.toPreorder` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Pi.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `condExp` `Filtration.seq` `Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	`Submartingale`	—	`Measure.instOuterMeasureClass` `submartingale_nat` `condExp_of_stronglyMeasurable` `Filtration.le` `sigmaFinite_of_sigmaFiniteFiltration` `IsFiniteMeasure.sigmaFiniteFiltration` `Filter.eventually_sub_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Filter.EventuallyLE.trans` `Filter.EventuallyEq.le` `condExp_sub`
`submartingale_of_setIntegral_le` 📖	mathematical	`StronglyAdapted` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Integrable` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Real.instLE` `integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Measure.restrict`	`Submartingale` `Real.instCompleteSpace`	—	`Measure.instOuterMeasureClass` `Real.instCompleteSpace` `Filtration.le` `ae_nonneg_of_forall_setIntegral_nonneg` `Integrable.trim` `Integrable.sub` `integrable_condExp` `StronglyMeasurable.sub` `IsTopologicalAddGroup.to_continuousSub` `instIsTopologicalAddGroupReal` `stronglyMeasurable_condExp` `setIntegral_trim` `integral_sub'` `Integrable.integrableOn` `sub_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `setIntegral_condExp` `sigmaFinite_of_sigmaFiniteFiltration` `Filter.mp_mem` `Filter.univ_mem'` `ae_le_of_ae_le_trim`
`submartingale_of_setIntegral_le_succ` 📖	mathematical	`StronglyAdapted` `Nat.instPreorder` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Integrable` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Real.instLE` `integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Measure.restrict`	`Submartingale` `Real.instCompleteSpace`	—	`submartingale_of_setIntegral_le` `IsFiniteMeasure.sigmaFiniteFiltration` `le_refl` `LE.le.trans` `Filtration.mono`
`supermartingale_nat` 📖	mathematical	`StronglyAdapted` `Nat.instPreorder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Integrable` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Filter.EventuallyLE` `Preorder.toLE` `PartialOrder.toPreorder` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `condExp` `Filtration.seq`	`Supermartingale`	—	`Measure.instOuterMeasureClass` `neg_neg` `Submartingale.neg` `IsOrderedAddMonoid.toAddLeftMono` `submartingale_nat` `StronglyAdapted.neg` `IsTopologicalAddGroup.toContinuousNeg` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Integrable.neg` `Filter.EventuallyLE.trans` `Filter.mp_mem` `Filter.univ_mem'` `neg_le_neg` `Filter.EventuallyEq.le` `Filter.EventuallyEq.symm` `condExp_neg`
`supermartingale_of_condExp_sub_nonneg_nat` 📖	mathematical	`StronglyAdapted` `Nat.instPreorder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Integrable` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Filter.EventuallyLE` `Preorder.toLE` `PartialOrder.toPreorder` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Pi.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `condExp` `Filtration.seq` `Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	`Supermartingale`	—	`Measure.instOuterMeasureClass` `neg_neg` `Submartingale.neg` `IsOrderedAddMonoid.toAddLeftMono` `submartingale_of_condExp_sub_nonneg_nat` `StronglyAdapted.neg` `IsTopologicalAddGroup.toContinuousNeg` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Integrable.neg` `neg_sub_neg`
`supermartingale_of_setIntegral_succ_le` 📖	mathematical	`StronglyAdapted` `Nat.instPreorder` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Integrable` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Real.instLE` `integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Measure.restrict`	`Supermartingale` `Real.instCompleteSpace`	—	`Real.instCompleteSpace` `neg_neg` `Submartingale.neg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `submartingale_of_setIntegral_le_succ` `StronglyAdapted.neg` `IsTopologicalRing.toContinuousNeg` `instIsTopologicalRingReal` `Integrable.neg` `integral_neg` `covariant_swap_add_of_covariant_add`

MeasureTheory.Martingale

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`MeasureTheory.Martingale`	`Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.StronglyAdapted.add` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `stronglyAdapted` `Filter.EventuallyEq.trans` `MeasureTheory.condExp_add` `integrable` `Filter.EventuallyEq.add`
`condExp_ae_eq` 📖	mathematical	`MeasureTheory.Martingale` `Preorder.toLE`	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.condExp` `MeasureTheory.Filtration.seq`	—	`MeasureTheory.Measure.instOuterMeasureClass`
`eq_zero_of_predictable` 📖	mathematical	`MeasureTheory.Martingale` `Nat.instPreorder` `MeasureTheory.StronglyAdapted` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Filter.EventuallyEq.refl` `Filter.EventuallyEq.trans` `Filter.EventuallyEq.symm` `Filter.Germ.coe_eq` `MeasureTheory.condExp_of_stronglyMeasurable` `MeasureTheory.Filtration.le` `MeasureTheory.sigmaFinite_of_sigmaFiniteFiltration` `integrable`
`eq_zero_of_predictable'` 📖	mathematical	`MeasureTheory.Martingale` `Nat.instPreorder` `MeasureTheory.IsPredictable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Nat.instOrderBot`	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`eq_zero_of_predictable` `Measurable.stronglyMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `BorelSpace.opensMeasurable` `MeasureTheory.IsPredictable.measurable_add_one` `EMetricSpace.metrizableSpace`
`integrable` 📖	mathematical	`MeasureTheory.Martingale`	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`MeasureTheory.Integrable.congr` `MeasureTheory.integrable_condExp` `condExp_ae_eq` `le_refl`
`neg` 📖	mathematical	`MeasureTheory.Martingale`	`Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.StronglyAdapted.neg` `IsTopologicalAddGroup.toContinuousNeg` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `stronglyAdapted` `Filter.EventuallyEq.trans` `MeasureTheory.condExp_neg` `Filter.EventuallyEq.neg`
`setIntegral_eq` 📖	mathematical	`MeasureTheory.Martingale` `Preorder.toLE` `MeasurableSet` `MeasureTheory.Filtration.seq`	`MeasureTheory.integral` `MeasureTheory.Measure.restrict`	—	`MeasureTheory.setIntegral_condExp` `MeasureTheory.Filtration.le` `MeasureTheory.sigmaFinite_of_sigmaFiniteFiltration` `integrable` `MeasureTheory.setIntegral_congr_ae` `Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `Filter.univ_mem'`
`smul` 📖	mathematical	`MeasureTheory.Martingale`	`Real` `Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.StronglyAdapted.smul` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `stronglyAdapted` `Filter.EventuallyEq.trans` `MeasureTheory.condExp_smul` `Filter.Eventually.mono`
`stronglyAdapted` 📖	mathematical	`MeasureTheory.Martingale`	`MeasureTheory.StronglyAdapted` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`MeasureTheory.Measure.instOuterMeasureClass`
`stronglyMeasurable` 📖	mathematical	`MeasureTheory.Martingale`	`MeasureTheory.StronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `MeasureTheory.Filtration.seq`	—	`stronglyAdapted`
`sub` 📖	mathematical	`MeasureTheory.Martingale`	`Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`sub_eq_add_neg` `add` `neg`
`submartingale` 📖	mathematical	`MeasureTheory.Martingale`	`MeasureTheory.Submartingale` `Preorder.toLE`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Filter.EventuallyEq.le` `Filter.EventuallyEq.symm` `integrable`
`supermartingale` 📖	mathematical	`MeasureTheory.Martingale`	`MeasureTheory.Supermartingale` `Preorder.toLE`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Filter.EventuallyEq.le` `integrable`

MeasureTheory.Submartingale

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`MeasureTheory.Submartingale` `Preorder.toLE`	`Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.StronglyAdapted.add` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Filter.EventuallyLE.trans` `Filter.mp_mem` `Filter.univ_mem'` `add_le_add` `covariant_swap_add_of_covariant_add` `Filter.EventuallyEq.le` `Filter.EventuallyEq.symm` `MeasureTheory.condExp_add` `integrable` `MeasureTheory.Integrable.add`
`add_martingale` 📖	mathematical	`MeasureTheory.Submartingale` `Preorder.toLE` `MeasureTheory.Martingale`	`Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`add` `MeasureTheory.Martingale.submartingale`
`ae_le_condExp` 📖	mathematical	`MeasureTheory.Submartingale` `Preorder.toLE`	`Filter.EventuallyLE` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.condExp` `MeasureTheory.Filtration.seq`	—	`MeasureTheory.Measure.instOuterMeasureClass`
`condExp_sub_nonneg` 📖	mathematical	`MeasureTheory.Submartingale` `Preorder.toLE` `PartialOrder.toPreorder`	`Filter.EventuallyLE` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `Pi.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `MeasureTheory.condExp` `MeasureTheory.Filtration.seq` `Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Filtration.le` `Filter.EventuallyLE.trans` `Filter.eventually_sub_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `MeasureTheory.condExp_of_stronglyMeasurable` `stronglyAdapted` `integrable` `Filter.EventuallyEq.le` `Filter.EventuallyEq.symm` `MeasureTheory.condExp_sub` `MeasureTheory.condExp_of_not_sigmaFinite` `Filter.EventuallyLE.refl`
`integrable` 📖	mathematical	`MeasureTheory.Submartingale`	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`MeasureTheory.Measure.instOuterMeasureClass`
`integrable_stoppedValue` 📖	mathematical	`MeasureTheory.Submartingale` `Nat.instPreorder` `MeasureTheory.IsStoppingTime` `ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `ENat.instNatCast`	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `MeasureTheory.stoppedValue`	—	`MeasureTheory.integrable_stoppedValue` `integrable`
`neg` 📖	mathematical	`MeasureTheory.Submartingale` `Preorder.toLE`	`MeasureTheory.Supermartingale` `Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.StronglyAdapted.neg` `IsTopologicalAddGroup.toContinuousNeg` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Filter.EventuallyLE.trans` `Filter.EventuallyEq.le` `MeasureTheory.condExp_neg` `Filter.mp_mem` `Filter.univ_mem'` `covariant_swap_add_of_covariant_add` `MeasureTheory.Integrable.neg`
`pos` 📖	mathematical	`MeasureTheory.Submartingale` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf`	`PosPart.posPart` `instPosPart` `Pi.instLattice` `Pi.addGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`sup` `MeasureTheory.Martingale.submartingale` `MeasureTheory.martingale_zero`
`setIntegral_le` 📖	mathematical	`MeasureTheory.Submartingale` `Preorder.toLE` `PartialOrder.toPreorder` `MeasurableSet` `MeasureTheory.Filtration.seq`	`MeasureTheory.integral` `MeasureTheory.Measure.restrict`	—	`neg_le_neg_iff` `IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add` `MeasureTheory.integral_neg` `MeasureTheory.Supermartingale.setIntegral_le` `neg`
`smul_nonneg` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `MeasureTheory.Submartingale` `Preorder.toLE` `PartialOrder.toPreorder`	`Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField`	—	`neg_neg` `smul_neg` `MeasureTheory.Supermartingale.neg` `IsOrderedAddMonoid.toAddLeftMono` `MeasureTheory.Supermartingale.smul_nonneg` `neg`
`smul_nonpos` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `MeasureTheory.Submartingale` `Preorder.toLE` `PartialOrder.toPreorder`	`MeasureTheory.Supermartingale` `Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField`	—	`neg_neg` `neg_smul` `neg` `IsOrderedAddMonoid.toAddLeftMono` `smul_nonneg` `neg_nonneg` `Real.instIsOrderedAddMonoid`
`stronglyAdapted` 📖	mathematical	`MeasureTheory.Submartingale`	`MeasureTheory.StronglyAdapted` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`MeasureTheory.Measure.instOuterMeasureClass`
`stronglyMeasurable` 📖	mathematical	`MeasureTheory.Submartingale`	`MeasureTheory.StronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `MeasureTheory.Filtration.seq`	—	`stronglyAdapted`
`sub_martingale` 📖	mathematical	`MeasureTheory.Submartingale` `Preorder.toLE` `MeasureTheory.Martingale`	`Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`sub_supermartingale` `MeasureTheory.Martingale.supermartingale`
`sub_supermartingale` 📖	mathematical	`MeasureTheory.Submartingale` `Preorder.toLE` `MeasureTheory.Supermartingale`	`Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`sub_eq_add_neg` `add` `MeasureTheory.Supermartingale.neg`
`sum_mul_sub` 📖	mathematical	`MeasureTheory.Submartingale` `Real` `Nat.instPreorder` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Real.instCompleteSpace` `Real.instLE` `MeasureTheory.StronglyAdapted` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero`	`Finset.sum` `Pi.addCommMonoid` `Real.instAddCommMonoid` `Finset.range` `Pi.instMul` `Real.instMul` `Pi.instSub` `Real.instSub`	—	`Real.instCompleteSpace` `sum_smul_sub` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid`
`sum_mul_sub'` 📖	mathematical	`MeasureTheory.Submartingale` `Real` `Nat.instPreorder` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Real.instCompleteSpace` `Real.instLE` `MeasureTheory.StronglyAdapted` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero`	`Finset.sum` `Pi.addCommMonoid` `Real.instAddCommMonoid` `Finset.range` `Pi.instMul` `Real.instMul` `Pi.instSub` `Real.instSub`	—	`Real.instCompleteSpace` `sum_smul_sub'` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid`
`sum_smul_sub` 📖	mathematical	`MeasureTheory.Submartingale` `Nat.instPreorder` `Preorder.toLE` `PartialOrder.toPreorder` `MeasureTheory.StronglyAdapted` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instLE` `Real.instZero`	`Finset.sum` `Pi.addCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Finset.range` `Pi.smul'` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `NormedSpace.toModule` `Real.normedField` `Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`Eq.trans_le` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `MeasureTheory.integrable_finset_sum'` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `MeasureTheory.Integrable.bdd_smul` `NormedSpace.toIsBoundedSMul` `MeasureTheory.Integrable.sub` `integrable` `MeasureTheory.StronglyMeasurable.aestronglyMeasurable` `MeasureTheory.StronglyAdapted.stronglyMeasurable` `MeasureTheory.ae_of_all` `MeasureTheory.Measure.instOuterMeasureClass` `Finset.stronglyMeasurable_sum` `MeasureTheory.StronglyMeasurable.smul` `IsBoundedSMul.continuousSMul` `MeasureTheory.StronglyAdapted.stronglyMeasurable_le` `LT.lt.le` `Finset.mem_range` `MeasureTheory.StronglyMeasurable.sub` `IsTopologicalAddGroup.to_continuousSub` `stronglyAdapted` `MeasureTheory.submartingale_of_condExp_sub_nonneg_nat` `Finset.sum_Ico_eq_sub` `Finset.sum_congr` `Nat.Ico_succ_singleton` `Finset.sum_singleton` `Filter.mp_mem` `MeasureTheory.condExp_smul_of_aestronglyMeasurable_left` `condExp_sub_nonneg` `Filter.univ_mem'` `smul_zero` `le_imp_le_of_le_of_le` `smul_le_smul_of_nonneg_right` `PosSMulMono.toSMulPosMono` `Real.instIsOrderedRing` `IsOrderedModule.toPosSMulMono` `le_refl` `smul_le_smul_of_nonneg_left`
`sum_smul_sub'` 📖	mathematical	`MeasureTheory.Submartingale` `Nat.instPreorder` `Preorder.toLE` `PartialOrder.toPreorder` `MeasureTheory.StronglyAdapted` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instLE` `Real.instZero`	`Finset.sum` `Pi.addCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Finset.range` `Pi.smul'` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `NormedSpace.toModule` `Real.normedField` `Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`sum_smul_sub`
`sup` 📖	mathematical	`MeasureTheory.Submartingale` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf`	`Pi.instMaxForall_mathlib` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.StronglyMeasurable.sup` `stronglyAdapted` `Filter.EventuallyLE.sup_le` `Filter.EventuallyLE.trans` `MeasureTheory.condExp_mono` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `integrable` `MeasureTheory.Integrable.sup` `Filter.Eventually.of_forall` `le_sup_left` `le_sup_right`
`zero_le_of_predictable` 📖	mathematical	`MeasureTheory.Submartingale` `Nat.instPreorder` `Preorder.toLE` `MeasureTheory.StronglyAdapted` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`Filter.EventuallyLE` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Filter.EventuallyLE.refl` `Filter.EventuallyLE.trans` `Filter.EventuallyLE.trans_eq` `Filter.Germ.coe_eq` `MeasureTheory.condExp_of_stronglyMeasurable` `MeasureTheory.Filtration.le` `MeasureTheory.sigmaFinite_of_sigmaFiniteFiltration` `integrable`
`zero_le_of_predictable'` 📖	mathematical	`MeasureTheory.Submartingale` `Nat.instPreorder` `Preorder.toLE` `MeasureTheory.IsPredictable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Nat.instOrderBot`	`Filter.EventuallyLE` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`zero_le_of_predictable` `Measurable.stronglyMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `BorelSpace.opensMeasurable` `MeasureTheory.IsPredictable.measurable_add_one` `EMetricSpace.metrizableSpace`

MeasureTheory.Supermartingale

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`MeasureTheory.Supermartingale` `Preorder.toLE`	`Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.StronglyAdapted.add` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Filter.EventuallyLE.trans` `Filter.EventuallyEq.le` `MeasureTheory.condExp_add` `integrable` `Filter.mp_mem` `Filter.univ_mem'` `add_le_add` `covariant_swap_add_of_covariant_add` `MeasureTheory.Integrable.add`
`add_martingale` 📖	mathematical	`MeasureTheory.Supermartingale` `Preorder.toLE` `MeasureTheory.Martingale`	`Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`add` `MeasureTheory.Martingale.supermartingale`
`condExp_ae_le` 📖	mathematical	`MeasureTheory.Supermartingale` `Preorder.toLE`	`Filter.EventuallyLE` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.condExp` `MeasureTheory.Filtration.seq`	—	`MeasureTheory.Measure.instOuterMeasureClass`
`integrable` 📖	mathematical	`MeasureTheory.Supermartingale`	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`MeasureTheory.Measure.instOuterMeasureClass`
`le_zero_of_predictable` 📖	mathematical	`MeasureTheory.Supermartingale` `Nat.instPreorder` `Preorder.toLE` `MeasureTheory.StronglyAdapted` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`Filter.EventuallyLE` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Filter.EventuallyLE.refl` `Filter.EventuallyLE.trans` `Filter.EventuallyEq.trans_le` `Filter.EventuallyEq.symm` `Filter.Germ.coe_eq` `MeasureTheory.condExp_of_stronglyMeasurable` `MeasureTheory.Filtration.le` `MeasureTheory.sigmaFinite_of_sigmaFiniteFiltration` `integrable`
`le_zero_of_predictable'` 📖	mathematical	`MeasureTheory.Supermartingale` `Nat.instPreorder` `Preorder.toLE` `MeasureTheory.IsPredictable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Nat.instOrderBot`	`Filter.EventuallyLE` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`le_zero_of_predictable` `Measurable.stronglyMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `BorelSpace.opensMeasurable` `MeasureTheory.IsPredictable.measurable_add_one` `EMetricSpace.metrizableSpace`
`neg` 📖	mathematical	`MeasureTheory.Supermartingale` `Preorder.toLE`	`MeasureTheory.Submartingale` `Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.StronglyAdapted.neg` `IsTopologicalAddGroup.toContinuousNeg` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Filter.EventuallyLE.trans` `Filter.mp_mem` `Filter.univ_mem'` `covariant_swap_add_of_covariant_add` `Filter.EventuallyEq.le` `Filter.EventuallyEq.symm` `MeasureTheory.condExp_neg` `MeasureTheory.Integrable.neg`
`setIntegral_le` 📖	mathematical	`MeasureTheory.Supermartingale` `Preorder.toLE` `PartialOrder.toPreorder` `MeasurableSet` `MeasureTheory.Filtration.seq`	`MeasureTheory.integral` `MeasureTheory.Measure.restrict`	—	`MeasureTheory.setIntegral_condExp` `MeasureTheory.Filtration.le` `MeasureTheory.sigmaFinite_of_sigmaFiniteFiltration` `integrable` `MeasureTheory.setIntegral_mono_ae` `MeasureTheory.Integrable.integrableOn` `MeasureTheory.integrable_condExp` `Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `Filter.univ_mem'`
`smul_nonneg` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `MeasureTheory.Supermartingale` `Preorder.toLE` `PartialOrder.toPreorder`	`Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.StronglyAdapted.smul` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Filter.mp_mem` `MeasureTheory.condExp_smul` `Filter.univ_mem'` `smul_le_smul_of_nonneg_left` `IsOrderedModule.toPosSMulMono` `MeasureTheory.Integrable.smul`
`smul_nonpos` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `MeasureTheory.Supermartingale` `Preorder.toLE` `PartialOrder.toPreorder`	`MeasureTheory.Submartingale` `Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField`	—	`neg_neg` `neg_smul` `neg` `IsOrderedAddMonoid.toAddLeftMono` `smul_nonneg` `neg_nonneg` `Real.instIsOrderedAddMonoid`
`stronglyAdapted` 📖	mathematical	`MeasureTheory.Supermartingale`	`MeasureTheory.StronglyAdapted` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`MeasureTheory.Measure.instOuterMeasureClass`
`stronglyMeasurable` 📖	mathematical	`MeasureTheory.Supermartingale`	`MeasureTheory.StronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `MeasureTheory.Filtration.seq`	—	`stronglyAdapted`
`sub_martingale` 📖	mathematical	`MeasureTheory.Supermartingale` `Preorder.toLE` `MeasureTheory.Martingale`	`Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`sub_submartingale` `MeasureTheory.Martingale.submartingale`
`sub_submartingale` 📖	mathematical	`MeasureTheory.Supermartingale` `Preorder.toLE` `MeasureTheory.Submartingale`	`Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`sub_eq_add_neg` `add` `MeasureTheory.Submartingale.neg`

---

← Back to Index