Theorems · Theorem · probability

ProbabilityTheory.IndepFun.hasGaussianLaw_sub_of_sub

∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {X Y : Ω → E},
  ProbabilityTheory.HasGaussianLaw X P →
    ProbabilityTheory.HasGaussianLaw Y P →
      ProbabilityTheory.IndepFun X (Y - X) P → ProbabilityTheory.HasGaussianLaw (Y - X) P

If X and Y are two Gaussian random variables such that X and Y - X are independent, then Y - X is Gaussian. This lemma is useful to prove that a process with independent increments and whose marginals are Gaussian has Gaussian increments.

Defined in

Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceMeasurableSpaceBorelSpaceSecondCountableTopology