Filtration

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

Statistics

Metric	Count
Definitions IsRightContinuous, const, cylinderEventsCompl, instBot, instCompleteLattice, instInfSet, instInhabited, instLE, instMax, instMin, instPartialOrder, instSupSet, instTop, limitProcess, natural, piFinset, piLE, rightCont, seq, «term_₊», SigmaFiniteFiltration, filtrationOfSet, instCoeFunFiltrationForallMeasurableSpace	23
Theorems RC, eq, measurableSet, coeFn_inf, coeFn_sup, condExp_condExp, const_apply, ext, ext_iff, filtrationOfSet_eq_natural, instIsRightContinuousRightCont, le, le', le_rightCont, memLp_limitProcess_of_eLpNorm_bdd, mono, mono', piFinset_eq_comap_restrict, piLE_eq_comap_frestrictLe, rightCont_apply, rightCont_def, rightCont_eq, rightCont_eq_of_exists_gt, rightCont_eq_of_isMax, rightCont_eq_of_neBot_nhdsGT, rightCont_eq_of_nhdsGT_eq_bot, rightCont_eq_of_not_isMax, rightCont_eq_self, rightCont_self, sInf_def, sSup_def, stronglyMeasurable_limitProcess, stronglyMeasurable_limit_process', uniformIntegrable_condExp_filtration, sigmaFiniteFiltration, SigmaFinite, measurableSet_filtrationOfSet, measurableSet_filtrationOfSet', measurableSet_of_filtration, sigmaFinite_of_sigmaFiniteFiltration	40
Total	63

MeasureTheory

Definitions

Name	Category	Theorems
SigmaFiniteFiltration 📖	CompData	1 math math: IsFiniteMeasure.sigmaFiniteFiltration
filtrationOfSet 📖	CompOp	4 math math: ProbabilityTheory.iIndepSet.condExp_indicator_filtrationOfSet_ae_eq, Filtration.filtrationOfSet_eq_natural, measurableSet_filtrationOfSet, measurableSet_filtrationOfSet'
instCoeFunFiltrationForallMeasurableSpace 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurableSet_filtrationOfSet 📖	mathematical	MeasurableSet Preorder.toLE	MeasurableSet Filtration.seq filtrationOfSet	—	MeasurableSpace.measurableSet_generateFrom
measurableSet_filtrationOfSet' 📖	mathematical	MeasurableSet	MeasurableSet Filtration.seq filtrationOfSet	—	measurableSet_filtrationOfSet le_rfl
measurableSet_of_filtration 📖	mathematical	MeasurableSet Filtration.seq	MeasurableSet	—	Filtration.le
sigmaFinite_of_sigmaFiniteFiltration 📖	mathematical	—	SigmaFinite Filtration.seq Measure.trim Filtration.le	—	SigmaFiniteFiltration.SigmaFinite

MeasureTheory.Filtration

Definitions

