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 {ι : Type u_2} {𝕜 : Type u_3} [Fintype ι] [NormedCommRing 𝕜] {X : ι → Type u_4} {i : ι} {mX : (i : ι) → MeasurableSpace (X i)} {μ : (i : ι) → MeasureTheory.Measure (X i)} [∀ (i : ι), MeasureTheory.IsFiniteMeasure (μ i)] {f : X i → 𝕜} (hf : MeasureTheory.Integrable f (μ i)) : MeasureTheory.Integrable (fun (x : (i : ι) → X i) => f (x i)) (MeasureTheory.Measure.pi μ)

theorem ProbabilityTheory.integral_eval_pi {ι : Type u_2} {𝕜 : Type u_3} [Fintype ι] [RCLike 𝕜] {X : ι → Type u_4} {i : ι} {mX : (i : ι) → MeasurableSpace (X i)} {μ : (i : ι) → MeasureTheory.Measure (X i)} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] {f : X i → 𝕜} : ∫ (x : (i : ι) → X i), f (x i) ∂MeasureTheory.Measure.pi μ = ∫ (x : X i), f x ∂μ i

@[simp]

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

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) = ‖L‖ ^ 2

theorem ProbabilityTheory.charFun_stdGaussian {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (t : E) : MeasureTheory.charFun (stdGaussian E) t = Complex.exp (-↑‖t‖ ^ 2 / 2)

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

theorem ProbabilityTheory.charFunDual_stdGaussian {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : NormedSpace.Dual ℝ E) : MeasureTheory.charFunDual (stdGaussian E) L = Complex.exp (-↑‖L‖ ^ 2 / 2)

theorem ProbabilityTheory.covInnerBilin_stdGaussian {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] : covInnerBilin (stdGaussian E) = ContinuousBilinForm.inner E

theorem ProbabilityTheory.covMatrix_stdGaussian {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] : covMatrix (stdGaussian E) = 1

theorem ProbabilityTheory.stdGaussian_map {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [MeasurableSpace F] [BorelSpace F] (f : E ≃ₗᵢ[ℝ] F) : MeasureTheory.Measure.map (⇑f) (stdGaussian E) = stdGaussian F

theorem ProbabilityTheory.pi_eq_stdGaussian {n : Type u_2} [Fintype n] : (MeasureTheory.Measure.pi fun (x : n) => gaussianReal 0 1) = stdGaussian (EuclideanSpace ℝ n)

theorem ProbabilityTheory.stdGaussian_eq_pi_map_orthonormalBasis {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {ι : Type u_2} [Fintype ι] (b : OrthonormalBasis ι ℝ E) : stdGaussian E = MeasureTheory.Measure.map (fun (x : ι → ℝ) => ∑ i : ι, x i • b i) (MeasureTheory.Measure.pi fun (x : ι) => gaussianReal 0 1)

noncomputable def ProbabilityTheory.multivariateGaussian {ι : Type u_2} [Fintype ι] [DecidableEq ι] (μ : EuclideanSpace ℝ ι) (S : Matrix ι ι ℝ) (hS : S.PosSemidef) : MeasureTheory.Measure (EuclideanSpace ℝ ι)

Equations

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

instance ProbabilityTheory.isGaussian_multivariateGaussian {ι : Type u_2} [Fintype ι] [DecidableEq ι] {μ : EuclideanSpace ℝ ι} {S : Matrix ι ι ℝ} {hS : S.PosSemidef} : IsGaussian (multivariateGaussian μ S hS)

@[simp]

theorem ProbabilityTheory.integral_id_multivariateGaussian {ι : Type u_2} [Fintype ι] [DecidableEq ι] {μ : EuclideanSpace ℝ ι} {S : Matrix ι ι ℝ} {hS : S.PosSemidef} : ∫ (x : EuclideanSpace ℝ ι), x ∂multivariateGaussian μ S hS = μ

theorem ProbabilityTheory.inner_toEuclideanCLM {ι : Type u_2} [Fintype ι] [DecidableEq ι] {S : Matrix ι ι ℝ} (x y : EuclideanSpace ℝ ι) : inner ℝ x ((Matrix.toEuclideanCLM S) y) = ⇑((EuclideanSpace.basisFun ι ℝ).toBasis.repr x) ⬝ᵥ S.mulVec ⇑((EuclideanSpace.basisFun ι ℝ).toBasis.repr y)

theorem ProbabilityTheory.covInnerBilin_multivariateGaussian {ι : Type u_2} [Fintype ι] [DecidableEq ι] {μ : EuclideanSpace ℝ ι} {S : Matrix ι ι ℝ} {hS : S.PosSemidef} : covInnerBilin (multivariateGaussian μ S hS) = ContinuousBilinForm.ofMatrix S (EuclideanSpace.basisFun ι ℝ).toBasis

theorem ProbabilityTheory.covariance_eval_multivariateGaussian {ι : Type u_2} [Fintype ι] [DecidableEq ι] {μ : EuclideanSpace ℝ ι} {S : Matrix ι ι ℝ} {hS : S.PosSemidef} (i j : ι) : covariance (fun (x : EuclideanSpace ℝ ι) => x i) (fun (x : EuclideanSpace ℝ ι) => x j) (multivariateGaussian μ S hS) = S i j

theorem ProbabilityTheory.variance_eval_multivariateGaussian {ι : Type u_2} [Fintype ι] [DecidableEq ι] {μ : EuclideanSpace ℝ ι} {S : Matrix ι ι ℝ} {hS : S.PosSemidef} (i : ι) : variance (fun (x : EuclideanSpace ℝ ι) => x i) (multivariateGaussian μ S hS) = S i i

theorem ProbabilityTheory.measurePreserving_multivariateGaussian {ι : Type u_2} [Fintype ι] [DecidableEq ι] {μ : EuclideanSpace ℝ ι} {S : Matrix ι ι ℝ} {hS : S.PosSemidef} {i : ι} : MeasureTheory.MeasurePreserving (fun (x : EuclideanSpace ℝ ι) => x i) (multivariateGaussian μ S hS) (gaussianReal (μ i) (S i i).toNNReal)

theorem ProbabilityTheory.charFun_multivariateGaussian {ι : Type u_2} [Fintype ι] [DecidableEq ι] {μ : EuclideanSpace ℝ ι} {S : Matrix ι ι ℝ} {hS : S.PosSemidef} (x : EuclideanSpace ℝ ι) : MeasureTheory.charFun (multivariateGaussian μ S hS) x = Complex.exp (↑(inner ℝ x μ) * Complex.I - ↑(((ContinuousBilinForm.ofMatrix S (EuclideanSpace.basisFun ι ℝ).toBasis) x) x) / 2)