A radial test bounds mixture TV

Huanjian Zhou and Taiji Suzuki, On Complexity of Gaussian Sampling. Eq20 with the Section2 factor-one event-TV convention. Measure/density and Bernoulli-kernel details are supplied background.

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 radial test bounds mixture TV

Read this first

Mathematical statement

The bounded radial test turns its signed Gaussian average into a lower bound on the actual mixture distance.

\[2|H(\ell)|\le\operatorname{TV}(P_+,P_-).\]

Lean statement · actual_radial_test_tv

Only the source parameters are premises; the literal actual density-defined H and event-supremum TV occur in the conclusion.

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_radial_test_tv {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 Ppos := νpos.bind γ
    let Pneg := νneg.bind γ
    let t : EuclideanSpace ℝ (Fin n) → ℝ := fun x => Real.exp (-ℓ * ‖x‖ ^ 2)
    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)
    2 * |∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
      (O : Matrix (Fin n) (Fin n) ℝ).det * (∫ x, t x * p O x) ∂μ| ≤
      sSup {z : ℝ | ∃ B : Set (EuclideanSpace ℝ (Fin n)),
        MeasurableSet B ∧ z = |Ppos.real B - Pneg.real B|}

Exact module and namespace context

Used by the single-block separation proof; its numerical lower bound remains open.

Full assumptions and notation

All objects and hypotheses

\(n\ge3\), \(\kappa\ge4\), and \(\ell\ge0\), including \(\ell=0\).
\(\mu\) is normalized Haar on full real \(O(n)\), \(\nu_\pm=2\mu|_{\{\det O=\pm1\}}\), and \(P_\pm=\nu_\pm\mathbin{\mathrm{bind}}\gamma\) with the actual \(\gamma_O=\mathcal N(0,A_O^{-1})\).
\(p_O\) is the actual normalized density relative to Euclidean volume. All integrals are real Bochner integrals; absolute integrability and actual law identities are proved internally.
TV uses the supremum over measurable events, with no extra factor of two. Measurability, probability laws and the event supremum conditions are produced inside the proof.

Notation and interpretation

\(A_O\) and \(p_O\): Literal precision and normalized Euclidean density.
\[A_O=\frac{\kappa+1}{2}I_n-\frac{\kappa-1}{4}(O+O^\top),\qquad p_O(x)=\frac{\sqrt{\det A_O}}{(2\pi)^{n/2}}e^{-x^\top A_Ox/2}.\]
\(t\) and \(H\): Radial test and source density-defined signed average.
\[t(x)=e^{-\ell\|x\|^2},\qquad H(\ell)=\int_{O(n)}\det(O)\!\left(\int_{\mathbb R^n}t(x)p_O(x)\,dx\right)d\mu(O).\]
\(\operatorname{TV}\): Factor-one event supremum; no signed-variation convention is substituted.
\[\operatorname{TV}(P_+,P_-)=\sup_{B\ \mathrm{measurable}}|P_+(B)-P_-(B)|.\]

Mathematical proof

Open a step to read its argument and formula.

1. Identify the actual Gaussian integral

Use the existing law–density theorem. The radial test is bounded, so its actual Gaussian integral and its density integral are absolutely integrable and agree.

\[f(O)=\int t\,d\gamma_O=\int_{\mathbb R^n}t(x)p_O(x)\,dx.\]

Corresponding Lean step

hpoint uses gaussian_law_eq_density, integrable_withDensity_iff and integral_withDensity_eq_integral_toReal_smul. hp0/hpm/hpfin and bounded actual-Gaussian L1 are internal.

2. Use the actual mixture gap

The existing mixture-expectation theorem gives the factor two. Its prior integrability and the sign partition also give absolute integrability of the signed full-Haar density average.

\[\mathbb E_{P_+}t-\mathbb E_{P_-}t=2H(\ell).\]

Corresponding Lean step

hgap is the identical actual_mixture_expectation_gap. hparts/hunion/hfL and bounded determinant multiplication produce hHactualL/hHdensityL; hH identifies the exact source density-defined H.

3. Represent the test by one output event

Construct a Bernoulli kernel with success probability equal to the radial test. Its probability of the event consisting of one is exactly the test value, and its composed probability is the actual test expectation.

\[K(x,\cdot)=t(x)\delta_1+(1-t(x))\delta_0,\qquad (K\circ P_\pm)(\{1\})=\mathbb E_{P_\pm}t.\]

Corresponding Lean step

b is the continuous unit-interval test. K is the literal bernoulliMeasure kernel; hKtest and happly prove its real event identity using bind_apply and finite integral_toReal.

