Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0

Compute the actual signed Gaussian test expectation

Huanjian Zhou and Taiji Suzuki, On Complexity of Gaussian Sampling. Actual law-to-density expectation transport and all required L1 conditions are explicit elaborations of the density-based source calculation.

arXiv:2610.20492v1 · Appendix B.2.2: Gaussian density p_O, bounded test h_lambda, H definition Ex56, Ex58/Ex59/Fubini, Ex60 and Eq21; Eq4/Eq26 providers. Conditioned-mixture Ex57/Eq20 remains separate. · faithful paraphrase

Complete source statement and conditions

Let \(n\ge3\), \(\kappa\ge4\), \(\ell\ge0\), and let \(\mu\) be normalized Haar probability on the full real orthogonal group. For each \(O\), set \(A_O=\frac{\kappa+1}{2}I_n-\frac{\kappa-1}{4}(O+O^\top)\), \(\gamma_O=\mathcal N(0,A_O^{-1})\), \(p_O(x)=\frac{\sqrt{\det A_O}}{(2\pi)^{n/2}}e^{-x^\top A_Ox/2}\), and \(t_\ell(x)=e^{-\ell\|x\|_2^2}\). Then \(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\). The signed expectation is absolutely integrable under \(\mu\), and its average is the displayed formula, with \(U=O_{11}\). The endpoint \(\ell=0\) is included; half-dimension powers use real division. Integrability and density transport are conclusions, with no extra premise. Conditioned target mixtures and the total-variation interpretation remain open.

  • 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.

Actual signed Gaussian transform through Eq21

\[\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}\]

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

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.

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) := 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

Source correspondence and review

Source assumptions versus formal assumptions

SourceActual LeanDifference kindWhy it matters
Standing n>=3,kappa>=4,ell>=0, actual Gaussian density p_O and full Haar O(n); H computation through Eq21.Same range, actual Gaussian/Haar/Euclidean measures and exact formula. Gaussian/weighted-volume/outer Haar L1 and law-to-density expectation equality are proved internally; conditioned-mixture/TV meaning is excluded.sameExplicitly makes the standard density-based expectation calculation rigorous for the actual existing Gaussian measure without a new public premise or constructor. The unchanged literal Fubini parent is actually consumed.

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.

Encoder–denoiser: accepted · equivalent-after-elaboration

Detected semantic differences

  • objects: H_γ, c_{n,κ} and a_ℓ(O) are reader notation with explicit definitions. Expanding them recovers the unchanged signed Eq21 statement; U=O₁₁ is the one-based source notation for Lean first entry O₀₀. — Current lesson formula and publication formulae[0].tex explicitly define c_{n,κ} and a_ℓ(O) immediately after the H_γ evaluation. The current lesson notation defines H_γ as the full determinant-weighted Haar integral and U=O₁₁; GaussianExpectation.lean binds U with j0=0 in Fin n. Pinned A2.SS2.p2 and A2.E21 use the corresponding first entry and expanded prefactor/denominator.
  • assumptions: Pointwise Gaussian/volume L1, exact actual-law transport and outer Haar L1 are explicit rigorous elaborations of the source density calculation. They are conclusions and add no assumption. — GaussianExpectation.lean first conclusion is ∀ O, Integrable t (γ O) ∧ Integrable (fun x => t x * p O x) volume ∧ the integral equality, followed by a distinct outer Integrable conjunct. The proof derives htL, hw', hpoint and houter from hn/hκ/hℓ and unchanged parents. Pinned A2.Ex56, Ex59 and surrounding p4 use the density-based bounded-test/Fubini calculation; the JSON assumptions[3] explicitly say these are conclusions with no extra premise.
  • scopes: The short headline and five concise steps retain their complete conditions, notation, exact Lean statement/proof, source correspondence and open boundaries within disclosures. Code-level preservation is confirmed; browser rendering and readability remain a separate coordinator QA responsibility. — website/scripts/declaration_lessons.py render_unit inserts every assumptions entry and all notation in Full assumptions and notation, renders each step text/formula plus its Lean disclosure, and retains exact statement/proof disclosures and boundary/provenance ledgers. website/scripts/publication_reader.py source_card retains item statement, all assumptions and formulae within Complete source statement and conditions. Current lesson has reading_layout=progressive, exactly five steps, reader_note and full boundary. This is source-code preservation evidence only.
  • scopes: The unchanged literal Fubini parent uses a sufficient compact prefactor instead of claiming the sharp source Ex59 envelope. This and B6 minor/path boundaries remain disclosed; no source repair or additional theorem is implied. — MixtureFubini.lean header discloses a finite compact prefactor as sufficient instead of the sharp Ex59 prefactor; joint_integrable obtains a bound from compactness. Current lesson boundary and publication bindings[0].boundary preserve Sharp Ex59 and B6 minor/path estimates retain unchanged disclosed parent boundaries, and expressly exclude conditioned mixtures/TV and the main bounds. The current expectation proof consumes literal_mixture_transform without expanding that scope.

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 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

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

Which proof obligations and prerequisites are covered?

  • TODO — not closed by these contributions Actual Gaussian test transport, genuine signed Haar L1 and Eq21