Documentation Verification Report

Basic

📁 Source: Mathlib/Probability/Distributions/Gaussian/IsGaussianProcess/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems `aemeasurable`, `comp_left`, `comp_right`, `hasGaussianLaw_add`, `hasGaussianLaw_eval`, `hasGaussianLaw_fun_add`, `hasGaussianLaw_fun_sub`, `hasGaussianLaw_fun_sum`, `hasGaussianLaw_increments`, `hasGaussianLaw_prodMk`, `hasGaussianLaw_sub`, `hasGaussianLaw_sum`, `isProbabilityMeasure`, `of_isGaussianProcess`, `restrict`, `shift`, `smul`	17
Total	17

ProbabilityTheory.IsGaussianProcess

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`aemeasurable` 📖	mathematical	`ProbabilityTheory.IsGaussianProcess`	`AEMeasurable`	—	`AEMeasurable.eval` `AEMeasurable.of_map_ne_zero` `MeasureTheory.IsProbabilityMeasure.ne_zero` `ProbabilityTheory.IsGaussian.toIsProbabilityMeasure` `ProbabilityTheory.HasGaussianLaw.isGaussian_map` `hasGaussianLaw`
`comp_left` 📖	mathematical	`ProbabilityTheory.IsGaussianProcess` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real` `Real.normedField`	`DFunLike.coe` `ContinuousLinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousLinearMap.funLike`	—	`of_isGaussianProcess` `map_add` `SemilinearMapClass.toAddHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `Continuous.clm_apply` `continuous_const` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `continuous_apply`
`comp_right` 📖	—	`ProbabilityTheory.IsGaussianProcess` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real` `Real.normedField`	—	—	`of_isGaussianProcess` `continuous_apply`
`hasGaussianLaw_add` 📖	mathematical	`ProbabilityTheory.IsGaussianProcess` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real` `Real.normedField`	`ProbabilityTheory.HasGaussianLaw` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`ProbabilityTheory.HasGaussianLaw.add` `hasGaussianLaw_prodMk`
`hasGaussianLaw_eval` 📖	mathematical	`ProbabilityTheory.IsGaussianProcess` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real` `Real.normedField`	`ProbabilityTheory.HasGaussianLaw`	—	`ProbabilityTheory.HasGaussianLaw.map` `Pi.borelSpace_of_subsingleton` `Unique.instSubsingleton` `hasGaussianLaw`
`hasGaussianLaw_fun_add` 📖	mathematical	`ProbabilityTheory.IsGaussianProcess` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real` `Real.normedField`	`ProbabilityTheory.HasGaussianLaw` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`hasGaussianLaw_add`
`hasGaussianLaw_fun_sub` 📖	mathematical	`ProbabilityTheory.IsGaussianProcess` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real` `Real.normedField`	`ProbabilityTheory.HasGaussianLaw` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`hasGaussianLaw_sub`
`hasGaussianLaw_fun_sum` 📖	mathematical	`ProbabilityTheory.IsGaussianProcess` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real` `Real.normedField`	`ProbabilityTheory.HasGaussianLaw` `Finset.sum`	—	`Finset.sum_apply` `hasGaussianLaw_sum`
`hasGaussianLaw_increments` 📖	mathematical	`ProbabilityTheory.IsGaussianProcess` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real` `Real.normedField`	`ProbabilityTheory.HasGaussianLaw` `Pi.topologicalSpace` `Pi.addCommMonoid` `Pi.Function.module` `Real.semiring` `MeasurableSpace.pi` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.const_add_termg` `Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval` `Mathlib.Tactic.Module.NF.sub_eq_eval` `Mathlib.Tactic.Module.NF.smul_eq_eval` `Mathlib.Tactic.Module.NF.atom_eq_eval` `Mathlib.Tactic.Module.NF.eval_algebraMap` `AddCommMonoid.nat_isScalarTower` `Mathlib.Tactic.Module.NF.sub_eq_eval₁` `Mathlib.Tactic.Module.NF.zero_sub_eq_eval` `AddCommGroup.intIsScalarTower` `Mathlib.Tactic.Module.NF.eq_cons_cons` `eq_natCast` `RingHom.instRingHomClass` `Nat.cast_one` `eq_intCast` `Int.cast_one` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Int.cast_neg` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `continuous_pi` `Continuous.sub` `IsTopologicalAddGroup.to_continuousSub` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `continuous_apply` `ProbabilityTheory.HasGaussianLaw.map` `Pi.borelSpace` `Finite.to_countable` `Finite.of_fintype` `instCountableFin` `hasGaussianLaw`
`hasGaussianLaw_prodMk` 📖	mathematical	`ProbabilityTheory.IsGaussianProcess` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real` `Real.normedField`	`ProbabilityTheory.HasGaussianLaw` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `Real.semiring` `Prod.instMeasurableSpace`	—	`ProbabilityTheory.HasGaussianLaw.prodMk` `Finite.of_fintype` `hasGaussianLaw`
`hasGaussianLaw_sub` 📖	mathematical	`ProbabilityTheory.IsGaussianProcess` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real` `Real.normedField`	`ProbabilityTheory.HasGaussianLaw` `Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`ProbabilityTheory.HasGaussianLaw.sub` `hasGaussianLaw_prodMk`
`hasGaussianLaw_sum` 📖	mathematical	`ProbabilityTheory.IsGaussianProcess` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real` `Real.normedField`	`ProbabilityTheory.HasGaussianLaw` `Finset.sum` `Pi.addCommMonoid`	—	`Finset.sum_congr` `Finset.sum_attach` `ProbabilityTheory.HasGaussianLaw.sum` `hasGaussianLaw`
`isProbabilityMeasure` 📖	mathematical	`ProbabilityTheory.IsGaussianProcess`	`MeasureTheory.IsProbabilityMeasure`	—	`ProbabilityTheory.HasGaussianLaw.isProbabilityMeasure` `hasGaussianLaw`
`of_isGaussianProcess` 📖	—	`ProbabilityTheory.IsGaussianProcess` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real` `Real.normedField` `DFunLike.coe` `ContinuousLinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.topologicalSpace` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Pi.addCommMonoid` `Pi.Function.module` `ContinuousLinearMap.funLike` `Finset.restrict`	—	—	`Finset.mem_biUnion` `map_add` `SemilinearMapClass.toAddHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `continuous_pi` `Continuous.comp'` `ContinuousLinearMap.continuous` `continuous_apply` `ProbabilityTheory.HasGaussianLaw.map` `Pi.borelSpace` `Finite.to_countable` `Finite.of_fintype` `hasGaussianLaw`
`restrict` 📖	mathematical	`ProbabilityTheory.IsGaussianProcess` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real` `Real.normedField`	`Set.Elem` `Set` `Set.instMembership`	—	`comp_right`
`shift` 📖	mathematical	`ProbabilityTheory.IsGaussianProcess` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real` `Real.normedField`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`of_isGaussianProcess` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.const_add_termg` `Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval` `Mathlib.Tactic.Module.NF.sub_eq_eval` `Mathlib.Tactic.Module.NF.smul_eq_eval` `Mathlib.Tactic.Module.NF.atom_eq_eval` `Mathlib.Tactic.Module.NF.eval_algebraMap` `AddCommMonoid.nat_isScalarTower` `Mathlib.Tactic.Module.NF.sub_eq_eval₁` `Mathlib.Tactic.Module.NF.zero_sub_eq_eval` `AddCommGroup.intIsScalarTower` `Mathlib.Tactic.Module.NF.eq_cons_cons` `eq_natCast` `RingHom.instRingHomClass` `Nat.cast_one` `eq_intCast` `Int.cast_one` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Int.cast_neg` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Continuous.sub` `IsTopologicalAddGroup.to_continuousSub` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `continuous_apply`
`smul` 📖	mathematical	`ProbabilityTheory.IsGaussianProcess` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real` `Real.normedField`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring`	—	`comp_left` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `IsScalarTower.left`

---

← Back to Index