Filtration

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

Statistics

Metric	Count
Definitions IsRightContinuous, const, cylinderEventsCompl, instBot, instCompleteLattice, instInfSet, instInhabited, instLE, instMax, instMin, instSupSet, instTop, limitProcess, natural, piFinset, piLE, rightCont, seq, «term_₊», SigmaFiniteFiltration, filtrationOfSet, instCoeFunFiltrationForallMeasurableSpace	22
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	62

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	Filtration.seq filtrationOfSet	—	MeasurableSpace.measurableSet_generateFrom
measurableSet_filtrationOfSet' 📖	mathematical	MeasurableSet	Filtration.seq filtrationOfSet	—	measurableSet_filtrationOfSet le_rfl
measurableSet_of_filtration 📖	—	MeasurableSet Filtration.seq	—	—	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
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	97 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.BorelCantelli.predictablePart_process_ae_eq, ProbabilityTheory.iIndepSet.condExp_indicator_filtrationOfSet_ae_eq, rightCont_eq_of_isMax, 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.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, ProbabilityTheory.Kernel.condExp_densityProcess, coeFn_sup, MeasureTheory.Martingale.condExp_ae_eq, MeasureTheory.StronglyAdapted.stronglyMeasurable_le, 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 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 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 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 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 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 📖	—	MeasurableSet MeasureTheory.Filtration.seq PartialOrder.toPreorder MeasureTheory.Filtration.rightCont	—	—	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.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