Documentation Verification Report

Centering

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

Statistics

Metric	Count
Definitions `martingalePart`, `predictablePart`	2
Theorems `integrable_martingalePart`, `martingalePart_add_ae_eq`, `martingalePart_add_predictablePart`, `martingalePart_bdd_difference`, `martingalePart_eq_sum`, `martingale_martingalePart`, `predictablePart_add_ae_eq`, `predictablePart_bdd_difference`, `predictablePart_zero`, `stronglyAdapted_martingalePart`, `stronglyAdapted_predictablePart`, `stronglyAdapted_predictablePart'`	12
Total	14

MeasureTheory

Definitions

Name	Category	Theorems
`martingalePart` 📖	CompOp	7 math math: `BorelCantelli.martingalePart_process_ae_eq`, `integrable_martingalePart`, `stronglyAdapted_martingalePart`, `martingalePart_add_predictablePart`, `martingale_martingalePart`, `martingalePart_add_ae_eq`, `martingalePart_eq_sum`
`predictablePart` 📖	CompOp	7 math math: `predictablePart_add_ae_eq`, `BorelCantelli.predictablePart_process_ae_eq`, `tendsto_sum_indicator_atTop_iff`, `stronglyAdapted_predictablePart'`, `martingalePart_add_predictablePart`, `stronglyAdapted_predictablePart`, `predictablePart_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`integrable_martingalePart` 📖	mathematical	`Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`martingalePart`	—	`martingalePart_eq_sum` `Integrable.add` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `integrable_finset_sum'` `Integrable.sub` `integrable_condExp`
`martingalePart_add_ae_eq` 📖	mathematical	`Martingale` `Nat.instPreorder` `StronglyAdapted` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Pi.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Integrable` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`Filter.EventuallyEq` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `martingalePart` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`sub_eq_sub_iff_add_eq_add` `add_comm` `martingalePart_add_predictablePart` `StronglyAdapted.sub` `IsTopologicalAddGroup.to_continuousSub` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `stronglyAdapted_predictablePart` `Martingale.sub` `martingale_martingalePart` `StronglyAdapted.add` `IsTopologicalAddGroup.toContinuousAdd` `Martingale.stronglyAdapted` `Predictable.stronglyAdapted` `stronglyMeasurable_zero` `Integrable.add` `Martingale.integrable` `Filter.EventuallyEq.symm` `Measure.instOuterMeasureClass` `Filter.eventuallyEq_iff_sub` `Filter.mp_mem` `Martingale.eq_zero_of_predictable` `Filter.univ_mem'` `Pi.sub_apply` `martingalePart.eq_1` `add_zero` `predictablePart_zero` `sub_zero` `sub_self`
`martingalePart_add_predictablePart` 📖	mathematical	—	`Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `martingalePart` `predictablePart`	—	`sub_add_cancel`
`martingalePart_bdd_difference` 📖	—	`Filter.Eventually` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass`	—	—	`Measure.instOuterMeasureClass` `Filter.mp_mem` `Real.instCompleteSpace` `Nat.instAtLeastTwoHAddOfNat` `predictablePart_bdd_difference` `Filter.univ_mem'` `two_mul` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf'` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `mul_one` `add_zero` `predictablePart.congr_simp` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.RingNF.int_rawCast_neg` `Mathlib.Tactic.RingNF.mul_neg` `Mathlib.Tactic.RingNF.add_assoc_rev` `Mathlib.Tactic.RingNF.add_neg` `LE.le.trans` `abs_sub` `Real.instIsOrderedAddMonoid` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add`
`martingalePart_eq_sum` 📖	mathematical	—	`martingalePart` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Finset.sum` `Pi.addCommMonoid` `Finset.range` `Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `condExp` `Filtration.seq` `Nat.instPreorder`	—	`Finset.eq_sum_range_sub` `add_sub` `Finset.sum_sub_distrib`
`martingale_martingalePart` 📖	mathematical	`StronglyAdapted` `Nat.instPreorder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Integrable` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`Martingale` `martingalePart`	—	`Measure.instOuterMeasureClass` `stronglyAdapted_martingalePart` `martingalePart_eq_sum` `Filter.EventuallyEq.trans` `condExp_add` `integrable_finset_sum'` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Integrable.sub` `integrable_condExp` `Filter.EventuallyEq.add` `Filter.EventuallyEq.rfl` `condExp_finset_sum` `condExp_of_stronglyMeasurable` `Filtration.le` `sigmaFinite_of_sigmaFiniteFiltration` `StronglyMeasurable.mono` `Filtration.mono` `zero_le` `Nat.instCanonicallyOrderedAdd` `Filter.EventuallyEq.refl` `eventuallyEq_sum` `condExp_sub` `condExp_condExp_of_le` `Filter.mp_mem` `Filter.univ_mem'` `Pi.sub_apply` `Pi.zero_apply` `sub_self` `Filter.EventuallyEq.sub` `StronglyMeasurable.sub` `IsTopologicalAddGroup.to_continuousSub` `LT.lt.le` `stronglyMeasurable_condExp` `Finset.sum_range_add_sum_Ico` `add_zero` `Finset.mem_range` `Finset.mem_Ico` `Finset.sum_const_zero`
`predictablePart_add_ae_eq` 📖	mathematical	`Martingale` `Nat.instPreorder` `StronglyAdapted` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Pi.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Integrable` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`Filter.EventuallyEq` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `predictablePart` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`Filter.mp_mem` `Measure.instOuterMeasureClass` `martingalePart_add_ae_eq` `Filter.univ_mem'` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Pi.add_apply` `martingalePart_add_predictablePart`
`predictablePart_bdd_difference` 📖	—	`Filter.Eventually` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass`	—	—	`Measure.instOuterMeasureClass` `Real.instCompleteSpace` `Finset.sum_apply` `Finset.sum_range_succ_sub_sum` `ae_all_iff` `instCountableNat` `ae_bdd_condExp_of_ae_bdd`
`predictablePart_zero` 📖	mathematical	—	`predictablePart` `Pi.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	—
`stronglyAdapted_martingalePart` 📖	mathematical	`StronglyAdapted` `Nat.instPreorder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`martingalePart`	—	`StronglyAdapted.sub` `IsTopologicalAddGroup.to_continuousSub` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `stronglyAdapted_predictablePart'`
`stronglyAdapted_predictablePart` 📖	mathematical	—	`StronglyAdapted` `Nat.instPreorder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `predictablePart`	—	`Finset.stronglyMeasurable_sum` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `StronglyMeasurable.mono` `stronglyMeasurable_condExp` `Filtration.mono` `Finset.mem_range_succ_iff`
`stronglyAdapted_predictablePart'` 📖	mathematical	—	`StronglyAdapted` `Nat.instPreorder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `predictablePart`	—	`Finset.stronglyMeasurable_sum` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `StronglyMeasurable.mono` `stronglyMeasurable_condExp` `Filtration.mono` `Finset.mem_range_le`

---

← Back to Index