Construct the actual determinant-conditioned Gaussian mixtures

Huanjian Zhou and Taiji Suzuki, On Complexity of Gaussian Sampling. The source definition of the single-block mixture is made measure-theoretically explicit; omitted construction bookkeeping is supplied background, not attributed author proof.

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

Construct the actual determinant-conditioned Gaussian mixtures

Read this first

Mathematical statement

For \(n\ge3\) and \(\kappa\ge4\), the actual Gaussian family \(\gamma_O=\mathcal N(0,A_O^{-1})\) is measurable. Mixing it over either determinant sign gives a genuine probability law \(P_\pm\), with the Borel-event evaluation formula below.

\[\begin{aligned}P_\pm&\in\mathcal P(\mathbb R^n),\\P_\pm(B)&=\int_{O(n)}\gamma_O(B)\,d\nu_\pm(O)\quad(B\text{ Borel}).\end{aligned}\]

Lean statement · actual_mixture_laws

Exact preproof sealed signature: actual covariance Gaussian family measurability, both literal conditioned binds probability, and universal Borel evaluations; source n>=3,kappa>=4.

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_laws {n : ℕ} (hn : 3 ≤ n) {κ : ℝ} (hκ : 4 ≤ κ) :
    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)⁻¹
    Measurable γ ∧ IsProbabilityMeasure (νpos.bind γ) ∧
      IsProbabilityMeasure (νneg.bind γ) ∧
      (∀ B : Set (EuclideanSpace ℝ (Fin n)), MeasurableSet B →
        (νpos.bind γ) B = ∫⁻ O, γ O B ∂νpos) ∧
      (∀ B : Set (EuclideanSpace ℝ (Fin n)), MeasurableSet B →
        (νneg.bind γ) B = ∫⁻ O, γ O B ∂νneg)

Exact module and namespace context

The bounded-test expectation gap, total-variation bound and main query lower bounds remain open.

Full assumptions and notation

All objects and hypotheses

Exactly \(n\ge3\) and \(\kappa\ge4\). No measurable-family, probability-kernel or normalization premise is supplied.
\(\mu\) is the same normalized Borel Haar probability on the full real orthogonal group. Both determinant signs occur.
\(\nu_\pm=2\mu|_{\{\det O=\pm1\}}\), and \(\gamma_O\) is the existing canonical Gaussian with zero mean and covariance \(A_O^{-1}\). The state space is Borel Euclidean \(\mathbb R^n\).
Measurability, positive-definiteness justification, prior probability, mixture probability and every Borel-set evaluation are produced internally. The source omits this construction bookkeeping; it is supplied explicitly here.

Notation and interpretation

\(A_O\): The literal source single-block precision.
\[A_O=\frac{\kappa+1}{2}I_n-\frac{\kappa-1}{4}(O+O^\top)\]
\(\mu\) and \(\nu_\pm\): Full Haar and its two normalized sign restrictions.
\[C_\pm=\{O\in O(n):\det O=\pm1\},\qquad\nu_\pm=2\mu|_{C_\pm}\]
\(\gamma_O\) and \(P_\pm\): Actual component Gaussian measures and their actual mixtures.
\[\gamma_O=\mathcal N(0,A_O^{-1}),\qquad P_\pm=\int_{O(n)}\gamma_O\,d\nu_\pm(O)\]

Mathematical proof

Open a step to read its argument and formula.

1. Make the density jointly measurable

The precision depends continuously on \(O\). The displayed density is continuous jointly in \((O,x)\), so its nonnegative extended-real form is measurable.

\[p_O(x)=\frac{\sqrt{\det A_O}}{(2\pi)^{n/2}}\exp\!\left(-\frac{x^\top A_Ox}{2}\right)\]

Corresponding Lean step

Local hAc and hpc prove continuity for the exact literal precision/density; hpm applies ENNReal.measurable_ofReal. No density measurability premise is added.

2. Identify the actual measurable Gaussian family

Use the existing exact law-density identity for every \(O\), at the unchanged source parameters. Measurability of measures with a jointly measurable density then gives measurability of the actual Gaussian family.

\[\gamma_O=p_O\,dx\quad\Longrightarrow\quad O\longmapsto\gamma_O\text{ is measurable}\]

Corresponding Lean step

The proof calls GaussianLawDensity.gaussian_law_eq_density hn hκ O, whose internal SPD proof uses the source precision bounds, then the exact Mathlib measurable_withDensity. The conclusion concerns the actual multivariateGaussian constructor.

3. Use the normalized determinant priors

The existing half-mass theorem supplies the two literal prior probability laws. The same full Haar law is retained throughout.

