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

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.