Expectations of the Gaussian mixtures

Huanjian Zhou and Taiji Suzuki, On Complexity of Gaussian Sampling. The source half-mass identity is made explicit on the actual mixture measures; omitted integration bookkeeping is supplied background. Source H uses the existing component density representation; this statement uses its actual Gaussian expectation representation.

Read the formalized proofs

Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.

Samplinglib mathematical lesson

Expectations of the Gaussian mixtures

Read this first

Mathematical statement

For \(n\ge3\), \(\kappa\ge4\) and \(\ell\ge0\), the radial test is integrable under both actual Gaussian mixtures. Their expectations are the corresponding component averages, and their difference is twice the signed Haar average.

\[\mathbb E_{P_+}t-\mathbb E_{P_-}t=2\int_{O(n)}\det(O)\,f(O)\,d\mu(O).\]

Lean statement · actual_mixture_expectation_gap

Exact sealed actual-law target: both mixture L1, both prior L1, both actual real expectation transports and exact2 signed Haar gap; all producer results internal.

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_mixture_expectation_gap {n : ℕ} (hn : 3 ≤ n) {κ : ℝ}
    (hκ : 4 ≤ κ) {ℓ : ℝ} (hℓ : 0 ≤ ℓ) :
    let μ := orthogonalHaar n
    let νpos := (2 : ℝ≥0∞) • μ.restrict
      {O : Matrix.orthogonalGroup (Fin n) ℝ | (O : Matrix (Fin n) (Fin n) ℝ).det = 1}
    let νneg := (2 : ℝ≥0∞) • μ.restrict
      {O : Matrix.orthogonalGroup (Fin n) ℝ | (O : Matrix (Fin n) (Fin n) ℝ).det = -1}
    let γ : Matrix.orthogonalGroup (Fin n) ℝ → Measure (EuclideanSpace ℝ (Fin n)) :=
      fun O => multivariateGaussian (0 : EuclideanSpace ℝ (Fin n))
        (singleBlockPrecision κ O)⁻¹
    let t : EuclideanSpace ℝ (Fin n) → ℝ := fun x => Real.exp (-ℓ * ‖x‖ ^ 2)
    let f : Matrix.orthogonalGroup (Fin n) ℝ → ℝ := fun O => ∫ x, t x ∂γ O
    Integrable t (νpos.bind γ) ∧ Integrable t (νneg.bind γ) ∧
      Integrable f νpos ∧ Integrable f νneg ∧
      (∫ x, t x ∂νpos.bind γ) = (∫ O, f O ∂νpos) ∧
      (∫ x, t x ∂νneg.bind γ) = (∫ O, f O ∂νneg) ∧
      ((∫ x, t x ∂νpos.bind γ) - (∫ x, t x ∂νneg.bind γ)) =
        2 * (∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
          (O : Matrix (Fin n) (Fin n) ℝ).det * f O ∂μ)

Exact module and namespace context

The TV inequality and the main query lower bounds remain open.

Full assumptions and notation

All objects and hypotheses

Exactly \(n\ge3\), \(\kappa\ge4\), \(\ell\ge0\), including \(\ell=0\). No integrability or measurable-family premise is supplied.
\(\mu\) is normalized Borel Haar on full real \(O(n)\); \(\nu_\pm=2\mu|_{\{\det O=\pm1\}}\). Both are the actual prior measures.
\(\gamma_O=\mathcal N(0,A_O^{-1})\), \(P_\pm=\nu_\pm\mathbin{\mathrm{bind}}\gamma\), and all expectations are real Bochner integrals on actual Borel Euclidean space.
The source defines \(H\) with component densities. Its actual Gaussian representation is supplied by the existing law-density/expectation interfaces. This packet proves the actual mixture expectation identity, while the quantitative Eq21 evaluation and TV inequality remain separate.

Notation and interpretation

\(A_O\): Literal source precision.
\[A_O=\frac{\kappa+1}{2}I_n-\frac{\kappa-1}{4}(O+O^\top)\]
\(t\) and \(f\): Radial test and actual component Gaussian expectation.
\[t(x)=e^{-\ell\|x\|^2},\qquad f(O)=\int t(x)\,d\gamma_O(x)\]
\(P_\pm\): Actual mixtures and their real expectation transports.
\[P_\pm=\int\gamma_O\,d\nu_\pm(O),\qquad\mathbb E_{P_\pm}t=\int f(O)\,d\nu_\pm(O)\]

