Documentation Verification Report

Adapted

πŸ“ Source: Mathlib/Probability/Process/Adapted.lean

Statistics

MetricCount
DefinitionsAdapted, ProgMeasurable, StronglyAdapted
3
Theoremsadd, div, inv, measurable, measurable_le, mul, neg, smul, stronglyAdapted, sub, stronglyAdapted_natural, stronglyAdapted, add, comp, div', finset_prod, finset_prod', finset_sum, finset_sum', inv, mul, neg, norm, stronglyAdapted, sub, adapted, add, div', inv, mul, neg, norm, progMeasurable_of_continuous, progMeasurable_of_discrete, smul, stronglyMeasurable, stronglyMeasurable_le, sub, adapted_const, adapted_const', progMeasurable_const, progMeasurable_of_tendsto, progMeasurable_of_tendsto', stronglyAdapted_const, stronglyAdapted_const', stronglyAdapted_iff_adapted, stronglyAdapted_zero, stronglyAdapted_zero'
48
Total51

MeasureTheory

Definitions

NameCategoryTheorems
Adapted πŸ“–MathDef
11 mathmath: Adapted.mul, Adapted.add, StronglyAdapted.adapted, adapted_const', adapted_const, Adapted.smul, Adapted.neg, Adapted.div, Adapted.inv, stronglyAdapted_iff_adapted, Adapted.sub
ProgMeasurable πŸ“–MathDef
20 mathmath: ProgMeasurable.sub, ProgMeasurable.finset_prod', StronglyAdapted.progMeasurable_of_continuous, ProgMeasurable.inv, IsPredictable.progMeasurable, ProgMeasurable.mul, ProgMeasurable.neg, ProgMeasurable.finset_sum', progMeasurable_min_stopping_time, ProgMeasurable.finset_prod, StronglyAdapted.progMeasurable_of_discrete, ProgMeasurable.finset_sum, ProgMeasurable.div', progMeasurable_const, progMeasurable_of_tendsto, ProgMeasurable.stoppedProcess, ProgMeasurable.comp, ProgMeasurable.add, ProgMeasurable.norm, progMeasurable_of_tendsto'
StronglyAdapted πŸ“–MathDef
31 mathmath: stronglyAdapted_const, Martingale.stronglyAdapted, stronglyAdapted_const', ProgMeasurable.stronglyAdapted_stoppedProcess, StronglyAdapted.sub, StronglyAdapted.inv, stronglyAdapted_zero, StronglyAdapted.stoppedProcess, Filtration.stronglyAdapted_natural, StronglyAdapted.stoppedProcess_of_discrete, stronglyAdapted_martingalePart, StronglyAdapted.neg, stronglyAdapted_predictablePart', StronglyAdapted.mul, stronglyAdapted_zero', StronglyAdapted.upcrossingStrat, StronglyAdapted.smul, Submartingale.stronglyAdapted, ProgMeasurable.stronglyAdapted, StronglyAdapted.add, Predictable.stronglyAdapted, BorelCantelli.stronglyAdapted_process, submartingale_iff_condExp_sub_nonneg, stronglyAdapted_predictablePart, stronglyAdapted_iff_adapted, StronglyAdapted.norm, IsPredictable.adapted, StronglyAdapted.div', Adapted.stronglyAdapted, Supermartingale.stronglyAdapted, ProbabilityTheory.Kernel.stronglyAdapted_densityProcess

Theorems

