Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412

KernelTotalVariation: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

  1. A common Markov kernel cannot amplify total-variation error
ASTIS mathematical exposition

A common Markov kernel cannot amplify total-variation error

AutoSamplingTheory.TechnicalLemmas.Probability.KernelTotalVariation.abs_real_comp_sub_le · theorem · Teaching coverage

Statement

Let A and B be measurable spaces, μ and ν probability measures on A, and K a Markov kernel from A to B. Let δ be real. If |μ(S)−ν(S)|≤δ for every measurable S⊆A, then |(μK)(T)−(νK)(T)|≤δ for every measurable T⊆B. No density, topology or coupling is required. The input assumption on the empty event already implies δ≥0.

\[\sup_{T\in\mathcal B}|(\mu K)(T)-(\nu K)(T)|\le\delta,\qquad (\rho K)(T)=\int_A K(x,T)\,\rho(dx).\]

All objects and hypotheses

  • K(x,·) is a probability measure for every x, and x↦K(x,T) is measurable for each measurable T. IsMarkovKernel records the first property and Kernel records the second; merely specifying transition probabilities without measurable dependence would not suffice.
  • Both input measures have total mass one. Every event probability is finite, so Measure.real is an ordinary real probability, not a misleading conversion of infinity.
  • The discrepancy premise is uniform over all measurable input events; a bound on one event, or only pointwise convergence of densities, is not the same hypothesis.
  • The same K is applied to both inputs. Comparing distinct kernels requires an additional approximation-error estimate.

Mathematical proof

1. Replace the output event by a bounded observable

Fix a measurable output event T and put f(x)=K(x,T). Kernel measurability makes f measurable and each transition law being a probability gives 0≤f≤1. Since each input measure is finite, f is strongly measurable and integrable for both inputs. Evaluating the composed law is therefore a genuine integral.

\[0\le f(x)\le1,\qquad(\rho K)(T)=\int_A f\,d\rho,\quad\rho\in\{\mu,\nu\}.\]
Corresponding Lean step

The local hf, hf0 and hf1 establish measurability and the bounds. hfi uses integrable_const and Integrable.mono'. happly unfolds Measure.bind, applies Measure.bind_apply, and converts the nonnegative integral with integral_toReal; finite event masses discharge the conversion condition.

2. Express a bounded observable by its level events

For each u, the event {x:u≤f(x)} is measurable. Integrate these event probabilities over (0,1]. This layercake identity follows because for each fixed x the set of levels u in (0,1] with u≤f(x) has length f(x). It remains valid at f=0 and f=1 and for atoms; no continuous distribution is assumed.

\[f(x)=\int_{(0,1]}\mathbf1_{\{u\le f(x)\}}\,du,\qquad\int_A f\,d\rho=\int_{(0,1]}\rho\{x:u\le f(x)\}\,du.\]
Corresponding Lean step

hlayer applies Integrable.integral_eq_integral_Ioc_meas_le using hfi and the everywhere bounds promoted to almost-everywhere bounds. This reuses Mathlib's layercake theorem rather than reproving Tonelli.

3. Justify subtraction of the two level integrals

As u increases, each level set shrinks, hence its measure is an antitone measurable function of u. These real probabilities lie in [0,1]. The interval has finite measure, so both level functions are integrable there. This explicit witness licenses subtracting their integrals.

\[0\le\rho\{f\ge u\}\le1,\qquad \int f\,d\mu-\int f\,d\nu=\int_{(0,1]}[\mu\{f\ge u\}-\nu\{f\ge u\}]\,du.\]
Corresponding Lean step

htail uses Antitone.measurable, finite-measure bounded integrability and measureReal_mono. integral_sub receives both htail witnesses. A totalized integral subtraction without those witnesses would not justify the mathematical equality.

4. Apply the event bound and preserve the exact constant

Apply the input hypothesis to every measurable level event. The absolute integrand is bounded by δ. The norm-of-integral estimate multiplies this bound by the measure of (0,1], which is exactly one. Thus no factor two is lost; this is the event-supremum convention for probability total variation.

\[|(\mu K)(T)-(\nu K)(T)|\le\int_{(0,1]}|\mu\{f\ge u\}-\nu\{f\ge u\}|\,du\le\delta\,|(0,1]|=\delta.\]
Corresponding Lean step

measurableSet_le measurable_const hf supplies each measurable event. norm_integral_le_of_norm_le_const and the interval-volume simplification close the bound; no integral-contraction hypothesis is smuggled into the inputs.

Lean statement · abs_real_comp_sub_le

Measure.real turns finite event mass into a real number. Lean writes K ∘ₘ μ for the input law μ passed through K (often written μK on paper). The theorem quantifies over arbitrary measurable spaces and uses actual Kernel and IsMarkovKernel data. There is no separate δ≥0 premise because the event bound already forces it.

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.

theorem abs_real_comp_sub_le
    {A B : Type*} [MeasurableSpace A] [MeasurableSpace B]
    (μ ν : Measure A) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
    (K : Kernel A B) [IsMarkovKernel K]
    {δ : ℝ}
    (hδ : ∀ s, MeasurableSet s → |μ.real s - ν.real s| ≤ δ) :
    ∀ t, MeasurableSet t →
      |(K ∘ₘ μ).real t - (K ∘ₘ ν).real t| ≤ δ

