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

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.