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, stronglyAdapted, sub, adapted, add, div, inv, mul, neg, 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'
46
Total49

MeasureTheory

Definitions

NameCategoryTheorems
Adapted πŸ“–MathDef
4 mathmath: StronglyAdapted.adapted, adapted_const', adapted_const, stronglyAdapted_iff_adapted
ProgMeasurable πŸ“–MathDef
5 mathmath: StronglyAdapted.progMeasurable_of_continuous, IsPredictable.progMeasurable, progMeasurable_min_stopping_time, StronglyAdapted.progMeasurable_of_discrete, progMeasurable_const
StronglyAdapted πŸ“–MathDef
18 mathmath: stronglyAdapted_const, Martingale.stronglyAdapted, stronglyAdapted_const', ProgMeasurable.stronglyAdapted_stoppedProcess, stronglyAdapted_zero, Filtration.stronglyAdapted_natural, stronglyAdapted_predictablePart', stronglyAdapted_zero', Submartingale.stronglyAdapted, ProgMeasurable.stronglyAdapted, BorelCantelli.stronglyAdapted_process, submartingale_iff_condExp_sub_nonneg, stronglyAdapted_predictablePart, stronglyAdapted_iff_adapted, IsPredictable.adapted, 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 πŸ“–β€”ProgMeasurable
Filter.Tendsto
Filter.atTop
Nat.instPreorder
nhds
Pi.topologicalSpace
β€”β€”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' πŸ“–β€”ProgMeasurable
Filter.Tendsto
nhds
Pi.topologicalSpace
β€”β€”stronglyMeasurable_of_tendsto
tendsto_pi_nhds
tendsto_nhds
IsOpen.preimage
continuous_apply
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
Pi.instAddβ€”Measurable.add
div πŸ“–mathematicalMeasurableDivβ‚‚
MeasureTheory.Adapted
Pi.instDivβ€”Measurable.div
inv πŸ“–mathematicalMeasurableInv
InvOneClass.toInv
DivInvOneMonoid.toInvOneClass
DivisionMonoid.toDivInvOneMonoid
Group.toDivisionMonoid
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
Pi.instMulβ€”Measurable.mul
neg πŸ“–mathematicalMeasurableNeg
NegZeroClass.toNeg
SubNegZeroMonoid.toNegZeroClass
SubtractionMonoid.toSubNegZeroMonoid
AddGroup.toSubtractionMonoid
MeasureTheory.Adapted
Pi.instNegβ€”Measurable.neg
smul πŸ“–mathematicalMeasurableSMul
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
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 πŸ“–β€”MeasureTheory.StronglyAdapted
Nat.instPreorder
MeasureTheory.StronglyMeasurable
MeasureTheory.Filtration.seq
β€”β€”MeasureTheory.StronglyMeasurable.mono
MeasureTheory.Filtration.mono

MeasureTheory.ProgMeasurable

Theorems

NameKindAssumesProvesValidatesDepends On
add πŸ“–β€”MeasureTheory.ProgMeasurableβ€”β€”MeasureTheory.StronglyMeasurable.add
comp πŸ“–β€”MeasureTheory.ProgMeasurable
Preorder.toLE
β€”β€”Set.mem_Iic
LE.le.trans
Subtype.prop
MeasureTheory.StronglyMeasurable.comp_measurable
Measurable.prodMk
MeasureTheory.StronglyMeasurable.measurable
measurable_snd
div πŸ“–mathematicalMeasureTheory.ProgMeasurableDivInvMonoid.toDiv
Group.toDivInvMonoid
β€”MeasureTheory.StronglyMeasurable.div
finset_prod πŸ“–mathematicalMeasureTheory.ProgMeasurableFinset.prodβ€”Finset.prod_apply
finset_prod'
finset_prod' πŸ“–mathematicalMeasureTheory.ProgMeasurableFinset.prod
Pi.commMonoid
β€”Finset.prod_induction
mul
MeasureTheory.progMeasurable_const
finset_sum πŸ“–mathematicalMeasureTheory.ProgMeasurableFinset.sumβ€”Finset.sum_apply
finset_sum'
finset_sum' πŸ“–mathematicalMeasureTheory.ProgMeasurableFinset.sum
Pi.addCommMonoid
β€”Finset.sum_induction
add
MeasureTheory.progMeasurable_const
inv πŸ“–mathematicalMeasureTheory.ProgMeasurableInvOneClass.toInv
DivInvOneMonoid.toInvOneClass
DivisionMonoid.toDivInvOneMonoid
Group.toDivisionMonoid
β€”MeasureTheory.StronglyMeasurable.inv
mul πŸ“–β€”MeasureTheory.ProgMeasurableβ€”β€”MeasureTheory.StronglyMeasurable.mul
neg πŸ“–mathematicalMeasureTheory.ProgMeasurableNegZeroClass.toNeg
SubNegZeroMonoid.toNegZeroClass
SubtractionMonoid.toSubNegZeroMonoid
AddGroup.toSubtractionMonoid
β€”MeasureTheory.StronglyMeasurable.neg
stronglyAdapted πŸ“–mathematicalMeasureTheory.ProgMeasurableMeasureTheory.StronglyAdaptedβ€”Set.mem_Iic
le_rfl
MeasureTheory.StronglyMeasurable.comp_measurable
measurable_prodMk_left
sub πŸ“–mathematicalMeasureTheory.ProgMeasurableSubNegMonoid.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
Pi.instAddβ€”MeasureTheory.StronglyMeasurable.add
div πŸ“–mathematicalContinuousDiv
MeasureTheory.StronglyAdapted
Pi.instDivβ€”MeasureTheory.StronglyMeasurable.div
inv πŸ“–mathematicalContinuousInv
InvOneClass.toInv
DivInvOneMonoid.toInvOneClass
DivisionMonoid.toDivInvOneMonoid
Group.toDivisionMonoid
MeasureTheory.StronglyAdapted
Pi.instInvβ€”MeasureTheory.StronglyMeasurable.inv
mul πŸ“–mathematicalContinuousMul
MeasureTheory.StronglyAdapted
Pi.instMulβ€”MeasureTheory.StronglyMeasurable.mul
neg πŸ“–mathematicalContinuousNeg
NegZeroClass.toNeg
SubNegZeroMonoid.toNegZeroClass
SubtractionMonoid.toSubNegZeroMonoid
AddGroup.toSubtractionMonoid
MeasureTheory.StronglyAdapted
Pi.instNegβ€”MeasureTheory.StronglyMeasurable.neg
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
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
Pi.instSubβ€”MeasureTheory.StronglyMeasurable.sub

---

← Back to Index