Name	Category	Theorems
IsRightContinuous 📖	CompData	1 math math: instIsRightContinuousRightCont
const 📖	CompOp	1 math math: const_apply
cylinderEventsCompl 📖	CompOp	—
instBot 📖	CompOp	—
instCompleteLattice 📖	CompOp	—
instInfSet 📖	CompOp	1 math math: sInf_def
instInhabited 📖	CompOp	—
instLE 📖	CompOp	2 math math: le_rightCont, IsRightContinuous.RC
instMax 📖	CompOp	1 math math: coeFn_sup
instMin 📖	CompOp	1 math math: coeFn_inf
instPartialOrder 📖	CompOp	—
instSupSet 📖	CompOp	1 math math: sSup_def
instTop 📖	CompOp	—
limitProcess 📖	CompOp	13 math math: ProbabilityTheory.Kernel.memL1_limitProcess_densityProcess, MeasureTheory.Submartingale.ae_tendsto_limitProcess_of_uniformIntegrable, ProbabilityTheory.Kernel.density_ae_eq_limitProcess, ProbabilityTheory.Kernel.tendsto_eLpNorm_one_densityProcess_limitProcess, stronglyMeasurable_limit_process', memLp_limitProcess_of_eLpNorm_bdd, MeasureTheory.Submartingale.tendsto_eLpNorm_one_limitProcess, ProbabilityTheory.Kernel.tendsto_densityProcess_limitProcess, MeasureTheory.Submartingale.ae_tendsto_limitProcess, MeasureTheory.Martingale.ae_eq_condExp_limitProcess, ProbabilityTheory.Kernel.tendsto_eLpNorm_one_restrict_densityProcess_limitProcess, MeasureTheory.Submartingale.memLp_limitProcess, stronglyMeasurable_limitProcess
natural 📖	CompOp	4 math math: ProbabilityTheory.iIndepFun.indep_comap_natural_of_lt, stronglyAdapted_natural, filtrationOfSet_eq_natural, ProbabilityTheory.iIndepFun.condExp_natural_ae_eq_of_lt
piFinset 📖	CompOp	1 math math: piFinset_eq_comap_restrict
piLE 📖	CompOp	3 math math: ProbabilityTheory.Kernel.condExp_traj', ProbabilityTheory.Kernel.condExp_traj, piLE_eq_comap_frestrictLe
rightCont 📖	CompOp	14 math math: rightCont_eq_of_nhdsGT_eq_bot, rightCont_eq_self, rightCont_eq_of_isMax, rightCont_apply, rightCont_def, rightCont_self, rightCont_eq_of_not_isMax, IsRightContinuous.eq, rightCont_eq, le_rightCont, IsRightContinuous.RC, rightCont_eq_of_neBot_nhdsGT, instIsRightContinuousRightCont, rightCont_eq_of_exists_gt
seq 📖	CompOp	102 math math: MeasureTheory.IsPredictable.measurable_add_one, MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable_range, ProbabilityTheory.Kernel.condExp_traj', MeasureTheory.IsStoppingTime.measurableSet, MeasureTheory.IsStoppingTime.measurableSet_gt, MeasureTheory.martingale_condExp, rightCont_eq_of_nhdsGT_eq_bot, ext_iff, MeasureTheory.BorelCantelli.martingalePart_process_ae_eq, ProbabilityTheory.Kernel.measurable_densityProcess_countableFiltration_aux, MeasureTheory.IsStoppingTime.measurableSet_ge_of_countable, MeasureTheory.IsStoppingTime.measurableSet_lt_of_isLUB, MeasureTheory.condExp_stopping_time_ae_eq_restrict_eq, condExp_condExp, MeasureTheory.sigmaFinite_of_sigmaFiniteFiltration, MeasureTheory.IsStoppingTime.measurableSpace_le_of_le_const, MeasureTheory.Integrable.tendsto_eLpNorm_condExp, MeasureTheory.BorelCantelli.predictablePart_process_ae_eq, ProbabilityTheory.iIndepSet.condExp_indicator_filtrationOfSet_ae_eq, rightCont_eq_of_isMax, MeasureTheory.Integrable.tendsto_ae_condExp, ProbabilityTheory.iIndepFun.indep_comap_natural_of_lt, MeasureTheory.IsStoppingTime.measurableSet_lt, ProbabilityTheory.measurableSet_partitionFiltration_of_mem, MeasureTheory.IsStoppingTime.measurableSet_lt_of_pred, MeasureTheory.IsStoppingTime.measurableSet_eq_le, MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable, MeasureTheory.IsStoppingTime.measurableSet_le, ProbabilityTheory.measurable_countablePartitionSet_subtype, const_apply, rightCont_apply, ProbabilityTheory.Kernel.measurable_countableFiltration_densityProcess, MeasureTheory.IsStoppingTime.measurableSet_ge, MeasureTheory.Submartingale.stronglyMeasurable, ProbabilityTheory.Kernel.condExp_traj, rightCont_def, MeasureTheory.IsStoppingTime.measurableSet_lt_of_countable, MeasureTheory.tendsto_sum_indicator_atTop_iff', MeasureTheory.IsStoppingTime.measurableSet_eq, MeasureTheory.measurableSet_preimage_stoppedValue_inter, MeasureTheory.measurableSet_filtrationOfSet, MeasureTheory.Adapted.measurable_le, le', rightCont_eq_of_not_isMax, MeasureTheory.tendsto_ae_condExp, ProbabilityTheory.measurableSet_partitionFiltration_memPartitionSet, ProbabilityTheory.iSup_partitionFiltration_eq_generateFrom_range, MeasureTheory.SigmaFiniteFiltration.SigmaFinite, ProbabilityTheory.measurableSet_countableFiltration_countablePartitionSet, MeasureTheory.IsStoppingTime.measurableSet_lt_le, MeasureTheory.condExp_stopping_time_ae_eq_restrict_eq_of_countable, MeasureTheory.Supermartingale.stronglyMeasurable, MeasureTheory.condExp_stopping_time_ae_eq_restrict_eq_of_countable_range, MeasureTheory.Supermartingale.condExp_ae_le, MeasureTheory.IsStoppingTime.measurableSpace_min_const, piFinset_eq_comap_restrict, MeasureTheory.tendsto_eLpNorm_condExp, ProbabilityTheory.iSup_countableFiltration, ProbabilityTheory.Kernel.stronglyMeasurable_countableFiltration_densityProcess, rightCont_eq, MeasureTheory.IsStoppingTime.measurableSet_lt_of_countable_range, IsRightContinuous.measurableSet, ProbabilityTheory.Kernel.condExp_densityProcess, coeFn_sup, MeasureTheory.Martingale.condExp_ae_eq, MeasureTheory.StronglyAdapted.stronglyMeasurable_le, MeasureTheory.ae_mem_limsup_atTop_iff, MeasureTheory.measurableSet_filtrationOfSet', MeasureTheory.martingalePart_eq_sum, MeasureTheory.IsPredictable.measurableSet_prodMk_add_one_of_predictable, mono, MeasureTheory.isPredictable_iff_measurable_add_one, sSup_def, ProbabilityTheory.iIndepFun.condExp_natural_ae_eq_of_lt, le, piLE_eq_comap_frestrictLe, ProbabilityTheory.measurableSet_countableFiltration_of_mem, MeasureTheory.submartingale_iff_condExp_sub_nonneg, MeasureTheory.Integrable.uniformIntegrable_condExp_filtration, ProbabilityTheory.measurable_memPartitionSet_subtype, ProbabilityTheory.iSup_partitionFiltration, MeasureTheory.Martingale.ae_eq_condExp_limitProcess, MeasureTheory.IsStoppingTime.measurableSet_ge_of_countable_range, MeasureTheory.Martingale.eq_condExp_of_tendsto_eLpNorm, MeasureTheory.IsStoppingTime.measurableSet_min_const_iff, ProbabilityTheory.measurable_partitionFiltration_memPartitionSet, MeasureTheory.Submartingale.exists_ae_trim_tendsto_of_bdd, rightCont_eq_of_neBot_nhdsGT, MeasureTheory.IsStoppingTime.measurableSpace_const, coeFn_inf, MeasureTheory.IsStoppingTime.measurable_of_le, MeasureTheory.Martingale.stronglyMeasurable, mono', MeasureTheory.IsStoppingTime.le_measurableSpace_of_const_le, ProbabilityTheory.measurable_countableFiltration_countablePartitionSet, MeasureTheory.Submartingale.ae_le_condExp, MeasureTheory.stronglyMeasurable_stoppedValue_of_le, MeasureTheory.Submartingale.condExp_sub_nonneg, rightCont_eq_of_exists_gt, MeasureTheory.IsStoppingTime.measurableSet_inter_eq_iff, stronglyMeasurable_limitProcess, sInf_def
«term_₊» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeFn_inf 📖	mathematical	—	seq MeasureTheory.Filtration instMin Pi.instMinForall_mathlib MeasurableSpace SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice MeasurableSpace.instCompleteLattice	—	—
coeFn_sup 📖	mathematical	—	seq MeasureTheory.Filtration instMax Pi.instMaxForall_mathlib MeasurableSpace SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice MeasurableSpace.instCompleteLattice	—	—
condExp_condExp 📖	mathematical	Preorder.toLE	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.condExp seq	—	le MeasureTheory.condExp_condExp_of_le mono
const_apply 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	seq const	—	—
ext 📖	—	seq	—	—	—
ext_iff 📖	mathematical	—	seq	—	ext
filtrationOfSet_eq_natural 📖	mathematical	TopologicalSpace.MetrizableSpace BorelSpace Nontrivial MeasurableSet	MeasureTheory.filtrationOfSet natural Set.indicator MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass MeasureTheory.StronglyMeasurable.indicator Pi.instOne MeasureTheory.stronglyMeasurable_one	—	MeasureTheory.StronglyMeasurable.indicator MeasureTheory.stronglyMeasurable_one iSup_congr_Prop MeasurableSpace.measurableSpace_iSup_eq le_antisymm MeasurableSpace.generateFrom_le MeasurableSpace.measurableSet_generateFrom MeasurableSpace.comap_eq_generateFrom MeasurableSingletonClass.measurableSet_singleton OpensMeasurableSpace.toMeasurableSingletonClass BorelSpace.opensMeasurable T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace Set.ext NeZero.one Set.indicator_const_preimage MeasurableSet.univ MeasurableSet.compl Set.mem_singleton_iff MeasurableSpace.measurableSet_empty
instIsRightContinuousRightCont 📖	mathematical	—	IsRightContinuous rightCont	—	Eq.le rightCont_self
le 📖	mathematical	—	MeasurableSpace MeasurableSpace.instLE seq	—	le'
le' 📖	mathematical	—	MeasurableSpace MeasurableSpace.instLE seq	—	—
le_rightCont 📖	mathematical	—	MeasureTheory.Filtration PartialOrder.toPreorder instLE rightCont	—	rightCont_eq_of_neBot_nhdsGT le_iInf₂ mono LT.lt.le rightCont_apply le_refl
memLp_limitProcess_of_eLpNorm_bdd 📖	mathematical	MeasureTheory.AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder MeasureTheory.eLpNorm ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddGroup.toContinuousENorm ENNReal.ofNNReal	MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace limitProcess Nat.instPreorder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	MeasureTheory.Measure.instOuterMeasureClass limitProcess.eq_1 MeasureTheory.StronglyMeasurable.aestronglyMeasurable MeasureTheory.StronglyMeasurable.mono sSup_le le lt_of_le_of_lt MeasureTheory.Lp.eLpNorm_lim_le_liminf_eLpNorm instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat LE.le.trans le_rfl ENNReal.coe_lt_top MeasureTheory.MemLp.zero
mono 📖	mathematical	Preorder.toLE	MeasurableSpace MeasurableSpace.instLE seq	—	mono'
mono' 📖	mathematical	—	Monotone MeasurableSpace PartialOrder.toPreorder MeasurableSpace.instPartialOrder seq	—	—
piFinset_eq_comap_restrict 📖	mathematical	—	seq Finset PartialOrder.toPreorder Finset.partialOrder MeasurableSpace.pi piFinset MeasurableSpace.comap Set.restrict SetLike.coe Finset.instSetLike Set.Elem Set Set.instMembership	—	—
piLE_eq_comap_frestrictLe 📖	mathematical	—	seq MeasurableSpace.pi piLE MeasurableSpace.comap Preorder.frestrictLe Finset SetLike.instMembership Finset.instSetLike Finset.Iic	—	le_antisymm MeasurableSpace.comap_mono Measurable.comap_le MeasurableEquiv.measurable Preorder.piCongrLeft_comp_restrictLe MeasurableEquiv.coe_piCongrLeft MeasurableSpace.comap_comp
rightCont_apply 📖	mathematical	—	seq PartialOrder.toPreorder rightCont MeasurableSpace Filter.NeBot nhdsWithin Set.Ioi iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice MeasurableSpace.instCompleteLattice Preorder.toLT	—	rightCont_def OrderTopology.topology_eq_generate_intervals
rightCont_def 📖	mathematical	—	rightCont PartialOrder.toPreorder MeasurableSpace Filter.NeBot nhdsWithin Preorder.topology Set.Ioi iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice MeasurableSpace.instCompleteLattice Preorder.toLT seq	—	—
rightCont_eq 📖	mathematical	—	seq PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder rightCont iInf MeasurableSpace ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice MeasurableSpace.instCompleteLattice Preorder.toLT	—	rightCont_eq_of_not_isMax not_isMax
rightCont_eq_of_exists_gt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Ioo Set Set.instEmptyCollection	seq PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder rightCont	—	covBy_iff_Ioo_eq rightCont_eq_of_nhdsGT_eq_bot CovBy.nhdsGT instClosedIciTopology OrderTopology.to_orderClosedTopology
rightCont_eq_of_isMax 📖	mathematical	IsMax Preorder.toLE PartialOrder.toPreorder	seq PartialOrder.toPreorder rightCont	—	rightCont_eq_of_nhdsGT_eq_bot nhdsWithin_empty IsMax.Ioi_eq
rightCont_eq_of_neBot_nhdsGT 📖	mathematical	—	seq PartialOrder.toPreorder rightCont iInf MeasurableSpace ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice MeasurableSpace.instCompleteLattice Preorder.toLT	—	rightCont_apply
rightCont_eq_of_nhdsGT_eq_bot 📖	mathematical	nhdsWithin Set.Ioi PartialOrder.toPreorder Bot.bot Filter Filter.instBot	seq PartialOrder.toPreorder rightCont	—	rightCont_apply Filter.neBot_iff
rightCont_eq_of_not_isMax 📖	mathematical	IsMax Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	seq PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder rightCont iInf MeasurableSpace ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice MeasurableSpace.instCompleteLattice Preorder.toLT	—	nhdsGT_neBot_of_exists_gt not_isMax_iff rightCont_eq_of_neBot_nhdsGT
rightCont_eq_self 📖	mathematical	—	rightCont SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	ext MeasurableSpace.ext rightCont_eq_of_nhdsGT_eq_bot SuccOrder.nhdsGT instClosedIciTopology OrderTopology.to_orderClosedTopology
rightCont_self 📖	mathematical	—	rightCont	—	le_antisymm le_iInf₂ mem_nhdsWithin_iff_exists_mem_nhds_inter IsOpen.mem_nhds isOpen_Iio' Filter.NeBot.nonempty_of_mem iInf₂_le_of_le le_rfl rightCont_eq_of_neBot_nhdsGT iInf_congr_Prop rightCont_apply mono LT.lt.le LE.le.trans le_refl le_rightCont
sInf_def 📖	mathematical	—	seq InfSet.sInf MeasureTheory.Filtration instInfSet MeasurableSpace Set.Nonempty ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice MeasurableSpace.instCompleteLattice Set.image	—	—
sSup_def 📖	mathematical	—	seq SupSet.sSup MeasureTheory.Filtration instSupSet MeasurableSpace ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice MeasurableSpace.instCompleteLattice Set.image	—	—
stronglyMeasurable_limitProcess 📖	mathematical	—	MeasureTheory.StronglyMeasurable iSup MeasurableSpace ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice MeasurableSpace.instCompleteLattice seq limitProcess	—	MeasureTheory.Measure.instOuterMeasureClass limitProcess.eq_1 MeasureTheory.stronglyMeasurable_zero
stronglyMeasurable_limit_process' 📖	mathematical	—	MeasureTheory.StronglyMeasurable limitProcess	—	MeasureTheory.StronglyMeasurable.mono stronglyMeasurable_limitProcess sSup_le le

