OptionalSampling

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

Statistics

Metric	Count
Definitions	0
Theorems condExp_stoppedValue_stopping_time_ae_eq_restrict_le, condExp_stopping_time_ae_eq_restrict_eq_const, condExp_stopping_time_ae_eq_restrict_eq_const_of_le_const, stoppedValue_ae_eq_condExp_of_le, stoppedValue_ae_eq_condExp_of_le_const, stoppedValue_ae_eq_condExp_of_le_const_of_countable_range, stoppedValue_ae_eq_condExp_of_le_of_countable_range, stoppedValue_ae_eq_restrict_eq, stoppedValue_min_ae_eq_condExp	9
Total	9

MeasureTheory.Martingale

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
condExp_stoppedValue_stopping_time_ae_eq_restrict_le 📖	mathematical	MeasureTheory.Martingale PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MeasureTheory.IsStoppingTime WithTop Preorder.toLE WithTop.instPreorder WithTop.some	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.restrict setOf WithTop Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MeasureTheory.condExp MeasureTheory.IsStoppingTime.measurableSpace MeasureTheory.stoppedValue bot_nonempty OrderBot.toBot	—	MeasureTheory.IsStoppingTime.measurableSpace_le MeasureTheory.Measure.instOuterMeasureClass bot_nonempty ae_eq_restrict_iff_indicator_ae_eq MeasureTheory.IsStoppingTime.measurableSet_le_stopping_time TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace Countable.LindelofSpace Countable.of_linearOrder_locallyFiniteOrder TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace TopologicalSpace.DiscreteTopology.metrizableSpace OrderTopology.of_linearLocallyFinite Filter.EventuallyEq.trans Filter.EventuallyEq.symm MeasureTheory.condExp_indicator MeasureTheory.integrable_stoppedValue integrable MeasureTheory.IsStoppingTime.measurableSet_stopping_time_le MeasureTheory.Integrable.indicator MeasureTheory.StronglyMeasurable.aestronglyMeasurable MeasureTheory.StronglyMeasurable.stronglyMeasurable_of_measurableSpace_le_on Set.inter_comm MeasureTheory.IsStoppingTime.min MeasureTheory.IsStoppingTime.measurableSet_min_iff MeasureTheory.IsStoppingTime.measurableSet_inter_le_iff MeasureTheory.StronglyMeasurable.indicator Measurable.stronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace BorelSpace.opensMeasurable MeasureTheory.measurable_stoppedValue MeasureTheory.StronglyAdapted.progMeasurable_of_discrete stronglyAdapted Set.indicator_of_notMem MeasureTheory.condExp_of_aestronglyMeasurable'
condExp_stopping_time_ae_eq_restrict_eq_const 📖	mathematical	MeasureTheory.Martingale PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MeasureTheory.IsStoppingTime Preorder.toLE	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.restrict setOf WithTop WithTop.some MeasureTheory.condExp MeasureTheory.IsStoppingTime.measurableSpace PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	MeasureTheory.IsStoppingTime.measurableSpace_le Filter.EventuallyEq.trans MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.condExp_ae_eq_restrict_of_measurableSpace_eq_on MeasureTheory.Filtration.le MeasureTheory.sigmaFinite_of_sigmaFiniteFiltration MeasureTheory.IsStoppingTime.measurableSet_eq' Set.inter_comm MeasureTheory.IsStoppingTime.measurableSet_inter_eq_iff MeasureTheory.ae_restrict_of_ae condExp_ae_eq
condExp_stopping_time_ae_eq_restrict_eq_const_of_le_const 📖	mathematical	MeasureTheory.Martingale PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MeasureTheory.IsStoppingTime WithTop Preorder.toLE WithTop.instPreorder WithTop.some	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.restrict setOf WithTop WithTop.some MeasureTheory.condExp MeasureTheory.IsStoppingTime.measurableSpace PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	MeasureTheory.IsStoppingTime.measurableSpace_le_of_le MeasureTheory.Measure.instOuterMeasureClass Filter.EventuallyEq.trans MeasureTheory.condExp_ae_eq_restrict_of_measurableSpace_eq_on MeasureTheory.Filtration.le MeasureTheory.sigmaFinite_of_sigmaFiniteFiltration MeasureTheory.IsStoppingTime.measurableSet_eq' Set.inter_comm MeasureTheory.IsStoppingTime.measurableSet_inter_eq_iff MeasureTheory.ae_restrict_of_ae condExp_ae_eq Set.ext Mathlib.Tactic.Contrapose.contrapose₄ MeasureTheory.ae.congr_simp MeasureTheory.Measure.restrict_empty MeasureTheory.ae_zero
stoppedValue_ae_eq_condExp_of_le 📖	mathematical	MeasureTheory.Martingale PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MeasureTheory.IsStoppingTime Pi.hasLe WithTop Preorder.toLE WithTop.instPreorder WithTop.some	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.stoppedValue MeasureTheory.condExp MeasureTheory.IsStoppingTime.measurableSpace PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	MeasureTheory.IsStoppingTime.measurableSpace_le stoppedValue_ae_eq_condExp_of_le_of_countable_range TopologicalSpace.SecondCountableTopology.to_firstCountableTopology instSecondCountableTopologyOfOrderTopologyOfCountable Set.to_countable SetCoe.countable WithTop.instCountable
stoppedValue_ae_eq_condExp_of_le_const 📖	mathematical	MeasureTheory.Martingale PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MeasureTheory.IsStoppingTime WithTop Preorder.toLE WithTop.instPreorder WithTop.some	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.stoppedValue MeasureTheory.condExp MeasureTheory.IsStoppingTime.measurableSpace PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	MeasureTheory.IsStoppingTime.measurableSpace_le_of_le stoppedValue_ae_eq_condExp_of_le_const_of_countable_range TopologicalSpace.SecondCountableTopology.to_firstCountableTopology instSecondCountableTopologyOfOrderTopologyOfCountable Set.to_countable SetCoe.countable WithTop.instCountable
stoppedValue_ae_eq_condExp_of_le_const_of_countable_range 📖	mathematical	MeasureTheory.Martingale PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MeasureTheory.IsStoppingTime WithTop Preorder.toLE WithTop.instPreorder WithTop.some	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.stoppedValue MeasureTheory.condExp MeasureTheory.IsStoppingTime.measurableSpace PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	MeasureTheory.IsStoppingTime.measurableSpace_le_of_le Set.ext Set.iUnion_congr_Prop Set.iUnion_exists Set.iUnion_iUnion_eq' MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.restrict_univ MeasureTheory.ae_eq_restrict_biUnion_iff CanLift.prf WithTop.canLift MeasureTheory.ae.congr_simp stoppedValue_ae_eq_restrict_eq
stoppedValue_ae_eq_condExp_of_le_of_countable_range 📖	mathematical	MeasureTheory.Martingale PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MeasureTheory.IsStoppingTime Pi.hasLe WithTop Preorder.toLE WithTop.instPreorder WithTop.some	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.stoppedValue MeasureTheory.condExp MeasureTheory.IsStoppingTime.measurableSpace PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	MeasureTheory.IsStoppingTime.measurableSpace_le_of_le LE.le.trans MeasureTheory.sigmaFiniteTrim_mono MeasureTheory.IsStoppingTime.measurableSpace_mono MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.condExp_congr_ae stoppedValue_ae_eq_condExp_of_le_const_of_countable_range Filter.EventuallyEq.trans Filter.EventuallyEq.symm MeasureTheory.condExp_condExp_of_le
stoppedValue_ae_eq_restrict_eq 📖	mathematical	MeasureTheory.Martingale PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MeasureTheory.IsStoppingTime WithTop Preorder.toLE WithTop.instPreorder WithTop.some	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.restrict setOf WithTop WithTop.some MeasureTheory.stoppedValue MeasureTheory.condExp MeasureTheory.IsStoppingTime.measurableSpace PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	MeasureTheory.IsStoppingTime.measurableSpace_le_of_le Filter.EventuallyEq.trans MeasureTheory.Measure.instOuterMeasureClass Filter.EventuallyEq.eq_1 MeasureTheory.ae_restrict_iff' MeasureTheory.Filtration.le MeasureTheory.IsStoppingTime.measurableSet_eq Filter.Eventually.of_forall WithTop.untopA.congr_simp Set.mem_setOf_eq Filter.EventuallyEq.symm condExp_stopping_time_ae_eq_restrict_eq_const_of_le_const
stoppedValue_min_ae_eq_condExp 📖	mathematical	MeasureTheory.Martingale PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MeasureTheory.IsStoppingTime WithTop Preorder.toLE WithTop.instPreorder WithTop.some	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.stoppedValue bot_nonempty OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder WithTop SemilatticeInf.toMin WithTop.semilatticeInf MeasureTheory.condExp MeasureTheory.IsStoppingTime.measurableSpace	—	MeasureTheory.IsStoppingTime.min MeasureTheory.IsStoppingTime.measurableSpace_le Filter.EventuallyEq.trans MeasureTheory.Measure.instOuterMeasureClass bot_nonempty stoppedValue_ae_eq_condExp_of_le OrderTopology.of_linearLocallyFinite Countable.of_linearOrder_locallyFiniteOrder min_le_right MeasureTheory.IsStoppingTime.sigmaFinite_stopping_time MeasureTheory.ae_of_ae_restrict_of_ae_restrict_compl MeasureTheory.condExp_min_stopping_time_ae_eq_restrict_le TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace Countable.LindelofSpace TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace TopologicalSpace.DiscreteTopology.metrizableSpace MeasureTheory.IsStoppingTime.measurableSpace_min inf_comm Filter.EventuallyEq.refl MeasureTheory.condExp_of_stronglyMeasurable Measurable.stronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace BorelSpace.opensMeasurable MeasureTheory.measurable_stoppedValue MeasureTheory.StronglyAdapted.progMeasurable_of_discrete stronglyAdapted MeasureTheory.integrable_stoppedValue integrable Filter.EventuallyEq.symm condExp_stoppedValue_stopping_time_ae_eq_restrict_le MeasureTheory.ae_restrict_iff' MeasurableSet.compl MeasureTheory.IsStoppingTime.measurableSet_le_stopping_time Filter.mp_mem Filter.EventuallyEq.eq_1 Filter.univ_mem' LT.lt.le

---

← Back to Index