The squared norm of a standard Gaussian has mean d
AutoSamplingTheory.TechnicalLemmas.Probability.StdGaussianMoment.integrable_norm_sq_and_integral_stdGaussian · theorem · Teaching coverage
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.
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.
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 ℝ EProof roadmap
- 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.
- 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.
- 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.
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.
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.
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.
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.StdGaussianMomentSource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| Mathlib exposes standard-Gaussian mean, covariance and L2 facts separately. | ASTIS combines them with a finite orthonormal basis to return squared-norm integrability and its exact integral. | same | This is a finite-dimensional consequence of the cited formal APIs, not a strengthened probability claim. |
Only the standard-Gaussian squared-norm L1 identity; no independent product law, OU update, higher moment or sampler theorem.
Encoder–denoiser: source-reviewed · equivalent-after-elaboration
Detected semantic differences
- domains: Completeness and Borel structure required by the formal Gaussian API are explicit. — Independent source review classification: explicit-elaboration; nonblocking.
- constant_dependencies: Dimension is resolved as Module.finrank ℝ E and expectation as integration against stdGaussian E. — Independent source review classification: explicit-elaboration; nonblocking.
A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.
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
- Mathlib multivariate Gaussian covariance API — Formal upstream for L2 integrability, covariance and mean zero; ASTIS supplies the finite-basis norm-square packaging.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.