Mathematical proof

Open a step to read its argument and formula.

1. Use the actual probability laws

The identical mixture-law theorem supplies the measurable actual Gaussian family and both actual mixture probabilities. The identical sign-prior theorem supplies both prior probabilities.

\[\gamma_O=\mathcal N(0,A_O^{-1}),\quad P_\pm=\nu_\pm\mathbin{\mathrm{bind}}\gamma\in\mathcal P(\mathbb R^n)\]

Corresponding Lean step

actual_mixture_laws hn hκ gives hγ and exact bind probability instances; component_probabilities internally uses n>0 derived from hn. No law or producer is a public premise.

2. Bound the radial test

Nonnegative tilt makes the continuous test lie between zero and one. Every actual probability law therefore integrates it absolutely, including both mixtures and every component Gaussian.

\[0<t(x)=e^{-\ell\|x\|^2}\le1,\qquad\int|t|\,dP_\pm\le1\]

Corresponding Lean step

htc, htnn and htb are internal; htL uses domination by integrable constant1. The same argument includes ell=0.

3. Make the component expectation measurable and integrable

The nonnegative component integral is measurable as a function of its actual measure. Its bound by one makes it finite; taking its real value gives the actual Bochner component expectation, which is bounded by one under either prior.

\[q(O)=\int t\,d\gamma_O\in[0,1],\qquad f(O)=q(O)\ \text{as a real value}\]

Corresponding Lean step

hqm composes Measure.measurable_lintegral with hγ; hqle/hqfin prove finite ENNReal integrals; hfq uses integral_eq_lintegral_of_nonneg_ae. hfm/hfb/hfL produce real measurability, boundedness and actual prior L1 internally.

4. Transport through each actual mixture

Apply the nonnegative integral formula for the actual bind. The already proved finiteness permits the conversion back to real Bochner integrals on both sides.

\[\int t\,dP_\pm=\int_{O(n)}\left(\int t\,d\gamma_O\right)d\nu_\pm(O)\]

Corresponding Lean step

htrans calls Measure.lintegral_bind with the explicit measurable nonnegative test and integral_toReal with hqfin. No unproved Bochner bind-interchange theorem or caller integrability assumption is used.

5. Split the determinant signs

An orthogonal matrix has determinant plus or minus one. Its signed expectation is the positive restricted integral minus the negative restricted integral. Each normalized prior multiplies its restriction by two, giving the displayed gap.

\[\begin{aligned}\int\det(O)f(O)\,d\mu&=\int_{C_+}f\,d\mu-\int_{C_-}f\,d\mu,\\\mathbb E_{P_+}t-\mathbb E_{P_-}t&=2\int\det(O)f(O)\,d\mu.\end{aligned}\]

Corresponding Lean step

hpos/hneg prove Borel sign events; hsign derives the determinant dichotomy from actual orthogonality. hsplit integrates the exact difference of indicators using hfL, and hipos/hineg use literal integral_smul_measure. Ring algebra closes factor2 and its sign; TV is not concluded.

Lean verification

Lean proof · actual_mixture_expectation_gap

Actual measurable probability laws, bounded radial test, finite nonnegative bind integration and exact sign-restriction algebra prove the real expectation gap.

Download module (.lean)

