The standard Gaussian measure on a finite product

The product measure γ^ι = Measure.pi (fun _ : ι => gaussianReal 0 1) is Lebesgue measure on ℝ^ι weighted by the joint density x ↦ ∏ i, gaussianPDFReal 0 1 (x i). That identification is what lets a weight-in-the-measure statement about γ^ι be read as a weight-in-the-function statement about volume^ι, via TauCeti.weightL2Isometry.

Like TauCeti.Probability.gaussianPDFReal_zero_one, these are statements about the Gaussian distribution alone (no orthogonal family appears), so they live here rather than with the multi-index Hermite basis that consumes them.

Main statements

• TauCeti.Probability.prod_gaussianPDFReal_zero_one: the joint density in closed form, (2π)^(-d/2) · e^{-∑ᵢ xᵢ²/2}, where d is the number of coordinates.
• TauCeti.Probability.pi_gaussianReal_eq_withDensity: γ^ι = volume^ι weighted by the joint density.
• TauCeti.Probability.pi_volume_absolutelyContinuous_pi_gaussianReal: the joint density never vanishes, so volume^ι-null sets are exactly γ^ι-null sets in the direction one needs to move an almost-everywhere statement from γ^ι to volume^ι.

theorem TauCeti.Probability.prod_gaussianPDFReal_pos (ι : Type u_1) [Fintype ι] (x : ι → ℝ) : 0 < ∏ i : ι, ProbabilityTheory.gaussianPDFReal 0 1 (x i)

The joint standard Gaussian density on ℝ^ι is everywhere positive.

theorem TauCeti.Probability.prod_gaussianPDFReal_zero_one (ι : Type u_1) [Fintype ι] (x : ι → ℝ) : ∏ i : ι, ProbabilityTheory.gaussianPDFReal 0 1 (x i) = (2 * Real.pi) ^ (-↑(Fintype.card ι) / 2) * Real.exp ((-∑ i : ι, x i ^ 2) / 2)

The joint standard Gaussian density on ℝ^ι in closed form: the normalisation (2π)^(-d/2) in the dimension d, times the exponential of minus half the sum of the squared coordinates.

theorem TauCeti.Probability.measurable_prod_gaussianPDFReal (ι : Type u_1) [Fintype ι] : Measurable fun (x : ι → ℝ) => ∏ i : ι, ProbabilityTheory.gaussianPDFReal 0 1 (x i)

The joint standard Gaussian density on ℝ^ι is measurable.

theorem TauCeti.Probability.pi_gaussianReal_eq_withDensity (ι : Type u_1) [Fintype ι] : (MeasureTheory.Measure.pi fun (x : ι) => ProbabilityTheory.gaussianReal 0 1) = (MeasureTheory.Measure.pi fun (x : ι) => MeasureTheory.volume).withDensity fun (x : ι → ℝ) => ENNReal.ofReal (∏ i : ι, ProbabilityTheory.gaussianPDFReal 0 1 (x i))

The standard Gaussian on ℝ^ι is volume^ι weighted by the joint density. Each factor is volume weighted by gaussianPDFReal 0 1 (ProbabilityTheory.gaussianReal_of_var_ne_zero), and coordinatewise densities multiply (TauCeti.pi_withDensity).

theorem TauCeti.Probability.pi_volume_absolutelyContinuous_pi_gaussianReal (ι : Type u_1) [Fintype ι] : (MeasureTheory.Measure.pi fun (x : ι) => MeasureTheory.volume).AbsolutelyContinuous (MeasureTheory.Measure.pi fun (x : ι) => ProbabilityTheory.gaussianReal 0 1)

volume^ι is absolutely continuous with respect to γ^ι. The joint density is everywhere positive, so weighting by it kills no set of positive measure. This is what moves an almost-everywhere identification of a L²(γ^ι) representative to one holding volume^ι-almost everywhere, where the √-density envelope lives.