4. Reuse the shared TV contraction

Probability bounds make the event supremum nonempty and bounded. Apply the same compiled common-kernel contraction theorem at the event consisting of one.

\[|\mathbb E_{P_+}t-\mathbb E_{P_-}t|\le\sup_{B\ \mathrm{measurable}}|P_+(B)-P_-(B)|.\]

Corresponding Lean step

D is the literal real event-discrepancy set; hDne/hDbd/hδ establish the actual sSup meaning. htest calls the canonical KernelTotalVariation.abs_real_comp_sub_le, not a copied layercake proof.

5. Keep the exact normalization

Substitute the density-defined signed gap into the bounded-test estimate. Taking the absolute value retains the factor two and gives Eq20.

\[2|H(\ell)|=|2H(\ell)|\le\operatorname{TV}(P_+,P_-).\]

Corresponding Lean step

hgap' composes the actual mixture gap with hH; abs_mul and positivity of2 finish. No quantitative value of H, Poisson estimate or query model is assumed.

Lean verification

Lean proof · actual_radial_test_tv

Identify density integrals, consume the actual mixture gap, construct the radial Bernoulli test kernel and reuse the identical compiled common-kernel TV contraction.

Download module (.lean)

theorem actual_radial_test_tv {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 Ppos := νpos.bind γ
    let Pneg := νneg.bind γ
    let t : EuclideanSpace ℝ (Fin n) → ℝ := fun x => Real.exp (-ℓ * ‖x‖ ^ 2)
    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)
    2 * |∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
      (O : Matrix (Fin n) (Fin n) ℝ).det * (∫ x, t x * p O x) ∂μ| ≤
      sSup {z : ℝ | ∃ B : Set (EuclideanSpace ℝ (Fin n)),
        MeasurableSet B ∧ z = |Ppos.real B - Pneg.real B|} := by
  classical
  dsimp only
  let G := Matrix.orthogonalGroup (Fin n) ℝ
  let E := EuclideanSpace ℝ (Fin n)
  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 Ppos := νpos.bind γ
  let Pneg := νneg.bind γ
  let t : EuclideanSpace ℝ (Fin n) → ℝ := fun x => Real.exp (-ℓ * ‖x‖ ^ 2)
  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 f : G → ℝ := fun O => ∫ x, t x ∂γ O
  have hlaws := actual_mixture_laws hn hκ
  let : IsProbabilityMeasure Ppos := hlaws.2.1
  let : IsProbabilityMeasure Pneg := hlaws.2.2.1
  have hgap := actual_mixture_expectation_gap hn hκ hℓ
  have htc : Continuous t := by dsimp [t]; fun_prop
  have ht0 (x : E) : 0 ≤ t x := (Real.exp_pos _).le
  have ht1 (x : E) : t x ≤ 1 := by
    exact Real.exp_le_one_iff.mpr
      (mul_nonpos_of_nonpos_of_nonneg (neg_nonpos.mpr hℓ) (sq_nonneg _))
  have htnorm (x : E) : ‖t x‖ ≤ 1 := by
    simpa only [Real.norm_eq_abs, abs_of_nonneg (ht0 x)] using ht1 x
  have hp0 (O : G) (x : E) : 0 ≤ p O x := by dsimp [p]; positivity
  have hpm (O : G) : Measurable (fun x => ENNReal.ofReal (p O x)) := by
    dsimp [p]; fun_prop
  have hpfin (O : G) : ∀ᵐ x ∂(volume : Measure E),
      ENNReal.ofReal (p O x) < ⊤ :=
    Filter.Eventually.of_forall fun _ => ENNReal.ofReal_lt_top
  have hpoint (O : G) :
      Integrable (fun x => t x * p O x) volume ∧
        f O = ∫ x, t x * p O x := by
    let : IsProbabilityMeasure (γ O) := by dsimp [γ]; infer_instance
    have htL : Integrable t (γ O) :=
      (integrable_const (1 : ℝ)).mono' htc.aestronglyMeasurable
        (Filter.Eventually.of_forall htnorm)
    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))) :=
      hd ▸ htL
    have hw := (integrable_withDensity_iff (hpm O) (hpfin O)).mp htd
    refine ⟨?_, ?_⟩
    · simpa only [ENNReal.toReal_ofReal (hp0 O _)] using hw
    · change (∫ x, t x ∂γ O) = _
      rw [hd, integral_withDensity_eq_integral_toReal_smul (hpm O) (hpfin 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 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 hparts :
      Integrable f (μ.restrict {O : G | (O : Matrix (Fin n) (Fin n) ℝ).det = 1}) ∧
      Integrable f (μ.restrict {O : G | (O : Matrix (Fin n) (Fin n) ℝ).det = -1}) := by
    constructor
    · exact (integrable_smul_measure (by norm_num : (2 : ℝ≥0∞) ≠ 0)
        (by norm_num : (2 : ℝ≥0∞) ≠ ⊤)).mp hgap.2.2.1
    · exact (integrable_smul_measure (by norm_num : (2 : ℝ≥0∞) ≠ 0)
        (by norm_num : (2 : ℝ≥0∞) ≠ ⊤)).mp hgap.2.2.2.1
  have hunion : {O : G | (O : Matrix (Fin n) (Fin n) ℝ).det = 1} ∪
      {O : G | (O : Matrix (Fin n) (Fin n) ℝ).det = -1} = Set.univ := by
    exact Set.eq_univ_iff_forall.mpr hsign
  have hfL : Integrable f μ := by
    have hU := integrableOn_union.mpr hparts
    simpa only [hunion, integrableOn_univ] using hU
  have hdetm : Continuous (fun O : G => (O : Matrix (Fin n) (Fin n) ℝ).det) := by
    fun_prop
  have hdetb (O : G) : ‖(O : Matrix (Fin n) (Fin n) ℝ).det‖ ≤ 1 := by
    rcases hsign O with h | h <;> simp [h]
  have hHactualL : Integrable
      (fun O : G => (O : Matrix (Fin n) (Fin n) ℝ).det * f O) μ :=
    hfL.bdd_mul hdetm.aestronglyMeasurable (Filter.Eventually.of_forall hdetb)
  have hHdensityL : Integrable (fun O : G =>
      (O : Matrix (Fin n) (Fin n) ℝ).det * (∫ x, t x * p O x)) μ := by
    apply hHactualL.congr
    exact Filter.Eventually.of_forall fun O => by
      change (O : Matrix (Fin n) (Fin n) ℝ).det * f O =
        (O : Matrix (Fin n) (Fin n) ℝ).det * (∫ x, t x * p O x)
      rw [(hpoint O).2]
  have hH : (∫ O : G, (O : Matrix (Fin n) (Fin n) ℝ).det * f O ∂μ) =
      ∫ O : G, (O : Matrix (Fin n) (Fin n) ℝ).det * (∫ x, t x * p O x) ∂μ := by
    apply integral_congr_ae
    exact Filter.Eventually.of_forall fun O => by
      change (O : Matrix (Fin n) (Fin n) ℝ).det * f O =
        (O : Matrix (Fin n) (Fin n) ℝ).det * (∫ x, t x * p O x)
      rw [(hpoint O).2]
  let D : Set ℝ := {z | ∃ B : Set E, MeasurableSet B ∧
    z = |Ppos.real B - Pneg.real B|}
  have hDne : D.Nonempty := ⟨0, ∅, MeasurableSet.empty, by simp⟩
  have hDbd : BddAbove D := by
    refine ⟨1, ?_⟩
    rintro z ⟨B, hB, rfl⟩
    have hp0 : 0 ≤ Ppos.real B := measureReal_nonneg
    have hp1 : Ppos.real B ≤ 1 := measureReal_le_one
    have hn0 : 0 ≤ Pneg.real B := measureReal_nonneg
    have hn1 : Pneg.real B ≤ 1 := measureReal_le_one
    exact abs_le.mpr ⟨by linarith, by linarith⟩
  have hδ (B : Set E) (hB : MeasurableSet B) :
      |Ppos.real B - Pneg.real B| ≤ sSup D :=
    le_csSup hDbd ⟨B, hB, rfl⟩
  let b : E → unitInterval := fun x => ⟨t x, ht0 x, ht1 x⟩
  have hbc : Continuous b := by dsimp [b]; fun_prop
  let K : Kernel E ℝ := ⟨fun x => bernoulliMeasure (1 : ℝ) 0 (b x), by
    refine Measure.measurable_of_measurable_coe _ fun B hB => ?_
    simp only [bernoulliMeasure_apply _ hB]
    split_ifs <;> fun_prop⟩
  let : IsMarkovKernel K := ⟨fun x => by
    change IsProbabilityMeasure (bernoulliMeasure (1 : ℝ) 0 (b x))
    infer_instance⟩
  have hKtest (x : E) : (K x).real {1} = t x := by
    exact bernoulliMeasure_real_apply_of_mem_of_notMem (b x)
      (measurableSet_singleton 1) (by simp) (by norm_num)
  have happly (ρ : Measure E) [IsProbabilityMeasure ρ] :
      (K ∘ₘ ρ).real {1} = ∫ x, t x ∂ρ := by
    change (Measure.bind ρ K {1}).toReal = _
    rw [Measure.bind_apply (measurableSet_singleton 1) K.aemeasurable]
    calc
      _ = ∫ x, (K x {1}).toReal ∂ρ :=
        (integral_toReal (K.measurable_coe (measurableSet_singleton 1)).aemeasurable
          (Filter.Eventually.of_forall fun x => measure_lt_top (K x) {1})).symm
      _ = _ := integral_congr_ae (Filter.Eventually.of_forall hKtest)
  have htest := AutoSamplingTheory.TechnicalLemmas.Probability.KernelTotalVariation.abs_real_comp_sub_le
    Ppos Pneg K hδ {1} (measurableSet_singleton 1)
  rw [happly Ppos, happly Pneg] at htest
  have hgap' : (∫ x, t x ∂Ppos) - (∫ x, t x ∂Pneg) =
      2 * (∫ O : G, (O : Matrix (Fin n) (Fin n) ℝ).det *
        (∫ x, t x * p O x) ∂μ) := by
    exact hgap.2.2.2.2.2.2.trans (congrArg (fun y : ℝ => 2 * y) hH)
  rw [hgap', abs_mul, abs_of_pos (by norm_num : (0 : ℝ) < 2)] at htest
  exact htest
end AutoSamplingTheory.ExampleCases.GaussianComplexity.ActualTotalVariation

Exact module and namespace context

Source correspondence and review

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
Section2 bounded [0,1] test inequality, AppendixB2 Eq20 at n>=3,kappa>=4 and radial ell>=0, with actual Gaussian density and actual mixtures.	Exactly those source parameters and literal actual objects. Measurable probability laws, absolute integrability, actual density/mixture identities, Bernoulli kernel, and event supremum conditions are produced internally.	source-implicit	Supplies omitted measure-theoretic and bounded-test details without an extra public premise. No numerical or query result is claimed.

Exact source Eq20 at n>=3,kappa>=4,ell>=0 including zero, for actual bind mixtures and source density-defined H, with factor-one measurable-event TV. Probability, measurability, absolute Bochner L1, density transport, supremum nonempty/bounded and factor2 all produced internally. No numerical H/Poisson separation, Eq6 product/amplification, query/transcript/cost, hidden-eigenbasis or either main lower bound. Merge, purification and full-paper completion separate.

Encoder–denoiser: accepted · equivalent-after-elaboration

Detected semantic differences

objects: Source conditional-Haar and mixture notation is elaborated as twice-restricted actual Haar and literal Measure.bind laws; source p_O is elaborated by the exact precision density with an internal actual-law equality. — Section2 half-mass statement; Section3.1 P_b definition; component_probabilities, actual_mixture_laws and gaussian_law_eq_density. This changes representation, not the mathematical objects.
assumptions: Source implicit well-definedness of the density expectation and TV supremum is witnessed by internal probability, measurability, Bochner L1 and nonempty/bounded proofs; no additional source hypothesis is introduced. — hpoint, hparts/hunion/hfL, hHactualL/hHdensityL, hDne/hDbd, and the actual mixture expectation parent. The density and outer signed averages cannot obtain their meaning merely from Lean zero-on-nonintegrable integral totalization.

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

Exact source Eq20 at n≥3,kappa≥4,ell≥0 including zero, for actual bind mixtures and source density-defined H, with factor-one measurable-event TV. Probability, measurability, absolute Bochner L1, density transport, supremum nonempty/bounded and factor2 all produced internally. No numerical H/Poisson separation, Eq6 product/amplification, query/transcript/cost, hidden-eigenbasis or either main lower bound. Merge, purification and full-paper completion separate.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

bernoulliMeasure
bernoulliMeasure_real_apply_of_mem_of_notMem
integrable_withDensity_iff
integral_withDensity_eq_integral_toReal_smul
integrable_smul_measure
integrableOn_union
Integrable.bdd_mul
Measure.bind_apply
integral_toReal
le_csSup

Mathematical sources

Radial test to single-block TV, Eq20 — Exact Eq20 only; quantitative Proposition B.7 is the immediate consumer, not a result of this packet.
Canonical shared Markov TV contraction — The identical compiled node is applied to the actual Bernoulli test kernel; no analogy is promoted to an implication.
Mathlib Bernoulli measure — Literal two-atom probability construction and its measurable-event evaluations; authors Etienne Marion and David Ledvinka, Apache2.

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

A radial test bounds mixture TV

Source Eq20 on actual mixtures

Read the formalized proofs

A radial test bounds mixture TV

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?