Theorems · Theorem · probability

ProbabilityTheory.isGaussian_map_of_measurable

∀ {E : Type u_1} {F : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommMonoid E] [inst_2 : Module ℝ E]
  {mE : MeasurableSpace E} [inst_3 : TopologicalSpace F] [inst_4 : AddCommMonoid F] [inst_5 : Module ℝ F]
  {mF : MeasurableSpace F} [OpensMeasurableSpace F] {μ : MeasureTheory.Measure E} {L : E →L[ℝ] F}
  [ProbabilityTheory.IsGaussian μ], Measurable ⇑L → ProbabilityTheory.IsGaussian (MeasureTheory.Measure.map (⇑L) μ)

Mapping a Gaussian measure by a measurable and continuous linear map yields a Gaussian measure. See also isGaussian_map, which does not assume measurability but has stronger hypotheses on E. In particular, it requires E to be a Borel space, which requires some second countability hypotheses if E is a product space. This version does not, which can be useful for instance if L := Prod.fst, which is always measurable.

Defined in

Mathlib.Probability.Distributions.Gaussian.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceAddCommMonoidModuleTopologicalSpaceAddCommMonoidModuleOpensMeasurableSpaceProbabilityTheory.IsGaussian