Samplinglib mathematical lesson

A signed Gaussian expectation

Read this first

Mathematical statement

For \(n\ge3\), \(\kappa\ge4\) and \(\ell\ge0\), the bounded radial Gaussian test has absolutely integrable expectations. Its signed Haar average is computed below.

\[\begin{aligned}H_\gamma(\ell)&=\mathbb E_{O\sim\mu}\!\left[\det(O)\int t_\ell\,d\gamma_O\right]\\&=c_{n,\kappa}\,\mathbb E_{O\sim\mu}\!\left[\frac{(\sqrt\kappa+1)U-(\sqrt\kappa-1)}{a_\ell(O)^{n/2}}\right],\\c_{n,\kappa}&=\frac{(-1)^{n-1}(\sqrt\kappa-1)^{n-1}}{2^{n/2}},\\a_\ell(O)&=\kappa+1+4\ell-(\kappa-1)U.\end{aligned}\]

Lean statement · actual_gaussian_transform

Unchanged preproof exact signature, literal p/t/U/a and actual gamma/Haar, pointwise and outer L1, exact Eq21.

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 actual_gaussian_transform {n : ℕ} (hn : 3 ≤ n) {κ : ℝ}
    (hκ : 4 ≤ κ) {ℓ : ℝ} (hℓ : 0 ≤ ℓ) :
    let j0 : Fin n := ⟨0, lt_of_lt_of_le (by decide : 0 < 3) hn⟩
    let U : Matrix.orthogonalGroup (Fin n) ℝ → ℝ :=
      fun O => (O : Matrix (Fin n) (Fin n) ℝ) j0 j0
    let a : Matrix.orthogonalGroup (Fin n) ℝ → ℝ :=
      fun O => κ + 1 + 4 * ℓ - (κ - 1) * U O
    let p : Matrix.orthogonalGroup (Fin n) ℝ → EuclideanSpace ℝ (Fin n) → ℝ :=
      fun O x => Real.sqrt (singleBlockPrecision κ O).det /
        (2 * Real.pi) ^ ((n : ℝ) / 2) *
          Real.exp (-((WithLp.ofLp x) ⬝ᵥ
            (singleBlockPrecision κ O *ᵥ WithLp.ofLp x)) / 2)
    let t : EuclideanSpace ℝ (Fin n) → ℝ := fun x => Real.exp (-ℓ * ‖x‖ ^ 2)
    let γ : Matrix.orthogonalGroup (Fin n) ℝ → Measure (EuclideanSpace ℝ (Fin n)) :=
      fun O => ProbabilityTheory.multivariateGaussian (0 : EuclideanSpace ℝ (Fin n))
        (singleBlockPrecision κ O)⁻¹
    (∀ O, Integrable t (γ O) ∧ Integrable (fun x => t x * p O x) volume ∧
      (∫ x, t x ∂γ O) = ∫ x, t x * p O x) ∧
    Integrable (fun O : Matrix.orthogonalGroup (Fin n) ℝ =>
      (O : Matrix (Fin n) (Fin n) ℝ).det * (∫ x, t x ∂γ O)) (orthogonalHaar n) ∧
    (∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
      (O : Matrix (Fin n) (Fin n) ℝ).det * (∫ x, t x ∂γ O) ∂orthogonalHaar n) =
      ((-1 : ℝ) ^ (n - 1) * (Real.sqrt κ - 1) ^ (n - 1) /
        (2 : ℝ) ^ ((n : ℝ) / 2)) *
        (∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
          ((Real.sqrt κ + 1) * U O - (Real.sqrt κ - 1)) /
            (a O) ^ ((n : ℝ) / 2) ∂orthogonalHaar n)

Exact module and namespace context

Conditioned target mixtures and total-variation bounds remain separate open steps.

Full assumptions and notation

All objects and hypotheses

Exactly \(n\ge3\), \(\kappa\ge4\) and \(\ell\ge0\); the endpoint \(\ell=0\) is included.
\(O\) ranges over the full real orthogonal group, with its normalized Borel Haar probability \(\mu\), including both determinant signs.
\(\gamma_O=\mathcal N(0,A_O^{-1})\) is the canonical Gaussian measure; \(dx\) is Euclidean volume and \(\|x\|_2\) is the true Euclidean norm.
The proof establishes \(t_\ell\in L^1(\gamma_O)\), \(t_\ell p_O\in L^1(dx)\), and \(\int t_\ell\,d\gamma_O=\int t_\ell p_O\,dx\) for every \(O\). It also proves absolute Haar integrability of \(O\mapsto\det(O)\int t_\ell\,d\gamma_O\). These are conclusions, with no extra integrability premise.
Dimension-half powers use real division. Positivity, density measurability and the law-to-density identity are proved internally.