NameKindAssumesProvesValidatesDepends On
adapted_const πŸ“–mathematicalβ€”Adaptedβ€”adapted_const'
adapted_const' πŸ“–mathematicalβ€”Adaptedβ€”measurable_const
progMeasurable_const πŸ“–mathematicalβ€”ProgMeasurableβ€”stronglyMeasurable_const
progMeasurable_of_tendsto πŸ“–mathematicalProgMeasurable
Filter.Tendsto
Filter.atTop
Nat.instPreorder
nhds
Pi.topologicalSpace
ProgMeasurableβ€”progMeasurable_of_tendsto'
Filter.atTop_neBot
instIsDirectedOrder
IsStrictOrderedRing.toIsOrderedRing
Nat.instIsStrictOrderedRing
instArchimedeanNat
instIsCountablyGenerated_atTop
OrderTopology.of_linearLocallyFinite
instDiscreteTopologyNat
TopologicalSpace.SecondCountableTopology.to_separableSpace
TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace
Countable.LindelofSpace
instCountableNat
PseudoEMetricSpace.pseudoMetrizableSpace
progMeasurable_of_tendsto' πŸ“–mathematicalProgMeasurable
Filter.Tendsto
nhds
Pi.topologicalSpace
ProgMeasurableβ€”stronglyMeasurable_of_tendsto
tendsto_pi_nhds
Filter.Tendsto.apply_nhds
stronglyAdapted_const πŸ“–mathematicalβ€”StronglyAdaptedβ€”stronglyAdapted_const'
stronglyAdapted_const' πŸ“–mathematicalβ€”StronglyAdaptedβ€”stronglyMeasurable_const
stronglyAdapted_iff_adapted πŸ“–mathematicalBorelSpace
TopologicalSpace.PseudoMetrizableSpace
SecondCountableTopology
StronglyAdapted
Adapted
β€”StronglyAdapted.adapted
Adapted.stronglyAdapted
BorelSpace.opensMeasurable
stronglyAdapted_zero πŸ“–mathematicalβ€”StronglyAdapted
Pi.instZero
β€”stronglyMeasurable_zero
stronglyAdapted_zero' πŸ“–mathematicalβ€”StronglyAdapted
Pi.instZero
β€”stronglyMeasurable_zero

MeasureTheory.Adapted

Theorems

NameKindAssumesProvesValidatesDepends On
add πŸ“–mathematicalMeasurableAddβ‚‚
MeasureTheory.Adapted
MeasureTheory.Adapted
Pi.instAdd
β€”Measurable.add
div πŸ“–mathematicalMeasurableDivβ‚‚
MeasureTheory.Adapted
MeasureTheory.Adapted
Pi.instDiv
β€”Measurable.div
inv πŸ“–mathematicalMeasurableInv
InvOneClass.toInv
DivInvOneMonoid.toInvOneClass
DivisionMonoid.toDivInvOneMonoid
Group.toDivisionMonoid
MeasureTheory.Adapted
MeasureTheory.Adapted
Pi.instInv
β€”Measurable.inv
measurable πŸ“–mathematicalMeasureTheory.AdaptedMeasurableβ€”Measurable.mono
MeasureTheory.Filtration.le
le_refl
measurable_le πŸ“–mathematicalMeasureTheory.Adapted
Preorder.toLE
Measurable
MeasureTheory.Filtration.seq
β€”Measurable.mono
MeasureTheory.Filtration.mono
le_refl
mul πŸ“–mathematicalMeasurableMulβ‚‚
MeasureTheory.Adapted
MeasureTheory.Adapted
Pi.instMul
β€”Measurable.mul
neg πŸ“–mathematicalMeasurableNeg
NegZeroClass.toNeg
SubNegZeroMonoid.toNegZeroClass
SubtractionMonoid.toSubNegZeroMonoid
AddGroup.toSubtractionMonoid
MeasureTheory.Adapted
MeasureTheory.Adapted
Pi.instNeg
β€”Measurable.neg
smul πŸ“–mathematicalMeasurableSMul
MeasureTheory.Adapted
MeasureTheory.Adapted
Pi.instSMul
Function.hasSMul
β€”Measurable.const_smul
MeasurableSMul.toMeasurableConstSMul
stronglyAdapted πŸ“–mathematicalOpensMeasurableSpace
TopologicalSpace.PseudoMetrizableSpace
SecondCountableTopology
MeasureTheory.Adapted
MeasureTheory.StronglyAdaptedβ€”Measurable.stronglyMeasurable
sub πŸ“–mathematicalMeasurableSubβ‚‚
MeasureTheory.Adapted
MeasureTheory.Adapted
Pi.instSub
β€”Measurable.sub

MeasureTheory.Filtration

Theorems

NameKindAssumesProvesValidatesDepends On
stronglyAdapted_natural πŸ“–mathematicalTopologicalSpace.MetrizableSpace
BorelSpace
MeasureTheory.StronglyMeasurable
MeasureTheory.StronglyAdapted
natural
β€”MeasureTheory.StronglyMeasurable.mono
stronglyMeasurable_iff_measurable_separable
TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace
measurable_iff_comap_le
le_rfl
MeasureTheory.StronglyMeasurable.isSeparable_range
le_iSupβ‚‚_of_le
le_refl

