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} {E : Type u_3} [Fintype ι] [NormedAddCommGroup E] {X : ι → Type u_4} {i : ι} {mX : (i : ι) → MeasurableSpace (X i)} {μ : (i : ι) → MeasureTheory.Measure (X i)} [∀ (i : ι), MeasureTheory.IsFiniteMeasure (μ i)] {f : X i → E} (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} {E : Type u_3} [Fintype ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {X : ι → Type u_4} {mX : (i : ι) → MeasurableSpace (X i)} {μ : (i : ι) → MeasureTheory.Measure (X i)} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] {i : ι} {f : X i → E} (hf : MeasureTheory.AEStronglyMeasurable f (μ 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.

theorem ProbabilityTheory.multivariateGaussian_congr_matrix {ι : Type u_2} [Fintype ι] [DecidableEq ι] {μ : EuclideanSpace ℝ ι} {S S' : Matrix ι ι ℝ} {hS : S.PosSemidef} (h : S = S') : multivariateGaussian μ S hS = multivariateGaussian μ S' ⋯

Because multivariateGaussian carries a proof that S is positive semidefinite, rw [h] will not solve the goal below. This is what this lemma is used for.

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.hasLaw_eval_multivariateGaussian {ι : Type u_2} [Fintype ι] [DecidableEq ι] {μ : EuclideanSpace ℝ ι} {S : Matrix ι ι ℝ} {hS : S.PosSemidef} {i : ι} : HasLaw (fun (x : EuclideanSpace ℝ ι) => x i) (gaussianReal (μ i) (S i i).toNNReal) (multivariateGaussian μ S hS)

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)

def Finset.restrict₂CLM {ι : Type u_3} (R : Type u_4) {M : ι → Type u_5} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [(i : ι) → TopologicalSpace (M i)] {I J : Finset ι} (hIJ : I ⊆ J) : ((i : { x : ι // x ∈ J }) → M ↑i) →L[R] (i : { x : ι // x ∈ I }) → M ↑i

Finset.restrict₂ as a continuous linear map.

Equations

• Finset.restrict₂CLM R hIJ = { toFun := Finset.restrict₂ hIJ, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

theorem Finset.coe_restrict₂CLM {ι : Type u_3} {R : Type u_4} {M : ι → Type u_5} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [(i : ι) → TopologicalSpace (M i)] {I J : Finset ι} (hIJ : I ⊆ J) : ⇑(restrict₂CLM R hIJ) = restrict₂ hIJ

@[simp]

theorem Finset.restrict₂CLM_apply {ι : Type u_3} {R : Type u_4} {M : ι → Type u_5} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [(i : ι) → TopologicalSpace (M i)] {I J : Finset ι} (hIJ : I ⊆ J) (x : (i : { x : ι // x ∈ J }) → M ↑i) (i : { x : ι // x ∈ I }) : (restrict₂CLM R hIJ) x i = x ⟨↑i, ⋯⟩

def EuclideanSpace.restrict₂ {ι : Type u_3} {𝕜 : Type u_4} [RCLike 𝕜] {I J : Finset ι} (hIJ : I ⊆ J) : EuclideanSpace 𝕜 { x : ι // x ∈ J } →L[𝕜] EuclideanSpace 𝕜 { x : ι // x ∈ I }

The restriction from EuclideanSpace 𝕜 J to EuclideanSpace κ I when I ⊆ J.

Equations

• EuclideanSpace.restrict₂ hIJ = (↑(EuclideanSpace.equiv { x : ι // x ∈ I } 𝕜).symm).comp ((Finset.restrict₂CLM 𝕜 hIJ).comp ↑(EuclideanSpace.equiv { x : ι // x ∈ J } 𝕜))

theorem EuclideanSpace.coe_restrict₂ {ι : Type u_3} {𝕜 : Type u_4} [RCLike 𝕜] {I J : Finset ι} (hIJ : I ⊆ J) : ⇑(restrict₂ hIJ) = ⇑(restrict₂ hIJ)

@[simp]

theorem EuclideanSpace.restrict₂_apply {ι : Type u_3} {𝕜 : Type u_4} [RCLike 𝕜] {I J : Finset ι} (hIJ : I ⊆ J) (x : EuclideanSpace 𝕜 { x : ι // x ∈ J }) (i : { x : ι // x ∈ I }) : (restrict₂ hIJ) x i = x ⟨↑i, ⋯⟩

theorem ProbabilityTheory.measurePreserving_restrict_multivariateGaussian {ι : Type u_3} [DecidableEq ι] {I J : Finset ι} {μ : EuclideanSpace ℝ { x : ι // x ∈ I }} {S : Matrix { x : ι // x ∈ I } { x : ι // x ∈ I } ℝ} {hS : S.PosSemidef} (hJI : J ⊆ I) : MeasureTheory.MeasurePreserving (⇑(EuclideanSpace.restrict₂ hJI)) (multivariateGaussian μ S hS) (multivariateGaussian ((EuclideanSpace.restrict₂ hJI) μ) (S.submatrix (fun (i : { x : ι // x ∈ J }) => ⟨↑i, ⋯⟩) fun (i : { x : ι // x ∈ J }) => ⟨↑i, ⋯⟩) ⋯)

@[simp]

theorem Matrix.PosSemidef.sqrt_one {n : Type u_4} {𝕜 : Type u_5} [Fintype n] [RCLike 𝕜] [DecidableEq n] (h : PosSemidef 1) : h.sqrt = 1

theorem ProbabilityTheory.multivariateGaussian_zero_one {ι : Type u_3} [DecidableEq ι] [Fintype ι] : multivariateGaussian 0 1 ⋯ = stdGaussian (EuclideanSpace ℝ ι)