Documentation Verification Report

HasIndepIncrements

📁 Source: Mathlib/Probability/Independence/Process/HasIndepIncrements.lean

Statistics

Metric	Count
Definitions `HasIndepIncrements`	1
Theorems `indepFun_eval_sub`, `indepFun_sub_sub`, `map`, `map'`, `nat`, `neg`, `of_nat`, `smul`, `hasIndepIncrements_iff_nat`	9
Total	10

ProbabilityTheory

Definitions

Name	Category	Theorems
`HasIndepIncrements` 📖	MathDef	6 math math: `hasIndepIncrements_iff_nat`, `HasIndepIncrements.map`, `HasIndepIncrements.map'`, `HasIndepIncrements.of_nat`, `HasIndepIncrements.neg`, `HasIndepIncrements.smul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasIndepIncrements_iff_nat` 📖	mathematical	—	`HasIndepIncrements` `iIndepFun`	—	`HasIndepIncrements.nat` `HasIndepIncrements.of_nat`

ProbabilityTheory.HasIndepIncrements

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`indepFun_eval_sub` 📖	mathematical	`ProbabilityTheory.HasIndepIncrements` `SubNegMonoid.toSub` `SubNegZeroMonoid.toSubNegMonoid` `Preorder.toLE` `Filter.Eventually` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	`ProbabilityTheory.IndepFun` `Pi.instSub` `SubNegMonoid.toSub` `SubNegZeroMonoid.toSubNegMonoid`	—	`MeasureTheory.Measure.instOuterMeasureClass` `ProbabilityTheory.IndepFun.congr` `indepFun_sub_sub` `Filter.mp_mem` `Filter.univ_mem'` `sub_zero` `Filter.EventuallyEq.rfl`
`indepFun_sub_sub` 📖	mathematical	`ProbabilityTheory.HasIndepIncrements` `Preorder.toLE`	`ProbabilityTheory.IndepFun` `Pi.instSub`	—	`ProbabilityTheory.iIndepFun.indepFun` `nat`
`map` 📖	mathematical	`ProbabilityTheory.HasIndepIncrements` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup`	`ProbabilityTheory.HasIndepIncrements` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `ContinuousLinearMap.funLike`	—	`map'` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `ContinuousLinearMap.measurable`
`map'` 📖	mathematical	`Measurable` `DFunLike.coe` `ProbabilityTheory.HasIndepIncrements` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	`ProbabilityTheory.HasIndepIncrements` `SubNegMonoid.toSub` `SubtractionMonoid.toSubNegMonoid` `DFunLike.coe`	—	`ProbabilityTheory.iIndepFun.comp`
`nat` 📖	mathematical	`ProbabilityTheory.HasIndepIncrements` `Monotone` `Nat.instPreorder`	`ProbabilityTheory.iIndepFun`	—	`ProbabilityTheory.iIndepFun_iff_finset` `Finset.eq_empty_or_nonempty` `ProbabilityTheory.iIndepFun.isProbabilityMeasure` `ProbabilityTheory.iIndepFun.of_subsingleton` `IsEmpty.instSubsingleton` `Finset.instIsEmpty` `Finset.le_max'` `ProbabilityTheory.iIndepFun.precomp` `Monotone.comp` `StrictMono.monotone` `Fin.val_strictMono`
`neg` 📖	mathematical	`ProbabilityTheory.HasIndepIncrements` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	`ProbabilityTheory.HasIndepIncrements` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`map'` `AddMonoidHom.instAddMonoidHomClass` `MeasurableNeg.measurable_neg`
`of_nat` 📖	mathematical	`ProbabilityTheory.iIndepFun`	`ProbabilityTheory.HasIndepIncrements`	—	`ProbabilityTheory.iIndepFun.precomp` `Fin.val_injective` `Filter.eventuallyConst_atTop`
`smul` 📖	mathematical	`ProbabilityTheory.HasIndepIncrements` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	`ProbabilityTheory.HasIndepIncrements` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass`	—	`map'` `AddMonoidHom.instAddMonoidHomClass` `MeasurableConstSMul.measurable_const_smul`

---

← Back to Index