Notation and interpretation

\(A_O\): The literal single-block precision.
\[A_O=\frac{\kappa+1}{2}I_n-\frac{\kappa-1}{4}(O+O^\top)\]
\(\gamma_O\) and \(p_O\): The actual Gaussian law and its density relative to Euclidean volume.
\[\begin{aligned}\gamma_O&=\mathcal N(0,A_O^{-1}),\\p_O(x)&=\frac{\sqrt{\det A_O}}{(2\pi)^{n/2}}\exp\!\left(-\frac{x^\top A_Ox}{2}\right).\end{aligned}\]
\(t_\ell\) and \(U\): The bounded radial test and the first matrix entry.
\[t_\ell(x)=e^{-\ell\|x\|_2^2},\qquad U=O_{11},\qquad 0<t_\ell\le1\]
\(H_\gamma\): The determinant-weighted expectation, under the same full Haar probability.
\[H_\gamma(\ell)=\int_{O(n)}\det(O)\!\left(\int_{\mathbb R^n}t_\ell(x)\,d\gamma_O(x)\right)d\mu(O)\]

Mathematical proof

Open a step to read its argument and formula.

1. Bound the test

Continuity and \(0<t_\ell\le1\) give absolute integrability under every Gaussian probability measure. This also covers \(\ell=0\).

\[0<e^{-\ell\|x\|_2^2}\leq1,\qquad t\in L^1(\gamma_O)\]

Corresponding Lean step

The proof uses actual multivariateGaussian probability, continuity and an explicit norm bound; Gaussian test integrability is produced internally.

2. Identify the density

The existing density theorem identifies the actual law \(\gamma_O\) with the nonnegative, measurable density \(p_O\) relative to Euclidean volume. All source conditions are unchanged.

\[\gamma_O=dx\,p_O,\qquad p_O\geq0\]

Corresponding Lean step

The proof actually calls GaussianLawDensity.gaussian_law_eq_density hn hκ O. Positivity and measurability are verified for the unchanged explicit p_O; no substitute Gaussian constructor is introduced.

3. Transport the integral

Transport absolute integrability and the expectation through that density identity. Both spatial integrals below are absolutely integrable.

\[tp_O\in L^1(dx),\qquad\int t\,d\gamma_O=\int t(x)p_O(x)\,dx\]

Corresponding Lean step

The proof uses integrable_withDensity_iff and integral_withDensity_eq_integral_toReal_smul, with internal measurable/finite/nonnegative density proofs. ENNReal.ofReal and multiplication order are simplified exactly.

4. Control the outer expectation

The compiled Fubini result gives joint integrability under \(\mu\otimes dx\). Integrating the spatial variable and using the pointwise identity gives absolute Haar integrability of the signed expectation.

\[\det(O)t(x)p_O(x)\in L^1(\mu\otimes dx)\Longrightarrow \det(O)\int t\,d\gamma_O\in L^1(\mu)\]

Corresponding Lean step

The proof consumes the exact literal_mixture_transform joint-L1 conclusion and actual Integrable.integral_prod_left, then pointwise congruence and integral_const_mul. No unproved family-measurability premise is supplied.

5. Apply the evaluated transform

The pointwise density identity turns \(H_\gamma\) into the literal transform \(H_{\mathrm{lit}}\). Apply its already evaluated formula. The relation to conditioned mixtures and total variation is a later step.

\[H_\gamma(\ell)=H_{\mathrm{lit}}(\ell)=\frac{(-1)^{n-1}(\sqrt\kappa-1)^{n-1}}{2^{n/2}}\mathbb E\!\left[\frac{(\sqrt\kappa+1)U-(\sqrt\kappa-1)}{[\kappa+1+4\ell-(\kappa-1)U]^{n/2}}\right]\]

Corresponding Lean step

The final composition uses the same pointwise expectation transport and exact equality projection of MixtureFubini.literal_mixture_transform hn hκ hℓ. No Gaussian/B6/Fubini proof is copied, and no TV or Poisson conclusion is asserted.

Lean verification

Lean proof · actual_gaussian_transform

Internal bounded-test L1 and actual withDensity transport compose the exact law-density and literal Fubini parents.

Download module (.lean)