theorem actual_mixture_expectation_gap {n : ℕ} (hn : 3 ≤ n) {κ : ℝ}
    (hκ : 4 ≤ κ) {ℓ : ℝ} (hℓ : 0 ≤ ℓ) :
    let μ := orthogonalHaar n
    let νpos := (2 : ℝ≥0∞) • μ.restrict
      {O : Matrix.orthogonalGroup (Fin n) ℝ | (O : Matrix (Fin n) (Fin n) ℝ).det = 1}
    let νneg := (2 : ℝ≥0∞) • μ.restrict
      {O : Matrix.orthogonalGroup (Fin n) ℝ | (O : Matrix (Fin n) (Fin n) ℝ).det = -1}
    let γ : Matrix.orthogonalGroup (Fin n) ℝ → Measure (EuclideanSpace ℝ (Fin n)) :=
      fun O => multivariateGaussian (0 : EuclideanSpace ℝ (Fin n))
        (singleBlockPrecision κ O)⁻¹
    let t : EuclideanSpace ℝ (Fin n) → ℝ := fun x => Real.exp (-ℓ * ‖x‖ ^ 2)
    let f : Matrix.orthogonalGroup (Fin n) ℝ → ℝ := fun O => ∫ x, t x ∂γ O
    Integrable t (νpos.bind γ) ∧ Integrable t (νneg.bind γ) ∧
      Integrable f νpos ∧ Integrable f νneg ∧
      (∫ x, t x ∂νpos.bind γ) = (∫ O, f O ∂νpos) ∧
      (∫ x, t x ∂νneg.bind γ) = (∫ O, f O ∂νneg) ∧
      ((∫ x, t x ∂νpos.bind γ) - (∫ x, t x ∂νneg.bind γ)) =
        2 * (∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
          (O : Matrix (Fin n) (Fin n) ℝ).det * f O ∂μ) := by
  classical
  dsimp only
  let G := Matrix.orthogonalGroup (Fin n) ℝ
  let E := EuclideanSpace ℝ (Fin n)
  let μ := orthogonalHaar n
  let Cpos : Set G := {O | (O : Matrix (Fin n) (Fin n) ℝ).det = 1}
  let Cneg : Set G := {O | (O : Matrix (Fin n) (Fin n) ℝ).det = -1}
  let νpos := (2 : ℝ≥0∞) • μ.restrict Cpos
  let νneg := (2 : ℝ≥0∞) • μ.restrict Cneg
  let γ : G → Measure E := fun O => multivariateGaussian (0 : E)
    (singleBlockPrecision κ O)⁻¹
  let t : E → ℝ := fun x => Real.exp (-ℓ * ‖x‖ ^ 2)
  let f : G → ℝ := fun O => ∫ x, t x ∂γ O
  have hlaws := actual_mixture_laws hn hκ
  have hγ : Measurable γ := hlaws.1
  let : IsProbabilityMeasure (νpos.bind γ) := hlaws.2.1
  let : IsProbabilityMeasure (νneg.bind γ) := hlaws.2.2.1
  have hpriors := component_probabilities (lt_of_lt_of_le (by decide : 0 < 3) hn)
  let : IsProbabilityMeasure νpos := hpriors.2.2.1
  let : IsProbabilityMeasure νneg := hpriors.2.2.2
  let : IsProbabilityMeasure μ := (orthogonalHaar_spec n).1
  have hγprob (O : G) : IsProbabilityMeasure (γ O) := by
    dsimp [γ]
    infer_instance
  have htc : Continuous t := by dsimp [t, E]; fun_prop
  have htnn (x : E) : 0 ≤ t x := (Real.exp_pos _).le
  have htb (x : E) : ‖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 htL (ρ : Measure E) [IsProbabilityMeasure ρ] : Integrable t ρ :=
    (integrable_const (1 : ℝ)).mono' htc.aestronglyMeasurable
      (Filter.Eventually.of_forall htb)
  let q : G → ℝ≥0∞ := fun O => ∫⁻ x, ENNReal.ofReal (t x) ∂γ O
  have hqm : Measurable q :=
    (Measure.measurable_lintegral (ENNReal.measurable_ofReal.comp htc.measurable)).comp hγ
  have hqle (O : G) : q O ≤ 1 := by
    let := hγprob O
    calc
      q O ≤ ∫⁻ x, (1 : ℝ≥0∞) ∂γ O := by
        apply lintegral_mono
        intro x
        have htupper : t x ≤ 1 :=
          (le_abs_self (t x)).trans (by simpa only [Real.norm_eq_abs] using htb x)
        simpa using ENNReal.ofReal_le_ofReal htupper
      _ = 1 := by simp
  have hqfin (O : G) : q O < ⊤ := (hqle O).trans_lt (by simp)
  have hfq (O : G) : f O = (q O).toReal :=
    integral_eq_lintegral_of_nonneg_ae (Filter.Eventually.of_forall htnn)
      htc.aestronglyMeasurable
  have hfm : Measurable f := by
    have heq : f = fun O => (q O).toReal := funext hfq
    rw [heq]
    exact ENNReal.measurable_toReal.comp hqm
  have hfb (O : G) : ‖f O‖ ≤ 1 := by
    let := hγprob O
    simpa only [f, probReal_univ, mul_one] using
      (norm_integral_le_of_norm_le_const (Filter.Eventually.of_forall htb) :
        ‖∫ x, t x ∂γ O‖ ≤ (1 : ℝ) * (γ O).real Set.univ)
  have hfL (ρ : Measure G) [IsProbabilityMeasure ρ] : Integrable f ρ :=
    (integrable_const (1 : ℝ)).mono' hfm.aestronglyMeasurable
      (Filter.Eventually.of_forall hfb)
  have htrans (ν : Measure G) [IsProbabilityMeasure ν] :
      (∫ x, t x ∂ν.bind γ) = ∫ O, f O ∂ν := by
    have htm : AEMeasurable (fun x => ENNReal.ofReal (t x)) (ν.bind γ) :=
      (ENNReal.measurable_ofReal.comp htc.measurable).aemeasurable
    rw [integral_eq_lintegral_of_nonneg_ae (Filter.Eventually.of_forall htnn)
      htc.aestronglyMeasurable, Measure.lintegral_bind hγ.aemeasurable htm]
    have heq : f = fun O => (q O).toReal := funext hfq
    rw [heq]
    exact (integral_toReal hqm.aemeasurable (Filter.Eventually.of_forall hqfin)).symm
  have hcont : Continuous (fun O : G => (O : Matrix (Fin n) (Fin n) ℝ).det) := by
    fun_prop
  have hpos : MeasurableSet Cpos := (isClosed_eq hcont continuous_const).measurableSet
  have hneg : MeasurableSet Cneg := (isClosed_eq hcont continuous_const).measurableSet
  have hsign (O : G) : (O : Matrix (Fin n) (Fin n) ℝ).det = 1 ∨
      (O : Matrix (Fin n) (Fin n) ℝ).det = -1 := by
    have h := congrArg Matrix.det
      ((Matrix.mem_orthogonalGroup_iff (Fin n) ℝ).mp O.property)
    rw [Matrix.det_mul, Matrix.det_transpose, Matrix.det_one] at h
    exact mul_self_eq_one_iff.mp h
  have hsplit : (∫ O : G, (O : Matrix (Fin n) (Fin n) ℝ).det * f O ∂μ) =
      (∫ O in Cpos, f O ∂μ) - (∫ O in Cneg, f O ∂μ) := by
    calc
      _ = ∫ O, Cpos.indicator f O - Cneg.indicator f O ∂μ := by
        apply integral_congr_ae
        exact Filter.Eventually.of_forall fun O => by
          rcases hsign O with h | h
          · have hp : O ∈ Cpos := h
            have hm : O ∉ Cneg := by change (O : Matrix (Fin n) (Fin n) ℝ).det ≠ -1; rw [h]; norm_num
            simp only [Set.indicator_of_mem hp, Set.indicator_of_notMem hm, h, one_mul, sub_zero]
          · have hm : O ∈ Cneg := h
            have hp : O ∉ Cpos := by change (O : Matrix (Fin n) (Fin n) ℝ).det ≠ 1; rw [h]; norm_num
            simp only [Set.indicator_of_mem hm, Set.indicator_of_notMem hp, h, neg_one_mul, zero_sub]
      _ = _ := by
        rw [integral_sub ((hfL μ).indicator hpos) ((hfL μ).indicator hneg),
          integral_indicator hpos, integral_indicator hneg]
  have hipos : (∫ O, f O ∂νpos) = 2 * (∫ O in Cpos, f O ∂μ) := by
    simp [νpos, integral_smul_measure]
  have hineg : (∫ O, f O ∂νneg) = 2 * (∫ O in Cneg, f O ∂μ) := by
    simp [νneg, integral_smul_measure]
  refine ⟨htL _, htL _, hfL _, hfL _, htrans _, htrans _, ?_⟩
  change (∫ x, t x ∂νpos.bind γ) - (∫ x, t x ∂νneg.bind γ) =
    2 * (∫ O : G, (O : Matrix (Fin n) (Fin n) ℝ).det * f O ∂μ)
  rw [htrans νpos, htrans νneg, hipos, hineg, hsplit]
  ring
