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

Bench / sampling

sogb-009 · public-dev · editorial and formal status separate

What kind of guarantee does a sampling claim describe?

SampleWiki research problems · natural-language: L1 (author-assigned; calibration pending)

Why this difficulty?

Distinguish the objects and quantities in three common research guarantees without proving their implications.

Editorial review and exact formal-coverage boundary

AI editorial review accepted. This is not canonical theorem publication, full Lean coverage or empirical difficulty calibration.

  • There is no aligned Lean certification of the full terminology comparison, the choice of an algorithmic run/input law, any invariant distribution or actual-output-law identification, or any expected-cost bound.

Content-bound review status and evidence hashes · Independent reports and frozen inputs. Historical rejected wording is audit material, not training gold.

Assumptions and conventions

  • \(π\) and \(ν\) are probability measures. K is a Markov transition kernel. C is the nonnegative random number of oracle calls in a specified run, under its actual input law.

Natural-language question

Explain separately the meanings of \(TV(ν,π)\le ε\), \(πK=π\) and \(E[C]\le B\). Which objects occur in each claim, and why should a theorem statement name the run/input law when discussing expected cost? No implication among the claims needs to be proved.

Reference mathematical proof

  1. The first claim compares two probability laws: \[\operatorname{TV}(\nu,\pi)=\sup_{A\text{ measurable}}|\nu(A)-\pi(A)|\le\varepsilon.\] Here the convention has no extra factor of two.

  2. The identity \(πK=π\) is invariance of the law \(π\) under one application of K. It is a statement about the kernel and its target law, not a bound on \(ν\) or a running time.

  3. The expectation \(E[C]\le B\) concerns an algorithmic cost random variable and the probability law governing the run. Different input laws or stopping/cap rules can change that expectation.

  4. These are different theorem outputs. A proof of one should not be relabelled as a proof of another; mixing, actual-input error and expected query cost require their own links.

Formal support and missing Lean alignment

The cited formal component concerns event discrepancy under a common Markov kernel. It is support for one guarantee type, not an aligned proof of this terminology QA or an expected-cost theorem.

Assessment rubric · 4 points
  1. Defines the event-supremum TV comparison and identifies both laws. (1 point)
  2. Explains \(πK=π\) as a one-step invariance identity. (1 point)
  3. Identifies the nonnegative cost variable and its governing run/input law. (1 point)
  4. Does not conflate output error, invariance and expected cost. (1 point)

Lean view: not yet aligned

The cited formal component concerns event discrepancy under a common Markov kernel. It is support for one guarantee type, not an aligned proof of this terminology QA or an expected-cost theorem.

This support theorem does not certify the complete QA or its explanatory counterexamples.

What this does—and does not—verify

No actual algorithm law, invariant distribution or query-cost result is constructed here.

Existing library mathematics reused; no new mathematical leaf or paper-completion credit. The editorial panel records the exact current review scope and remaining unformalized explanation.

Sources, graph location and dependencies

Original introductory classification exercise for source-grounded sampling research claims.

Exact local source and full context · Locate the existing Lean declaration

AutoSamplingTheory.TechnicalLemmas.Probability.KernelTotalVariation.abs_real_comp_sub_le

ASTIS formal support (not an equivalent QA)

    Mathlib facts / definitions

      Binding SHA-256: a01b6366bfff653a1e2d2d7304b4e284d28669bfebdcfb82e663f26765274315