theorem actual_gaussian_transform {n : ℕ} (hn : 3 ≤ n) {κ : ℝ}
    (hκ : 4 ≤ κ) {ℓ : ℝ} (hℓ : 0 ≤ ℓ) :
    let j0 : Fin n := ⟨0, lt_of_lt_of_le (by decide : 0 < 3) hn⟩
    let U : Matrix.orthogonalGroup (Fin n) ℝ → ℝ :=
      fun O => (O : Matrix (Fin n) (Fin n) ℝ) j0 j0
    let a : Matrix.orthogonalGroup (Fin n) ℝ → ℝ :=
      fun O => κ + 1 + 4 * ℓ - (κ - 1) * U O
    let p : Matrix.orthogonalGroup (Fin n) ℝ → EuclideanSpace ℝ (Fin n) → ℝ :=
      fun O x => Real.sqrt (singleBlockPrecision κ O).det /
        (2 * Real.pi) ^ ((n : ℝ) / 2) *
          Real.exp (-((WithLp.ofLp x) ⬝ᵥ
            (singleBlockPrecision κ O *ᵥ WithLp.ofLp x)) / 2)
    let t : EuclideanSpace ℝ (Fin n) → ℝ := fun x => Real.exp (-ℓ * ‖x‖ ^ 2)
    let γ : Matrix.orthogonalGroup (Fin n) ℝ → Measure (EuclideanSpace ℝ (Fin n)) :=
      fun O => ProbabilityTheory.multivariateGaussian (0 : EuclideanSpace ℝ (Fin n))
        (singleBlockPrecision κ O)⁻¹
    (∀ O, Integrable t (γ O) ∧ Integrable (fun x => t x * p O x) volume ∧
      (∫ x, t x ∂γ O) = ∫ x, t x * p O x) ∧
    Integrable (fun O : Matrix.orthogonalGroup (Fin n) ℝ =>
      (O : Matrix (Fin n) (Fin n) ℝ).det * (∫ x, t x ∂γ O)) (orthogonalHaar n) ∧
    (∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
      (O : Matrix (Fin n) (Fin n) ℝ).det * (∫ x, t x ∂γ O) ∂orthogonalHaar n) =
      ((-1 : ℝ) ^ (n - 1) * (Real.sqrt κ - 1) ^ (n - 1) /
        (2 : ℝ) ^ ((n : ℝ) / 2)) *
        (∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
          ((Real.sqrt κ + 1) * U O - (Real.sqrt κ - 1)) /
            (a O) ^ ((n : ℝ) / 2) ∂orthogonalHaar n) := by
  classical
  let j0 : Fin n := ⟨0, lt_of_lt_of_le (by decide : 0 < 3) hn⟩
  let U : Matrix.orthogonalGroup (Fin n) ℝ → ℝ :=
    fun O => (O : Matrix (Fin n) (Fin n) ℝ) j0 j0
  let a : Matrix.orthogonalGroup (Fin n) ℝ → ℝ :=
    fun O => κ + 1 + 4 * ℓ - (κ - 1) * U O
  let p : Matrix.orthogonalGroup (Fin n) ℝ → EuclideanSpace ℝ (Fin n) → ℝ :=
    fun O x => Real.sqrt (singleBlockPrecision κ O).det /
      (2 * Real.pi) ^ ((n : ℝ) / 2) *
        Real.exp (-((WithLp.ofLp x) ⬝ᵥ
          (singleBlockPrecision κ O *ᵥ WithLp.ofLp x)) / 2)
  let t : EuclideanSpace ℝ (Fin n) → ℝ := fun x => Real.exp (-ℓ * ‖x‖ ^ 2)
  let γ : Matrix.orthogonalGroup (Fin n) ℝ → Measure (EuclideanSpace ℝ (Fin n)) :=
    fun O => multivariateGaussian (0 : EuclideanSpace ℝ (Fin n))
      (singleBlockPrecision κ O)⁻¹
  have htcont : Continuous t := by dsimp [t]; fun_prop
  have htbound (x : EuclideanSpace ℝ (Fin n)) : ‖t x‖ ≤ 1 := by
    dsimp [t]
    rw [abs_of_pos (Real.exp_pos _)]
    apply Real.exp_le_one_iff.mpr
    exact mul_nonpos_of_nonpos_of_nonneg (neg_nonpos.mpr hℓ) (sq_nonneg _)
  have hp0 (O : Matrix.orthogonalGroup (Fin n) ℝ) (x : EuclideanSpace ℝ (Fin n)) :
      0 ≤ p O x := by dsimp [p]; positivity
  have hpmeas (O : Matrix.orthogonalGroup (Fin n) ℝ) :
      Measurable (fun x => ENNReal.ofReal (p O x)) := by dsimp [p]; fun_prop
  have hfinite (O : Matrix.orthogonalGroup (Fin n) ℝ) :
      ∀ᵐ x ∂(volume : Measure (EuclideanSpace ℝ (Fin n))),
        ENNReal.ofReal (p O x) < ⊤ := Filter.Eventually.of_forall fun _ => ENNReal.ofReal_lt_top
  have hpoint (O : Matrix.orthogonalGroup (Fin n) ℝ) :
      Integrable t (γ O) ∧ Integrable (fun x => t x * p O x) volume ∧
        (∫ x, t x ∂γ O) = ∫ x, t x * p O x := by
    let : IsProbabilityMeasure (γ O) := by dsimp [γ]; infer_instance
    have htL : Integrable t (γ O) :=
      (integrable_const (1 : ℝ)).mono' htcont.aestronglyMeasurable
        (Filter.Eventually.of_forall htbound)
    have hd : γ O = volume.withDensity (fun x => ENNReal.ofReal (p O x)) :=
      gaussian_law_eq_density hn hκ O
    have htd : Integrable t (volume.withDensity (fun x => ENNReal.ofReal (p O x))) := by
      rw [← hd]
      exact htL
    have hw := (integrable_withDensity_iff (hpmeas O) (hfinite O)).mp htd
    have hw' : Integrable (fun x => t x * p O x) volume := by
      simpa only [ENNReal.toReal_ofReal (hp0 O _)] using hw
    refine ⟨htL, hw', ?_⟩
    rw [hd, integral_withDensity_eq_integral_toReal_smul (hpmeas O) (hfinite O)]
    apply integral_congr_ae
    exact Filter.Eventually.of_forall fun x => by
      change (ENNReal.ofReal (p O x)).toReal * t x = t x * p O x
      rw [ENNReal.toReal_ofReal (hp0 O x), mul_comm]
  have hlit := literal_mixture_transform hn hκ hℓ
  have hjoint : Integrable
      (fun z : Matrix.orthogonalGroup (Fin n) ℝ × EuclideanSpace ℝ (Fin n) =>
        (z.1 : Matrix (Fin n) (Fin n) ℝ).det * (t z.2 * p z.1 z.2))
      ((orthogonalHaar n).prod volume) := hlit.1
  have houter : Integrable (fun O : Matrix.orthogonalGroup (Fin n) ℝ =>
      (O : Matrix (Fin n) (Fin n) ℝ).det * (∫ x, t x ∂γ O)) (orthogonalHaar n) := by
    have hi := hjoint.integral_prod_left
    apply hi.congr
    exact Filter.Eventually.of_forall fun O => by
      change (∫ x, (O : Matrix (Fin n) (Fin n) ℝ).det * (t x * p O x)) =
        (O : Matrix (Fin n) (Fin n) ℝ).det * (∫ x, t x ∂γ O)
      rw [integral_const_mul, (hpoint O).2.2]
  refine ⟨hpoint, houter, ?_⟩
  calc
    _ = (∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
        (O : Matrix (Fin n) (Fin n) ℝ).det * (∫ x, t x * p O x)
          ∂orthogonalHaar n) := by
      apply integral_congr_ae
      exact Filter.Eventually.of_forall fun O => by
        change (O : Matrix (Fin n) (Fin n) ℝ).det * (∫ x, t x ∂γ O) =
          (O : Matrix (Fin n) (Fin n) ℝ).det * (∫ x, t x * p O x)
        rw [(hpoint O).2.2]
    _ = _ := hlit.2.2

end AutoSamplingTheory.ExampleCases.GaussianComplexity.GaussianExpectation

Exact module and namespace context

Scope and omitted-condition boundaries

Actual pointwise Gaussian test/weighted-density L1 and transport, genuine signed outer Haar L1 and exact actual Gaussian H through Eq21. Determinant-conditioned target-mixture construction/half-mass, Ex57/Eq20 H-to-TV, sphere/Poisson, parameter choice, amplification/transcript/eigenbasis and both main lower bounds remain open. Sharp Ex59 and B6 minor/path estimates retain unchanged disclosed parent boundaries. No sign-to-eigenbasis lower-bound implication.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

ProbabilityTheory.multivariateGaussian
integrable_const
Integrable.mono'
integrable_withDensity_iff
integral_withDensity_eq_integral_toReal_smul
Integrable.integral_prod_left
integral_const_mul
ENNReal.toReal_ofReal

Mathematical sources

Actual Gaussian expectation interpretation through Eq21 — Actual Gaussian signed test expectation; target-mixture/TV interpretation separate.

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