end AutoSamplingTheory.ExampleCases.GaussianComplexity.MixtureExpectation

Exact module and namespace context

Source correspondence and review

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
AppendixB2.2 explicitly uses n>=3,kappa>=4 and radial ell>=0, then asserts H is half the actual mixture expectation difference. The component density representation is the source convention.	Exactly those source parameters and actual mixtures; measurability/probability/L1/transport and partition estimates are internal. H is represented by the actual signed Gaussian expectation, whose density correspondence is an existing separate result.	source-implicit	Expands omitted measure/test interchange and real integrability bookkeeping without extra public premises. It does not duplicate or claim the quantitative Eq21 evaluation, TV inequality or main query results.

Actual radial-test L1 under both literal conditioned mixture laws, component-expectation L1 under both literal priors, both real Bochner transports and exact difference=2 signed actual Gaussian Haar expectation, at n>=3,kappa>=4,ell>=0 including zero. Density representation of source H and Eq21 evaluation are existing separate interfaces, not re-proved here. No TV inequality, Eq6 product, spherical/Poisson, parameter/transcript/eigenbasis or main query lower bound. Purification and full-paper completion separate.

Encoder–denoiser: accepted · equivalent-after-elaboration

Detected semantic differences

objects: The source defines H by integrating the component density; this target displays its actual Gaussian-expectation representation. The current lesson and publication attribution make the representation change visible. The separate actual density transport justifies fidelity, without becoming an analytic hypothesis of the bind-interchange proof. — Pinned HTML A2.SS2.p2 and A2.SS2.SSS2.p3/Ex56; GaussianLawDensity.gaussian_law_eq_density; GaussianExpectation.actual_gaussian_transform first conjunct; target htrans:105–115; current lesson assumptions[3], boundary and source attribution, and publication source.attribution/bindings[0].boundary.
assumptions: The implementation expands the source-implicit probability/measurability/L1 and interchange bookkeeping, proving it for the actual objects rather than requesting it as public premises. This is an explicit elaboration, not a source repair. — Target binders:22–23, laws/priors:54–65, bounded radial test:66–76, q/f:77–104, htrans:105–115; pinned GiryMonad measurable_lintegral:116ff, bind definition:248ff and lintegral_bind:285ff; pinned Bochner.Basic integral_eq_lintegral_of_nonneg_ae:483ff and integral_toReal:709ff.
scopes: The formal edge stops at the identity before Eq20 and includes the boundary tilt ℓ=0. It does not assert the TV inequality or reuse the separate Eq21 transform as its proof. The five current formula steps correctly describe this bounded proof. — Pinned HTML A2.SS2.SSS2.p3 starts with λ≥0, displays Ex57 and then separately Eq20, later choosing λ>0; current target whole module:1–148; lesson steps[0]–[4], reader_note and boundary; publication bindings[0].boundary.

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

