Theorems · Theorem · probability

ProbabilityTheory.IsGaussianProcess.indepFun_of_covariance_inner

∀ {T : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E]
  [CompleteSpace E] {S : Type u_4} {X : S → Ω → E} {Y : T → Ω → E} [inst_5 : InnerProductSpace ℝ E],
  ProbabilityTheory.IsGaussianProcess (Sum.elim X Y) P →
    (∀ (s : S), AEMeasurable (X s) P) →
      (∀ (t : T), AEMeasurable (Y t) P) →
        (∀ (s : S) (t : T) (x y : E),
            ProbabilityTheory.covariance (fun ω => inner ℝ x (X s ω)) (fun ω => inner ℝ y (Y t ω)) P = 0) →
          ProbabilityTheory.IndepFun (fun ω s => X s ω) (fun ω t => Y t ω) P

Two Gaussian processes $(X_s)_{s \in S}$ and $(Y_t)_{t \in T}$ that are jointly Gaussian are independent if for all $s \in S$ and $t \in T$, $X_s$ and $Y_t$ are uncorrelated.

Defined in

Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupMeasurableSpaceBorelSpaceSecondCountableTopologyCompleteSpaceInnerProductSpace