Exact module and namespace context

Lean proof · abs_real_comp_sub_le

The only production declaration is this contraction theorem; hf, hfi, happly, htail and hlayer are local proof terms. The focused tests exercise the declaration at zero discrepancy and compose it with a separately assumed proxy-output estimate using the triangle inequality. They also check that the empty-event premise forces nonnegative δ. No wrapper is counted as a new leaf.

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.

theorem abs_real_comp_sub_le
    {A B : Type*} [MeasurableSpace A] [MeasurableSpace B]
    (μ ν : Measure A) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
    (K : Kernel A B) [IsMarkovKernel K]
    {δ : ℝ}
    (hδ : ∀ s, MeasurableSet s → |μ.real s - ν.real s| ≤ δ) :
    ∀ t, MeasurableSet t →
      |(K ∘ₘ μ).real t - (K ∘ₘ ν).real t| ≤ δ := by
  intro t ht
  let f : A → ℝ := fun x => (K x).real t
  have hf : Measurable f := (K.measurable_coe ht).ennreal_toReal
  have hf0 (x : A) : 0 ≤ f x := measureReal_nonneg
  have hf1 (x : A) : f x ≤ 1 := measureReal_le_one
  have hfi (ρ : Measure A) [IsProbabilityMeasure ρ] :
      Integrable f ρ := by
    apply (integrable_const (1 : ℝ)).mono' hf.aestronglyMeasurable
    exact Filter.Eventually.of_forall fun x => by
      simpa only [Real.norm_eq_abs, abs_of_nonneg (hf0 x)] using hf1 x
  have happly (ρ : Measure A) [IsProbabilityMeasure ρ] :
      (K ∘ₘ ρ).real t = ∫ x, f x ∂ρ := by
    change (Measure.bind ρ K t).toReal = ∫ x, (K x t).toReal ∂ρ
    rw [Measure.bind_apply ht K.aemeasurable]
    exact (integral_toReal (K.measurable_coe ht).aemeasurable
      (Filter.Eventually.of_forall fun x => measure_lt_top (K x) t)).symm
  have htail (ρ : Measure A) [IsProbabilityMeasure ρ] :
      IntegrableOn (fun u : ℝ => ρ.real {x | u ≤ f x}) (Ioc 0 1) := by
    apply Measure.integrableOn_of_bounded
      (M := ρ.real univ) measure_Ioc_lt_top.ne
    · apply
        (Measurable.ennreal_toReal (Antitone.measurable ?_)).aestronglyMeasurable
      exact fun _ _ huv => measure_mono (fun _ hx => huv.trans hx)
    · exact Filter.Eventually.of_forall fun u => by
        simp only [Real.norm_eq_abs, abs_of_nonneg measureReal_nonneg]
        exact measureReal_mono (subset_univ _)
  have hlayer (ρ : Measure A) [IsProbabilityMeasure ρ] :
      (∫ x, f x ∂ρ) =
        ∫ u in Ioc (0 : ℝ) 1, ρ.real {x | u ≤ f x} :=
    (hfi ρ).integral_eq_integral_Ioc_meas_le
      (Filter.Eventually.of_forall hf0)
      (Filter.Eventually.of_forall hf1)
  rw [happly μ, happly ν, hlayer μ, hlayer ν,
    ← integral_sub (htail μ) (htail ν)]
  simpa [Real.norm_eq_abs, measureReal_def] using
    (norm_integral_le_of_norm_le_const
      (μ := volume.restrict (Ioc (0 : ℝ) 1))
      (f := fun u => μ.real {x | u ≤ f x} - ν.real {x | u ≤ f x})
      (C := δ)
      (Filter.Eventually.of_forall fun u => by
        simpa only [Real.norm_eq_abs] using
          hδ {x | u ≤ f x} (measurableSet_le measurable_const hf)))

end AutoSamplingTheory.TechnicalLemmas.Probability.KernelTotalVariation

Exact module and namespace context

Scope and omitted-condition boundaries

  • This proves the standard data-processing edge used in SPHMC Section 7.2, not construction of the proximal BPS kernel or the implementable/proxy laws.
  • A separate estimate TV(νK,π)≤ε gives TV(μK,π)≤δ+ε by triangle. The focused consumer test makes that estimate explicit; it does not establish mixing.
  • TV proximity alone does not control an unbounded expected query count. Actual-input cost, event-rate bounds and algorithm termination remain independent open obligations.
  • The MCMC E6 perturbed-kernel route is an intended additional consumer for its TV-specialized stability step, not an already compiled general perturbation theorem.

Source and reuse

ASTIS parents called

    Mathlib API called (external library)

    • Kernel.measurable_coe
    • Measure.bind_apply
    • integral_toReal
    • Integrable.integral_eq_integral_Ioc_meas_le
    • Antitone.measurable
    • Measure.integrableOn_of_bounded
    • integral_sub
    • norm_integral_le_of_norm_le_const

    Mathematical sources

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