Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0

StdGaussianMoment: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

  1. The squared norm of a standard Gaussian has mean d
Samplinglib mathematical lesson

The squared norm of a standard Gaussian has mean d

AutoSamplingTheory.TechnicalLemmas.Probability.StdGaussianMoment.integrable_norm_sq_and_integral_stdGaussian · theorem · Teaching coverage

Read this first

Mathematical statement

If Z is standard Gaussian in E, then its squared norm is Bochner-integrable and its expectation is the real dimension of E.

\[\mathbb E\|Z\|^2=\dim_{\mathbb R}E.\]
Lean statement · integrable_norm_sq_and_integral_stdGaussian

The declaration returns integrability and the exact integral in one reusable interface, because downstream product-measure calculations need both facts.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)
theorem integrable_norm_sq_and_integral_stdGaussian
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [CompleteSpace E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] :
    Integrable (fun x : E => ‖x‖ ^ 2) (stdGaussian E) ∧
      (∫ x : E, ‖x‖ ^ 2 ∂stdGaussian E) = Module.finrank ℝ E

Exact module and namespace context

Proof roadmap

  1. 1Obtain genuine L2 integrability

    Mathlib proves that the identity random variable belongs to L2 under the standard Gaussian law. The L2-to-integrable-square equivalence therefore gives integrability of the squared norm before any coordinate sum is exchanged with the integral.

  2. 2Compute every directional variance

    For an orthonormal basis vector e_i, the covariance identity and zero Gaussian mean give E<e_i,Z>²=1. Each scalar square is dominated by ‖Z‖², so it is integrable.

  3. 3Apply finite-dimensional Parseval

    Parseval writes the squared norm as the finite sum of directional squares. Since every summand is integrable, the integral commutes with the finite sum and each term contributes one.

Full assumptions and notation

All objects and hypotheses

  • E is a complete finite-dimensional real inner-product space with its Borel sigma algebra.
  • The probability law is Mathlib's actual standard Gaussian stdGaussian E; no abstract covariance hypothesis replaces it.

Mathematical proof

1. Obtain genuine L2 integrability

Mathlib proves that the identity random variable belongs to L2 under the standard Gaussian law. The L2-to-integrable-square equivalence therefore gives integrability of the squared norm before any coordinate sum is exchanged with the integral.

\[Z\in L^2(\gamma_E)\quad\Longrightarrow\quad \|Z\|^2\in L^1(\gamma_E).\]
Corresponding Lean step

IsGaussian.memLp_two_id and memLp_two_iff_integrable_sq_norm produce hi.

2. Compute every directional variance

For an orthonormal basis vector e_i, the covariance identity and zero Gaussian mean give E<e_i,Z>²=1. Each scalar square is dominated by ‖Z‖², so it is integrable.

\[\mathbb E\langle e_i,Z\rangle^2=1,\qquad |\langle e_i,Z\rangle|^2\le\|Z\|^2.\]
Corresponding Lean step

covarianceBilin_apply, covarianceBilin_stdGaussian and integral_id_stdGaussian prove hdir; norm_inner_le_norm supplies hL1.

3. Apply finite-dimensional Parseval

Parseval writes the squared norm as the finite sum of directional squares. Since every summand is integrable, the integral commutes with the finite sum and each term contributes one.

\[\mathbb E\|Z\|^2=\sum_{i=1}^{d}\mathbb E\langle e_i,Z\rangle^2=\sum_{i=1}^{d}1=d.\]
Corresponding Lean step

stdOrthonormalBasis.sum_sq_norm_inner_right and integral_finsetSum close the calculation.

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · integrable_norm_sq_and_integral_stdGaussian

ASTIS packages existing Mathlib Gaussian L2/covariance facts through finite-dimensional Parseval; it introduces no new axiom or source-specific assumption.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)
theorem integrable_norm_sq_and_integral_stdGaussian
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [CompleteSpace E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] :
    Integrable (fun x : E => ‖x‖ ^ 2) (stdGaussian E) ∧
      (∫ x : E, ‖x‖ ^ 2 ∂stdGaussian E) = Module.finrank ℝ E := by
  classical
  have hi : Integrable (fun x : E => ‖x‖ ^ 2) (stdGaussian E) :=
    (memLp_two_iff_integrable_sq_norm (by fun_prop)).1 IsGaussian.memLp_two_id
  let b := stdOrthonormalBasis ℝ E
  have hdir (i) : (∫ x : E, (inner ℝ (b i) x) ^ 2 ∂stdGaussian E) = 1 := by
    have hh := covarianceBilin_apply (μ := stdGaussian E)
      IsGaussian.memLp_two_id (b i) (b i)
    rw [covarianceBilin_stdGaussian] at hh
    change inner ℝ (b i) (b i) = _ at hh
    simpa [integral_id_stdGaussian, real_inner_self_eq_norm_sq,
      b.orthonormal.norm_eq_one, pow_two] using hh.symm
  have hL1 (i) : Integrable (fun x : E => (inner ℝ (b i) x) ^ 2)
      (stdGaussian E) := by
    apply hi.mono' (by fun_prop)
    filter_upwards with x
    rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)]
    have hb := norm_inner_le_norm (𝕜 := ℝ) (b i) x
    rw [b.orthonormal.norm_eq_one, one_mul] at hb
    have hsq := (sq_le_sq₀ (norm_nonneg (inner ℝ (b i) x)) (norm_nonneg x)).2 hb
    simpa [Real.norm_eq_abs, sq_abs] using hsq
  refine ⟨hi, ?_⟩
  calc
    (∫ x : E, ‖x‖ ^ 2 ∂stdGaussian E) =
        ∫ x : E, ∑ i, (inner ℝ (b i) x) ^ 2 ∂stdGaussian E := by
      apply integral_congr_ae
      filter_upwards with x
      simpa [Real.norm_eq_abs, sq_abs] using (b.sum_sq_norm_inner_right x).symm
    _ = ∑ i, ∫ x : E, (inner ℝ (b i) x) ^ 2 ∂stdGaussian E :=
      integral_finsetSum _ (fun i _ => hL1 i)
    _ = Module.finrank ℝ E := by simp [hdir]

end AutoSamplingTheory.TechnicalLemmas.Probability.StdGaussianMoment

Exact module and namespace context

Scope and omitted-condition boundaries
  • A reusable finite-dimensional standard-Gaussian second-moment identity. It does not assert independence, construct an OU refresh, give higher moments, or prove a sampling result.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

    Mathlib API called (external library)

    • ProbabilityTheory.IsGaussian.memLp_two_id
    • ProbabilityTheory.covarianceBilin_apply
    • ProbabilityTheory.covarianceBilin_stdGaussian
    • InnerProductSpace.stdOrthonormalBasis
    • MeasureTheory.integral_finsetSum

    Mathematical sources

    Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.