\[\mu\{\det O=\pm1\}=\tfrac12,\qquad\nu_\pm(O(n))=1\]

Corresponding Lean step

DeterminantComponents.component_probabilities is applied at the internally derived positive dimension. Its actual2*restriction probability conclusions are installed, not supplied by the caller.

4. Construct genuine probability mixtures

Mix the same measurable Gaussian family against each probability prior. Every component Gaussian has total mass one, so both resulting measures have total mass one.

\[P_\pm=\int\gamma_O\,d\nu_\pm(O),\qquad P_\pm(\mathbb R^n)=\int1\,d\nu_\pm=1\]

Corresponding Lean step

The actual measures are νpos.bind γ and νneg.bind γ, where bind is join of map. isProbabilityMeasure_bind consumes the proved family measurability, exact prior probabilities and actual Gaussian probability instances. No replacement density-only law or fallback kernel is defined.

5. Evaluate every Borel event

For any Borel event, the value of each actual mixture equals the corresponding average of component Gaussian probabilities. This identifies the source mixture laws; bounded-test expectation transport remains a separate step.

\[P_\pm(B)=\int\gamma_O(B)\,d\nu_\pm(O)\qquad(B\text{ Borel})\]

Corresponding Lean step

Both Measure.bind_apply calls use the measurable family already proved above. B is universally quantified in the conclusion; its Borel condition is the ordinary evaluation domain, not an additional theorem-level regularity assumption.

Lean verification

Lean proof · actual_mixture_laws

Joint literal density continuity and the exact actual Gaussian law-density node produce family measurability; exact component priors and canonical Mathlib bind facts produce both actual mixture laws.

Download module (.lean)

theorem actual_mixture_laws {n : ℕ} (hn : 3 ≤ n) {κ : ℝ} (hκ : 4 ≤ κ) :
    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)⁻¹
    Measurable γ ∧ IsProbabilityMeasure (νpos.bind γ) ∧
      IsProbabilityMeasure (νneg.bind γ) ∧
      (∀ B : Set (EuclideanSpace ℝ (Fin n)), MeasurableSet B →
        (νpos.bind γ) B = ∫⁻ O, γ O B ∂νpos) ∧
      (∀ B : Set (EuclideanSpace ℝ (Fin n)), MeasurableSet B →
        (νneg.bind γ) B = ∫⁻ O, γ O B ∂νneg) := by
  classical
  dsimp only
  let G := Matrix.orthogonalGroup (Fin n) ℝ
  let E := EuclideanSpace ℝ (Fin n)
  let μ := orthogonalHaar n
  let νpos := (2 : ℝ≥0∞) • μ.restrict
    {O : G | (O : Matrix (Fin n) (Fin n) ℝ).det = 1}
  let νneg := (2 : ℝ≥0∞) • μ.restrict
    {O : G | (O : Matrix (Fin n) (Fin n) ℝ).det = -1}
  let γ : G → Measure E := fun O =>
    multivariateGaussian (0 : E) (singleBlockPrecision κ O)⁻¹
  let p : G → E → ℝ := fun O x =>
    Real.sqrt (singleBlockPrecision κ O).det / (2 * Real.pi) ^ ((n : ℝ) / 2) *
      Real.exp (-((WithLp.ofLp x) ⬝ᵥ
        (singleBlockPrecision κ O *ᵥ WithLp.ofLp x)) / 2)
  have hAc : Continuous (fun O : G => singleBlockPrecision κ O) := by
    unfold singleBlockPrecision
    exact continuous_const.sub
      ((continuous_subtype_val.add continuous_subtype_val.matrix_transpose).const_smul ((κ - 1) / 4))
  have hpc : Continuous (fun z : G × E => p z.1 z.2) := by
    dsimp only [p, E]
    fun_prop
  have hpm : Measurable (Function.uncurry (fun O x => ENNReal.ofReal (p O x))) :=
    ENNReal.measurable_ofReal.comp hpc.measurable
  have hd : γ = fun O => (volume : Measure E).withDensity
      (fun x => ENNReal.ofReal (p O x)) := by
    funext O
    exact gaussian_law_eq_density hn hκ O
  have hm : Measurable γ := by
    rw [hd]
    exact measurable_withDensity hpm
  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
  have hprob (O : G) : IsProbabilityMeasure (γ O) := by
    dsimp [γ]
    infer_instance
  refine ⟨hm, isProbabilityMeasure_bind hm.aemeasurable
    (Filter.Eventually.of_forall hprob),
    isProbabilityMeasure_bind hm.aemeasurable (Filter.Eventually.of_forall hprob), ?_, ?_⟩
  · intro B hB
    exact Measure.bind_apply hB hm.aemeasurable
  · intro B hB
    exact Measure.bind_apply hB hm.aemeasurable

