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 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	—	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 MeasureTheory.condExp MeasureTheory.IsStoppingTime.measurableSpace	—	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	—	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	—	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	—	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	—	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 MeasureTheory.stoppedValue MeasureTheory.condExp MeasureTheory.IsStoppingTime.measurableSpace	—	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 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