MeasureTheory.Predictable

Theorems

NameKindAssumesProvesValidatesDepends On
stronglyAdapted πŸ“–mathematicalMeasureTheory.StronglyAdapted
Nat.instPreorder
MeasureTheory.StronglyMeasurable
MeasureTheory.Filtration.seq
MeasureTheory.StronglyAdapted
Nat.instPreorder
β€”MeasureTheory.StronglyMeasurable.mono
MeasureTheory.Filtration.mono

MeasureTheory.ProgMeasurable

Theorems

NameKindAssumesProvesValidatesDepends On
add πŸ“–mathematicalMeasureTheory.ProgMeasurableMeasureTheory.ProgMeasurableβ€”MeasureTheory.StronglyMeasurable.add
comp πŸ“–mathematicalMeasureTheory.ProgMeasurable
Preorder.toLE
MeasureTheory.ProgMeasurableβ€”Set.mem_Iic
LE.le.trans
Subtype.prop
MeasureTheory.StronglyMeasurable.comp_measurable
Measurable.prodMk
MeasureTheory.StronglyMeasurable.measurable
measurable_snd
div' πŸ“–mathematicalMeasureTheory.ProgMeasurableMeasureTheory.ProgMeasurable
DivInvMonoid.toDiv
Group.toDivInvMonoid
β€”MeasureTheory.StronglyMeasurable.div'
finset_prod πŸ“–mathematicalMeasureTheory.ProgMeasurableMeasureTheory.ProgMeasurable
Finset.prod
β€”Finset.prod_apply
finset_prod'
finset_prod' πŸ“–mathematicalMeasureTheory.ProgMeasurableMeasureTheory.ProgMeasurable
Finset.prod
Pi.commMonoid
β€”Finset.prod_induction
mul
MeasureTheory.progMeasurable_const
finset_sum πŸ“–mathematicalMeasureTheory.ProgMeasurableMeasureTheory.ProgMeasurable
Finset.sum
β€”Finset.sum_apply
finset_sum'
finset_sum' πŸ“–mathematicalMeasureTheory.ProgMeasurableMeasureTheory.ProgMeasurable
Finset.sum
Pi.addCommMonoid
β€”Finset.sum_induction
add
MeasureTheory.progMeasurable_const
inv πŸ“–mathematicalMeasureTheory.ProgMeasurableMeasureTheory.ProgMeasurable
InvOneClass.toInv
DivInvOneMonoid.toInvOneClass
DivisionMonoid.toDivInvOneMonoid
Group.toDivisionMonoid
β€”MeasureTheory.StronglyMeasurable.inv
mul πŸ“–mathematicalMeasureTheory.ProgMeasurableMeasureTheory.ProgMeasurableβ€”MeasureTheory.StronglyMeasurable.mul
neg πŸ“–mathematicalMeasureTheory.ProgMeasurableMeasureTheory.ProgMeasurable
NegZeroClass.toNeg
SubNegZeroMonoid.toNegZeroClass
SubtractionMonoid.toSubNegZeroMonoid
AddGroup.toSubtractionMonoid
β€”MeasureTheory.StronglyMeasurable.neg
norm πŸ“–mathematicalMeasureTheory.ProgMeasurable
UniformSpace.toTopologicalSpace
PseudoMetricSpace.toUniformSpace
SeminormedAddCommGroup.toPseudoMetricSpace
MeasureTheory.ProgMeasurable
Real
UniformSpace.toTopologicalSpace
PseudoMetricSpace.toUniformSpace
Real.pseudoMetricSpace
Norm.norm
SeminormedAddCommGroup.toNorm
β€”MeasureTheory.StronglyMeasurable.norm
stronglyAdapted πŸ“–mathematicalMeasureTheory.ProgMeasurableMeasureTheory.StronglyAdaptedβ€”Set.mem_Iic
le_rfl
MeasureTheory.StronglyMeasurable.comp_measurable
measurable_prodMk_left
sub πŸ“–mathematicalMeasureTheory.ProgMeasurableMeasureTheory.ProgMeasurable
SubNegMonoid.toSub
AddGroup.toSubNegMonoid
β€”MeasureTheory.StronglyMeasurable.sub

