Theorems · Theorem · probability

ProbabilityTheory.IsGaussianProcess.hasGaussianLaw

∀ {Ω : Type u_1} {E : Type u_2} {T : Type u_3} {mΩ : MeasurableSpace Ω} [inst : MeasurableSpace E]
  [inst_1 : TopologicalSpace E] [inst_2 : AddCommMonoid E] [inst_3 : Module ℝ E] {X : T → Ω → E}
  {P : autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.IsGaussianProcess._auto_1},
  ProbabilityTheory.IsGaussianProcess X P →
    ∀ (I : Finset T), ProbabilityTheory.HasGaussianLaw (fun ω => I.restrict fun x => X x ω) P

Defined in

Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Def

Cited by

10 results in Mathlib

Foundations

Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpaceTopologicalSpaceAddCommMonoidModule