Actual radial-test L1 under both literal conditioned mixture laws, component-expectation L1 under both literal priors, both real Bochner transports and exact difference=2 signed actual Gaussian Haar expectation, at n≥3,kappa≥4,ell≥0 including zero. Density representation of source H and Eq21 evaluation are existing separate interfaces, not re-proved here. No TV inequality, Eq6 product, spherical/Poisson, parameter/transcript/eigenbasis or main query lower bound. Purification and full-paper completion separate.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Measure.measurable_lintegral
Measure.lintegral_bind
integral_eq_lintegral_of_nonneg_ae
integral_toReal
norm_integral_le_of_norm_le_const
integral_indicator
integral_sub
integral_smul_measure

Mathematical sources

Radial test and half-mass expectation split — Actual mixture test transport and factor2 identity only; source-omitted bookkeeping is supplied, not attributed as an explicit author proof.
Mathlib: measurable integrals over actual measures — measurable_lintegral composes with the already proved actual measurable Gaussian family.
Mathlib: nonnegative integration through actual bind — Literal measure bind with proved family measurability; no arbitrary kernel replacement.
Mathlib: real integral of a nonnegative test — Converts actual Gaussian and mixture real expectations to the corresponding finite nonnegative integral.
Mathlib: finite nonnegative integrals back to real values — integral_toReal uses the internally proved q(O)<=1 finiteness, not a caller-supplied interchange hypothesis.

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

Expectations of the Gaussian mixtures

Actual mixture expectation difference

Read the formalized proofs

Expectations of the Gaussian mixtures

Mathematical statement

All objects and hypotheses

Notation and interpretation

Mathematical proof

Lean verification

Source assumptions versus formal assumptions

Detected semantic differences

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Mathematical sources

Which proof obligations and prerequisites are covered?