MeasureTheory.StronglyAdapted

Theorems

NameKindAssumesProvesValidatesDepends On
adapted πŸ“–mathematicalBorelSpace
TopologicalSpace.PseudoMetrizableSpace
MeasureTheory.StronglyAdapted
MeasureTheory.Adaptedβ€”MeasureTheory.StronglyMeasurable.measurable
add πŸ“–mathematicalContinuousAdd
MeasureTheory.StronglyAdapted
MeasureTheory.StronglyAdapted
Pi.instAdd
β€”MeasureTheory.StronglyMeasurable.add
div' πŸ“–mathematicalContinuousDiv
MeasureTheory.StronglyAdapted
MeasureTheory.StronglyAdapted
Pi.instDiv
β€”MeasureTheory.StronglyMeasurable.div'
inv πŸ“–mathematicalContinuousInv
InvOneClass.toInv
DivInvOneMonoid.toInvOneClass
DivisionMonoid.toDivInvOneMonoid
Group.toDivisionMonoid
MeasureTheory.StronglyAdapted
MeasureTheory.StronglyAdapted
Pi.instInv
β€”MeasureTheory.StronglyMeasurable.inv
mul πŸ“–mathematicalContinuousMul
MeasureTheory.StronglyAdapted
MeasureTheory.StronglyAdapted
Pi.instMul
β€”MeasureTheory.StronglyMeasurable.mul
neg πŸ“–mathematicalContinuousNeg
NegZeroClass.toNeg
SubNegZeroMonoid.toNegZeroClass
SubtractionMonoid.toSubNegZeroMonoid
AddGroup.toSubtractionMonoid
MeasureTheory.StronglyAdapted
MeasureTheory.StronglyAdapted
Pi.instNeg
β€”MeasureTheory.StronglyMeasurable.neg
norm πŸ“–mathematicalMeasureTheory.StronglyAdapted
UniformSpace.toTopologicalSpace
PseudoMetricSpace.toUniformSpace
SeminormedAddCommGroup.toPseudoMetricSpace
MeasureTheory.StronglyAdapted
Real
UniformSpace.toTopologicalSpace
PseudoMetricSpace.toUniformSpace
Real.pseudoMetricSpace
Norm.norm
SeminormedAddCommGroup.toNorm
β€”MeasureTheory.StronglyMeasurable.norm
progMeasurable_of_continuous πŸ“–mathematicalMeasureTheory.StronglyAdapted
Continuous
MeasureTheory.ProgMeasurableβ€”MeasureTheory.stronglyMeasurable_uncurry_of_continuous_of_stronglyMeasurable
TopologicalSpace.MetrizableSpace.subtype
TopologicalSpace.Subtype.secondCountableTopology
Subtype.opensMeasurableSpace
Continuous.comp
continuous_induced_dom
MeasureTheory.StronglyMeasurable.mono
MeasureTheory.Filtration.mono
Subtype.prop
progMeasurable_of_discrete πŸ“–mathematicalMeasureTheory.StronglyAdaptedMeasureTheory.ProgMeasurableβ€”progMeasurable_of_continuous
TopologicalSpace.DiscreteTopology.metrizableSpace
continuous_of_discreteTopology
smul πŸ“–mathematicalContinuousConstSMul
Real
MeasureTheory.StronglyAdapted
MeasureTheory.StronglyAdapted
Real
Pi.instSMul
Function.hasSMul
β€”MeasureTheory.StronglyMeasurable.const_smul
stronglyMeasurable πŸ“–mathematicalMeasureTheory.StronglyAdaptedMeasureTheory.StronglyMeasurableβ€”MeasureTheory.StronglyMeasurable.mono
MeasureTheory.Filtration.le
stronglyMeasurable_le πŸ“–mathematicalMeasureTheory.StronglyAdapted
Preorder.toLE
MeasureTheory.StronglyMeasurable
MeasureTheory.Filtration.seq
β€”MeasureTheory.StronglyMeasurable.mono
MeasureTheory.Filtration.mono
sub πŸ“–mathematicalContinuousSub
MeasureTheory.StronglyAdapted
MeasureTheory.StronglyAdapted
Pi.instSub
β€”MeasureTheory.StronglyMeasurable.sub

---

← Back to Index