Multivariate Gaussian distributions

noncomputable def ProbabilityTheory.stdGaussian (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] : MeasureTheory.Measure E

Standard Gaussian distribution on E.

Equations

• One or more equations did not get rendered due to their size.

instance ProbabilityTheory.isProbabilityMeasure_stdGaussian {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] : MeasureTheory.IsProbabilityMeasure (stdGaussian E)

theorem ProbabilityTheory.integrable_eval_pi {d : ℕ} {i : Fin d} {μ : Fin d → MeasureTheory.Measure ℝ} [∀ (i : Fin d), MeasureTheory.IsProbabilityMeasure (μ i)] {f : ℝ → ℝ} (hf : MeasureTheory.Integrable f (μ i)) : MeasureTheory.Integrable (fun (a : Fin d → ℝ) => f (a i)) (MeasureTheory.Measure.pi μ)

theorem ProbabilityTheory.integral_eval_pi {d : ℕ} {i : Fin d} {μ : Fin d → MeasureTheory.Measure ℝ} [∀ (i : Fin d), MeasureTheory.IsProbabilityMeasure (μ i)] {f : ℝ → ℝ} (hf : MeasureTheory.Integrable f (μ i)) : ∫ (a : Fin d → ℝ), f (a i) ∂MeasureTheory.Measure.pi μ = ∫ (x : ℝ), f x ∂μ i

theorem ProbabilityTheory.isCentered_stdGaussian {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : NormedSpace.Dual ℝ E) : ∫ (x : E), L x ∂stdGaussian E = 0

theorem ProbabilityTheory.variance_dual_stdGaussian {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : NormedSpace.Dual ℝ E) : variance (⇑L) (stdGaussian E) = ∑ i : Fin (Module.finrank ℝ E), L ((stdOrthonormalBasis ℝ E) i) ^ 2

instance ProbabilityTheory.isGaussian_stdGaussian {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] : IsGaussian (stdGaussian E)

noncomputable def ProbabilityTheory.multivariateGaussian {d : ℕ} (μ : EuclideanSpace ℝ (Fin d)) (S : Matrix (Fin d) (Fin d) ℝ) (hS : S.PosSemidef) : MeasureTheory.Measure (EuclideanSpace ℝ (Fin d))

Equations

• One or more equations did not get rendered due to their size.

instance ProbabilityTheory.isGaussian_multivariateGaussian {d : ℕ} {μ : EuclideanSpace ℝ (Fin d)} {S : Matrix (Fin d) (Fin d) ℝ} {hS : S.PosSemidef} : IsGaussian (multivariateGaussian μ S hS)