Documentation Verification Report

Predictable

📁 Source: Mathlib/Probability/Process/Predictable.lean

Statistics

Metric	Count
Definitions `predictable`, `IsPredictable`	2
Theorems `adapted`, `measurableSet_prodMk_add_one_of_predictable`, `measurable_add_one`, `progMeasurable`, `isPredictable_iff_measurable_add_one`, `isPredictable_of_measurable_add_one`, `measurableSet_predictable_Ioc_prod`, `measurableSet_predictable_Ioi_prod`, `measurableSet_predictable_singleton_bot_prod`, `measurableSet_predictable_singleton_prod`, `measurableSpace_le_predictable_of_measurableSet`	11
Total	13

MeasureTheory

Definitions

Name	Category	Theorems
`IsPredictable` 📖	MathDef	2 math math: `isPredictable_of_measurable_add_one`, `isPredictable_iff_measurable_add_one`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPredictable_iff_measurable_add_one` 📖	mathematical	—	`IsPredictable` `Nat.instPreorder` `Nat.instOrderBot` `Measurable` `Filtration.seq`	—	`StronglyMeasurable.measurable` `TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace` `IsPredictable.adapted` `BorelSpace.opensMeasurable` `Nat.borelSpace` `OrderTopology.to_orderClosedTopology` `OrderTopology.of_linearLocallyFinite` `instDiscreteTopologyNat` `IsPredictable.measurable_add_one` `isPredictable_of_measurable_add_one`
`isPredictable_of_measurable_add_one` 📖	mathematical	`Measurable` `Filtration.seq` `Nat.instPreorder`	`IsPredictable` `Nat.instOrderBot`	—	`Measurable.stronglyMeasurable` `TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace` `BorelSpace.opensMeasurable` `Set.ext` `MeasurableSet.iUnion` `instCountableNat` `MeasurableSpace.measurableSet_generateFrom` `measurableSet_predictable_singleton_prod`
`measurableSet_predictable_Ioc_prod` 📖	mathematical	`MeasurableSet` `Filtration.seq` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Filtration.predictable` `SProd.sprod` `Set` `Set.instSProd` `Set.Ioc`	—	`le_total` `Set.Ioc_eq_empty` `Set.empty_prod` `Set.Ioi_diff_Ioi` `sdiff_self` `Set.prod_empty` `Set.empty_union` `Set.prod_diff_prod` `MeasurableSet.diff` `measurableSet_predictable_Ioi_prod` `Filtration.mono`
`measurableSet_predictable_Ioi_prod` 📖	mathematical	`MeasurableSet` `Filtration.seq` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Filtration.predictable` `SProd.sprod` `Set` `Set.instSProd` `Set.Ioi`	—	`MeasurableSpace.measurableSet_generateFrom`
`measurableSet_predictable_singleton_bot_prod` 📖	mathematical	`MeasurableSet` `Filtration.seq` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Bot.bot` `OrderBot.toBot` `Preorder.toLE`	`Filtration.predictable` `SProd.sprod` `Set` `Set.instSProd` `Set.instSingletonSet`	—	`MeasurableSpace.measurableSet_generateFrom`
`measurableSet_predictable_singleton_prod` 📖	mathematical	`MeasurableSet` `Filtration.seq` `Nat.instPreorder`	`Filtration.predictable` `Nat.instOrderBot` `SProd.sprod` `Set` `Set.instSProd` `Set.instSingletonSet`	—	`Set.ext` `measurableSet_predictable_Ioc_prod`
`measurableSpace_le_predictable_of_measurableSet` 📖	mathematical	`MeasurableSet` `SProd.sprod` `Set` `Set.instSProd` `Set.instSingletonSet` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `Set.Ioi`	`MeasurableSpace` `MeasurableSpace.instLE` `Filtration.predictable`	—	`MeasurableSpace.generateFrom_le`

MeasureTheory.Filtration

Definitions

Name	Category	Theorems
`predictable` 📖	CompOp	5 math math: `MeasureTheory.measurableSet_predictable_Ioi_prod`, `MeasureTheory.measurableSet_predictable_singleton_bot_prod`, `MeasureTheory.measurableSet_predictable_Ioc_prod`, `MeasureTheory.measurableSpace_le_predictable_of_measurableSet`, `MeasureTheory.measurableSet_predictable_singleton_prod`

MeasureTheory.IsPredictable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adapted` 📖	mathematical	`MeasureTheory.IsPredictable` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`MeasureTheory.StronglyAdapted`	—	`MeasureTheory.ProgMeasurable.stronglyAdapted` `progMeasurable`
`measurableSet_prodMk_add_one_of_predictable` 📖	mathematical	`MeasurableSet` `MeasureTheory.Filtration.predictable` `Nat.instPreorder` `Nat.instOrderBot`	`MeasureTheory.Filtration.seq` `setOf` `Set` `Set.instMembership`	—	`measurableSet_preimage` `measurable_prodMk_left` `measurable_iff_comap_le` `MeasurableSpace.comap_le_iff_le_map` `MeasurableSpace.generateFrom_le` `MeasurableSpace.map_def` `Set.ext` `lt_or_ge` `Order.lt_add_one_iff` `Nat.instNoMaxOrder` `MeasurableSet.prod` `MeasurableSet.of_subtype_image` `MeasureTheory.Filtration.mono`
`measurable_add_one` 📖	mathematical	`MeasureTheory.IsPredictable` `Nat.instPreorder` `Nat.instOrderBot`	`Measurable` `MeasureTheory.Filtration.seq`	—	`measurableSet_prodMk_add_one_of_predictable` `MeasureTheory.StronglyMeasurable.measurable` `TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace`
`progMeasurable` 📖	mathematical	`MeasureTheory.IsPredictable` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`MeasureTheory.ProgMeasurable`	—	`Measurable.stronglyMeasurable` `TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace` `BorelSpace.opensMeasurable` `measurable_iff_comap_le` `MeasurableSpace.comap_comp` `LE.le.trans` `MeasurableSpace.comap_mono` `stronglyMeasurable_iff_measurable` `eq_1` `MeasurableSpace.comap_le_iff_le_map` `MeasureTheory.measurableSpace_le_predictable_of_measurableSet` `Set.ext` `MeasurableSet.prod` `MeasurableSingletonClass.measurableSet_singleton` `Subtype.instMeasurableSingletonClass` `OpensMeasurableSpace.toMeasurableSingletonClass` `T2Space.t1Space` `OrderClosedTopology.to_t2Space` `MeasureTheory.Filtration.mono` `bot_le` `le_total` `measurable_subtype_coe` `measurableSet_Ioc` `instClosedIicTopology`

---

← Back to Index