Mathlib.Probability.Distributions.Gaussian
This barrel collects finite-dimensional Gaussian-measure developments.
Standard 3 core · 6 supporting This file develops the coordinate-product representation of the standard Gaussian measure on a finite-dimensional real inner-product space. ★ stdGaussian_map_normSq_eq_pi
Standard Gaussian measures
This file develops the coordinate-product representation of the standard Gaussian measure on a finite-dimensional real inner-product space. It also identifies the law of the squared norm with the sum of squared independent one-dimensional standard Gaussians.
def piGaussian reviewed
⚑ flagged
Causalean.Mathlib
For every real normed inner-product space, the coordinate product Gaussian measure is the product of independent standard normal laws, with one real-valued coordinate for every element of the finite index set whose size is the space's real rank.
def stdGaussian reviewed
⚑ flagged
Causalean.Mathlib
The standard Gaussian measure on a finite-dimensional real inner-product space.
Definition (Lean source)
parameters
E :
def
given by
ProbabilityTheory.stdGaussian E
theorem stdGaussian_map_normSq_eq_pi reviewed
⚑ flagged
Causalean.Mathlib
Product-of-1-D-Gaussians model for the squared norm. The law of the squared norm under the standard Gaussian measure on E equals the law of the sum of squared coordinates under a product of finrank ℝ E independent standard real Gaussians.
Formal statement
Proof (Lean source)
theorem stdGaussian_map_normSq_eq_pi :
(stdGaussian E).map (fun x => ‖x‖ ^ 2)
= (Measure.pi (fun _ : Fin (finrank ℝ E) => gaussianReal 0 1)).map
(fun w => ∑ i, (w i) ^ 2) := by
rw [stdGaussian,
ProbabilityTheory.stdGaussian_eq_map_pi_orthonormalBasis (stdOrthonormalBasis ℝ E),
Measure.map_map (by fun_prop) (by fun_prop)]
refine Measure.map_congr (ae_of_all _ fun w => ?_)
simp only [Function.comp_apply]
rw [← (stdOrthonormalBasis ℝ E).equiv_apply_euclideanSpace (toLp 2 w),
LinearIsometryEquiv.norm_map, EuclideanSpace.norm_eq,
Real.sq_sqrt (Finset.sum_nonneg fun i _ => by positivity)]
refine Finset.sum_congr rfl fun i _ => ?_
rw [Real.norm_eq_abs, sq_abs]
6 supporting declarations (lemmas, instances)
-
isProbabilityMeasure_piGaussianinstance — For every real normed inner-product space, the coordinate product of independent one-dimensional standard Gaussian laws is a probability measure. -
isGaussian_piGaussianinstance — For every real normed inner-product space, the coordinate product of independent one-dimensional standard Gaussian laws is a Gaussian probability law.parametersE :sharedType u_1instancegiven byby have hIndep : iIndepFun (fun (i : Fin (finrank ℝ E)) (ω : Fin (finrank ℝ E) → ℝ) => ω i) (piGaussian E) := iIndepFun_pi (X := fun _ => (id : ℝ → ℝ)) (fun _ => aemeasurable_id) have hLaw : ∀ i, HasGaussianLaw (fun ω : Fin (finrank ℝ E) → ℝ => ω i) (piGaussian E) := by intro i classical have hmap : (piGaussian E).map (fun ω => ω i)= gaussianReal 0 1 := by unfold piGaussian rw [show (fun ω : Fin (finrank ℝ E) → ℝ => ω i) = Function.eval i from rfl, Measure.pi_map_eval] simp refine ⟨?_⟩ rw [hmap] infer_instance have hJoint : IsGaussian ((piGaussian E).map (fun ω => (fun i => ω i : Fin (finrank ℝ E) → ℝ))) := (hIndep.hasGaussianLaw hLaw).isGaussian_map simpa using hJoint -
memLp_evallemma — Each coordinate is MemLp of order 2 under the product measure.hypothesesconclusionProof (Lean source)
lemma memLp_eval (i : Fin (finrank ℝ E)) : MemLp (fun ω : Fin (finrank ℝ E) → ℝ => ω i) 2 (piGaussian E) := by have h : MemLp id 2 (gaussianReal (0 : ℝ) 1) := memLp_id_gaussianReal' 2 (by simp) exact h.comp_measurePreserving (measurePreserving_eval _ i) -
integral_id_map_equivlemma — Transporting a measure through a continuous linear equivalence transports its vector integral through the same equivalence.hypothesesF G :L :F ≃L[ℝ] Gconclusion∫ x, x ∂(μ.map L) = L (∫ x, x ∂μ)Proof (Lean source)
lemma integral_id_map_equiv {F G : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace F] [BorelSpace F] [NormedAddCommGroup G] [NormedSpace ℝ G] [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology G] {μ : Measure F} (L : F ≃L[ℝ] G) : ∫ x, x ∂(μ.map L) = L (∫ x, x ∂μ) := by rw [integral_map (φ := L) (f := fun x => x) (by fun_prop) (aestronglyMeasurable_id.congr (by rfl))] exact L.integral_comp_comm (fun x => x) -
isProbabilityMeasure_stdGaussianinstance — The standard Gaussian measure is a probability measure.parametersE :sharedType u_1instancegiven byby change IsProbabilityMeasure (ProbabilityTheory.stdGaussian E) infer_instance -
isGaussian_stdGaussianinstance — The standard Gaussian measure is Gaussian.parametersE :sharedType u_1instancegiven byby change IsGaussian (ProbabilityTheory.stdGaussian E) infer_instance