end AutoSamplingTheory.ExampleCases.GaussianComplexity.GaussianMixtureLaws

Exact module and namespace context

Source correspondence and review

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
Source single-block definition uses n>=3,kappa>=4, full Haar conditioned on each determinant sign, and N(0,A_O inverse); measurable-family and probability-construction bookkeeping is implicit.	Exactly these source parameters and literal laws. Actual Gaussian measurability, both normalized-prior binds probability and all Borel evaluations are proved internally.	source-implicit	Explicit well-definedness elaborates the source expectation of measures without adding a theorem premise or claiming an omitted author proof. No mixture expectation/H/TV or product theorem follows from this packet alone.

Actual single-block Gaussian family measurability, both determinant-conditioned probability measures and their universal Borel-set evaluations only, n>=3 and kappa>=4. Source omits measurable-family/bind well-definedness bookkeeping; this supplies it without inventing an author proof. No product Eq6, mixture-density/expectation interchange, H expectation gap, TV adapter, Poisson, parameters, transcript, eigenbasis or main lower bound.

Encoder–denoiser: accepted · equivalent-after-elaboration

Detected semantic differences

assumptions: The source expected-measure notation suppresses well-definedness bookkeeping. The current theorem and exposition make it explicit as proved conclusions, without adding a measurable-family, probability-kernel or SPD premise. This is a faithful elaboration rather than a verbatim author theorem/proof. — Pinned S3.SS1.p3 defines P_b as the expected canonical Gaussian, A2.SS2.p2 uses p_O and p_b, and A2.SS3.p2 gives Eq26. Current proof hpc/hpm/hd/hm, internal gaussian_law_eq_density PosDef argument, hpriors and isProbabilityMeasure_bind produce the bookkeeping. Current publication source.attribution, bindings[0].assumption_deltas and lesson boundary identify it as supplied background.
domains: The surrounding source construction uses n <= d and later chooses n=2T+1. The isolated single-block result has no ambient-d, product, budget or parity parameter. Omitting these irrelevant surrounding parameters is justified and does not weaken the block claim or import a future result. — Pinned S3.SS1.p1 states 3 <= n <= d and later main-proof choice n=2T+1; A2.SS2.p2 restates precisely n >= 3 and kappa >= 4 for the single-block calculation. Current actual_mixture_laws quantifies only n,kappa; its conclusion and lesson/publication boundary exclude Eq6 and oracle lower bounds.
conclusion: The source average of measures is elaborated by the canonical Giry bind and universal Borel-event identities. ENNReal nonnegative integrals are the natural formal representation of nonnegative event probabilities; no arbitrary law characterized by those identities is substituted. — Pinned S3.SS1.p3 first formula. Current theorem fixes nu_pos.bind gamma and nu_neg.bind gamma in every conclusion; both final proof branches call Measure.bind_apply. Mathlib GiryMonad.lean:228-236 defines this bind as join(map) and proves its evaluation identity.

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 single-block Gaussian family measurability, both determinant-conditioned probability measures and their universal Borel-set evaluations only, n≥3 and kappa≥4. Source omits measurable-family/bind well-definedness bookkeeping; this supplies it without inventing an author proof. No product Eq6, mixture-density/expectation interchange, H expectation gap, TV adapter, Poisson, parameters, transcript, eigenbasis or main lower bound.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

measurable_withDensity
isProbabilityMeasure_bind
Measure.bind_apply
ENNReal.measurable_ofReal
ProbabilityTheory.multivariateGaussian
Continuous.measurable

Mathematical sources

Single-block Gaussian mixture definition — Actual law construction and supplied measurable-family bookkeeping only; Eq6 product and Eq20 H-to-TV remain separate.
Mathlib: measurable measures with density — The jointly measurable density produces a measurable measure-valued family; the actual same compiled theorem is called.
Mathlib: actual bind and Borel evaluation — Literal join of map and bind_apply; no separately invented kernel law.
Mathlib: probability preserved by measurable bind — Actual same isProbabilityMeasure_bind consumes the proved family and actual probability priors.
Mathlib: actual multivariate Gaussian constructor — Existing centered covariance Gaussian; source precision admissibility is established by the identical imported law-density provider.

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

Construct the actual determinant-conditioned Gaussian mixtures

Actual single-block Gaussian mixtures

Read the formalized proofs

Construct the actual determinant-conditioned 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?