MeasureTheory.Filtration.IsRightContinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
RC 📖	mathematical	—	MeasureTheory.Filtration PartialOrder.toPreorder MeasureTheory.Filtration.instLE MeasureTheory.Filtration.rightCont	—	—
eq 📖	mathematical	—	MeasureTheory.Filtration.rightCont	—	le_antisymm MeasureTheory.Filtration.le_rightCont RC
measurableSet 📖	mathematical	MeasurableSet MeasureTheory.Filtration.seq PartialOrder.toPreorder MeasureTheory.Filtration.rightCont	MeasurableSet MeasureTheory.Filtration.seq PartialOrder.toPreorder	—	eq

MeasureTheory.Integrable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
uniformIntegrable_condExp_filtration 📖	mathematical	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing	MeasureTheory.UniformIntegrable Real Real.normedAddCommGroup MeasureTheory.condExp MeasureTheory.Filtration.seq Real.instCompleteSpace InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	uniformIntegrable_condExp MeasureTheory.Filtration.le

MeasureTheory.IsFiniteMeasure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sigmaFiniteFiltration 📖	mathematical	—	MeasureTheory.SigmaFiniteFiltration	—	MeasureTheory.Filtration.le toSigmaFinite MeasureTheory.isFiniteMeasure_trim

MeasureTheory.SigmaFiniteFiltration

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
SigmaFinite 📖	mathematical	—	MeasureTheory.SigmaFinite MeasureTheory.Filtration.seq MeasureTheory.Measure.trim MeasureTheory.Filtration.le	—	—

---

← Back to Index