Bench / mcmc
One null set for every event, or a different null set for each event?
Markov Chain Monte Carlo / SampleWiki research problems · natural-language: L3 (author-assigned; calibration pending)
Why this difficulty?
Build a finite measure and two measurable kernels, audit the order of an uncountable family of almost-everywhere quantifiers, and distinguish equality after averaging from equality of conditional versions. This is a multi-step foundational diagnosis, not a claimed research-level L5 theorem or an equivalent Lean task.
Editorial review and exact formal-coverage boundary
AI editorial review accepted. This is not canonical theorem publication, full Lean coverage or empirical difficulty calibration.
- No aligned Lean task is present. The countable/co-countable sigma-algebra and measure, kernel construction and measurability, singleton counterexample, averaged-law identities for this example, and non-countable-generation proof remain independently checked natural-language mathematics, not Lean-certified conclusions of the cited support.
- This editorial review does not freshly compile the support, create an ASTIS-owned port of the external uniqueness theorem, certify a measurable diagonal or event supremum, construct an adaptive process, or establish expected query costs. It is not a theorem-publication verdict, human consensus, or measured benchmark run.
Content-bound review status and evidence hashes · Independent reports and frozen inputs. Historical rejected wording is audit material, not training gold.
Assumptions and conventions
- \(Ω\) is an uncountable set equipped with the countable/co-countable \(σ\)-algebra: a measurable set is countable or has countable complement. Define \(μ(B)=0\) for countable B and \(μ(B)=1\) for co-countable B. Both input and output spaces use this \(σ\)-algebra.
- For measurable B define K(x,B)=1_B(x) and \(L(x,B)=μ(B)\). A Markov kernel must be a probability measure in B for each x, and measurable in x for every measurable B. The total-variation event supremum is not assumed measurable.
- Compare the statements \[(\forall B\text{ measurable})\;(K(x,B)=L(x,B)\text{ for }\mu\text{-a.e. }x)\] and \[\mu\text{-a.e. }x\;(\forall B\text{ measurable})\;K(x,B)=L(x,B).\] In the second statement the same exceptional set must work for all events.
Natural-language question
Verify that \(μ\) is a probability measure and K,L are measurable Markov kernels. Prove the first quantified statement but refute the second. Compute both output laws after averaging over \(μ\): does this example refute equality of the averaged laws? Explain exactly what it does—and does not—show about the uniform eventwise hypothesis in the local conditional-error bound, and why it is not a standard-Borel counterexample.
Reference mathematical proof
Uncountability ensures a set cannot be both countable and co-countable, so \(μ\) is well defined, with \(μ(Ω)=1\) and \(μ(∅)=0\). For a disjoint sequence of measurable sets, if one is co-countable, all the others are countable and their union is co-countable; the sum and union mass are one. If none is co-countable, the countable union is countable and both masses are zero. This proves countable additivity.
For each x, \(K(x,·)=δₓ\) and \(L(x,·)=μ\) are probability measures. For each fixed measurable B, \(x\mapsto K(x,B)=1_{B}(x)\) is measurable and \(x\mapsto L(x,B)=μ(B)\) is constant. Hence both assignments are Markov kernels; no diagonal-subset measurability in the product space is asserted or needed.
If B is countable, \(L(x,B)=0\) and K differs only on the \(μ\)-null set B. If B is co-countable, \(L(x,B)=1\) and K differs only on its \(μ\)-null complement. Thus \[\begin{gathered}\forall B\text{ measurable},\\ K(\cdot,B)=L(\cdot,B)\quad\mu\text{-a.e.}\end{gathered}\] The exceptional set depends on B.
For every x choose the measurable singleton B={x}. Then \[\begin{gathered}K(x,\{x\})=1,\\ L(x,\{x\})=0.\end{gathered}\] Consequently no x has equality for all measurable events. There cannot be a common full-measure set. An uncountable union of the individual null exceptions may be all of \(Ω\); countable closure of null sets does not justify that union.
Nevertheless, for each measurable B, \[\begin{gathered}(\mu K)(B)=\int 1_B(x)\,d\mu(x)=\mu(B),\\(\mu L)(B)=\int\mu(B)\,d\mu=\mu(B).\end{gathered}\] Both output measures are \(μ\). This refutes the quantifier interchange and equality of kernel versions almost everywhere, not the true averaged-law equality. For a fixed output event an averaging proof can use that event's own exceptional set; a common null set is a sufficient stronger API premise, not shown mathematically necessary for the averaged conclusion.
The output \(σ\)-algebra here is not countably generated: any countable family of countable/co-countable generators involves a countable union C of their countable sides, and every generator is constant on \(Ω∖C\). Every generated measurable set is therefore constant there, but the full \(σ\)-algebra contains a singleton inside \(Ω∖C\) and can separate it from another such point. The uncountable input also is not a countable type. Thus this is outside the countable-input-or-countably-generated-output interface used by Mathlib's finite-kernel uniqueness theorem. Standard-Borel outputs have countably generated \(σ\)-algebras; this example does not refute that theorem or the selected conditional-distribution interface.
Formal support and missing Lean alignment
The exact supporting source requires ∀ᵐ x, ∀ measurable event s, an event discrepancy bound. Its proof fixes the requested output event before integrating, so this source premise is sufficient, not established necessary. The folded module shows that quantifier order, the integrability/finite-mass checks and its common-suffix/telescope consumers. It does not formalize the countable/co-countable construction or this counterexample. No equivalent Lean task or compiler credit for the complete QA is invented. The external finite-kernel uniqueness interface is separately named with its countability hypothesis.
Supporting library Lean (not an aligned QA task)
import AutoSamplingTheory.TechnicalLemmas.Probability.KernelTotalVariation
/-!
# Mean conditional-kernel errors and finite hybrid telescopes
This module isolates the reusable probability-kernel core of Chen--Chewi--Lu--
Zhang, arXiv:2609.38710v1, Lemma 6.3. If two conditional Markov kernels differ
eventwise by an integrable history-dependent bound, their output laws differ by
at most the mean of that bound. A common downstream Markov kernel preserves
the same estimate, so later adaptive computation is absorbed by data
processing. A finite real-valued telescope then adds the adjacent hybrid
errors.
The declarations do not construct the paper's dummy-filled history kernels,
identify its `δ_t` with a measurable total-variation function, or compare the
capped ideal algorithm with its uncapped version. Those adapters remain
separate source obligations.
-/
open MeasureTheory ProbabilityTheory Set Finset
open scoped ProbabilityTheory BigOperators
namespace AutoSamplingTheory.TechnicalLemmas.Probability.KernelHybridTelescope
/-- An integrable pointwise event bound between two Markov kernels controls the
corresponding event discrepancy after averaging over the input law. This is
the mean-replacement step in the adaptive hybrid argument. -/
theorem abs_real_comp_sub_le_integral_eventBound
{A B : Type*} [MeasurableSpace A] [MeasurableSpace B]
(μ : Measure A) [IsProbabilityMeasure μ]
(K L : Kernel A B) [IsMarkovKernel K] [IsMarkovKernel L]
(ε : A → ℝ) (hε : Integrable ε μ)
(hbound : ∀ᵐ x ∂μ, ∀ s, MeasurableSet s →
|(K x).real s - (L x).real s| ≤ ε x) :
∀ t, MeasurableSet t →
|(K ∘ₘ μ).real t - (L ∘ₘ μ).real t| ≤ ∫ x, ε x ∂μ := by
intro t ht
have hint (M : Kernel A B) [IsMarkovKernel M] :
Integrable (fun x => (M x).real t) μ := by
apply (integrable_const (1 : ℝ)).mono'
(M.measurable_coe ht).ennreal_toReal.aestronglyMeasurable
exact Filter.Eventually.of_forall fun x => by
rw [Real.norm_eq_abs, abs_of_nonneg ENNReal.toReal_nonneg]
exact (measureReal_le_one : (M x).real t ≤ 1)
have happly (M : Kernel A B) [IsMarkovKernel M] :
(M ∘ₘ μ).real t = ∫ x, (M x).real t ∂μ := by
change (Measure.bind μ M t).toReal = ∫ x, (M x t).toReal ∂μ
rw [Measure.bind_apply ht M.aemeasurable]
exact (integral_toReal (M.measurable_coe ht).aemeasurable
(Filter.Eventually.of_forall fun x => measure_lt_top (M x) t)).symm
rw [happly K, happly L, ← integral_sub (hint K) (hint L)]
exact abs_integral_le_integral_abs.trans <|
integral_mono_ae ((hint K).sub (hint L)).abs hε <|
hbound.mono fun x hx => hx t ht
/-- The same mean replacement bound survives a common downstream Markov
kernel. In an adjacent adaptive hybrid, the downstream kernel represents all
later calls after the one conditional rule being replaced. -/
theorem abs_real_comp_commonSuffix_sub_le_integral_eventBound
{A B C : Type*} [MeasurableSpace A] [MeasurableSpace B] [MeasurableSpace C]
(μ : Measure A) [IsProbabilityMeasure μ]
(K L : Kernel A B) [IsMarkovKernel K] [IsMarkovKernel L]
(S : Kernel B C) [IsMarkovKernel S]
(ε : A → ℝ) (hε : Integrable ε μ)
(hbound : ∀ᵐ x ∂μ, ∀ s, MeasurableSet s →
|(K x).real s - (L x).real s| ≤ ε x) :
∀ t, MeasurableSet t →
|((S ∘ₖ K) ∘ₘ μ).real t - ((S ∘ₖ L) ∘ₘ μ).real t| ≤
∫ x, ε x ∂μ := by
have hKL := abs_real_comp_sub_le_integral_eventBound μ K L ε hε hbound
have hS := KernelTotalVariation.abs_real_comp_sub_le
(K ∘ₘ μ) (L ∘ₘ μ) S hKL
simpa only [← Measure.comp_assoc] using hS
/-- Finite adjacent-hybrid errors telescope. Applying this to the output laws
of hybrids `0, ..., n` turns the one-slot bounds into their accumulated error.
The result is deliberately stated for real sequences so it does not invent a
second total-variation definition. -/
theorem abs_sub_zero_le_sum_range_of_adjacent
(a δ : ℕ → ℝ) (n : ℕ)
(hstep : ∀ i < n, |a (i + 1) - a i| ≤ δ i) :
|a n - a 0| ≤ ∑ i ∈ range n, δ i := by
induction n with
| zero => simp
| succ n ih =>
calc
|a (n + 1) - a 0| ≤ |a (n + 1) - a n| + |a n - a 0| := by
exact abs_sub_le _ _ _
_ ≤ δ n + ∑ i ∈ range n, δ i :=
add_le_add (hstep n (Nat.lt_succ_self n))
(ih fun i hi => hstep i (hi.trans (Nat.lt_succ_self n)))
_ = ∑ i ∈ range (n + 1), δ i := by
rw [sum_range_succ, add_comm]
end AutoSamplingTheory.TechnicalLemmas.Probability.KernelHybridTelescope
Download exact supporting module · Uses the project toolchain and its listed imports; not a standalone replacement QA proof.
Assessment rubric · 4 points
- Proves countable additivity and normalization of the countable/co-countable measure and checks both Markov-kernel measurability requirements without assuming a measurable diagonal. (1 point)
- Establishes eventwise almost-everywhere equality and refutes a common exceptional set using measurable singletons, correctly distinguishing uncountable from countable null unions. (1 point)
- Computes both averaged output laws as \(μ\) and identifies quantifier interchange, not averaged equality, as the failed inference; does not call the source's stronger premise necessary for averaging. (1 point)
- Explains why the output \(σ\)-algebra is not countably generated and the input is uncountable, keeping standard-Borel/countability uniqueness interfaces and the absent formal QA distinct. (1 point)
Lean view: not yet aligned
The exact supporting source requires ∀ᵐ x, ∀ measurable event s, an event discrepancy bound. Its proof fixes the requested output event before integrating, so this source premise is sufficient, not established necessary. The folded module shows that quantifier order, the integrability/finite-mass checks and its common-suffix/telescope consumers. It does not formalize the countable/co-countable construction or this counterexample. No equivalent Lean task or compiler credit for the complete QA is invented. The external finite-kernel uniqueness interface is separately named with its countability hypothesis.
Supporting library Lean (not an aligned QA task)
import AutoSamplingTheory.TechnicalLemmas.Probability.KernelTotalVariation
/-!
# Mean conditional-kernel errors and finite hybrid telescopes
This module isolates the reusable probability-kernel core of Chen--Chewi--Lu--
Zhang, arXiv:2609.38710v1, Lemma 6.3. If two conditional Markov kernels differ
eventwise by an integrable history-dependent bound, their output laws differ by
at most the mean of that bound. A common downstream Markov kernel preserves
the same estimate, so later adaptive computation is absorbed by data
processing. A finite real-valued telescope then adds the adjacent hybrid
errors.
The declarations do not construct the paper's dummy-filled history kernels,
identify its `δ_t` with a measurable total-variation function, or compare the
capped ideal algorithm with its uncapped version. Those adapters remain
separate source obligations.
-/
open MeasureTheory ProbabilityTheory Set Finset
open scoped ProbabilityTheory BigOperators
namespace AutoSamplingTheory.TechnicalLemmas.Probability.KernelHybridTelescope
/-- An integrable pointwise event bound between two Markov kernels controls the
corresponding event discrepancy after averaging over the input law. This is
the mean-replacement step in the adaptive hybrid argument. -/
theorem abs_real_comp_sub_le_integral_eventBound
{A B : Type*} [MeasurableSpace A] [MeasurableSpace B]
(μ : Measure A) [IsProbabilityMeasure μ]
(K L : Kernel A B) [IsMarkovKernel K] [IsMarkovKernel L]
(ε : A → ℝ) (hε : Integrable ε μ)
(hbound : ∀ᵐ x ∂μ, ∀ s, MeasurableSet s →
|(K x).real s - (L x).real s| ≤ ε x) :
∀ t, MeasurableSet t →
|(K ∘ₘ μ).real t - (L ∘ₘ μ).real t| ≤ ∫ x, ε x ∂μ := by
intro t ht
have hint (M : Kernel A B) [IsMarkovKernel M] :
Integrable (fun x => (M x).real t) μ := by
apply (integrable_const (1 : ℝ)).mono'
(M.measurable_coe ht).ennreal_toReal.aestronglyMeasurable
exact Filter.Eventually.of_forall fun x => by
rw [Real.norm_eq_abs, abs_of_nonneg ENNReal.toReal_nonneg]
exact (measureReal_le_one : (M x).real t ≤ 1)
have happly (M : Kernel A B) [IsMarkovKernel M] :
(M ∘ₘ μ).real t = ∫ x, (M x).real t ∂μ := by
change (Measure.bind μ M t).toReal = ∫ x, (M x t).toReal ∂μ
rw [Measure.bind_apply ht M.aemeasurable]
exact (integral_toReal (M.measurable_coe ht).aemeasurable
(Filter.Eventually.of_forall fun x => measure_lt_top (M x) t)).symm
rw [happly K, happly L, ← integral_sub (hint K) (hint L)]
exact abs_integral_le_integral_abs.trans <|
integral_mono_ae ((hint K).sub (hint L)).abs hε <|
hbound.mono fun x hx => hx t ht
/-- The same mean replacement bound survives a common downstream Markov
kernel. In an adjacent adaptive hybrid, the downstream kernel represents all
later calls after the one conditional rule being replaced. -/
theorem abs_real_comp_commonSuffix_sub_le_integral_eventBound
{A B C : Type*} [MeasurableSpace A] [MeasurableSpace B] [MeasurableSpace C]
(μ : Measure A) [IsProbabilityMeasure μ]
(K L : Kernel A B) [IsMarkovKernel K] [IsMarkovKernel L]
(S : Kernel B C) [IsMarkovKernel S]
(ε : A → ℝ) (hε : Integrable ε μ)
(hbound : ∀ᵐ x ∂μ, ∀ s, MeasurableSet s →
|(K x).real s - (L x).real s| ≤ ε x) :
∀ t, MeasurableSet t →
|((S ∘ₖ K) ∘ₘ μ).real t - ((S ∘ₖ L) ∘ₘ μ).real t| ≤
∫ x, ε x ∂μ := by
have hKL := abs_real_comp_sub_le_integral_eventBound μ K L ε hε hbound
have hS := KernelTotalVariation.abs_real_comp_sub_le
(K ∘ₘ μ) (L ∘ₘ μ) S hKL
simpa only [← Measure.comp_assoc] using hS
/-- Finite adjacent-hybrid errors telescope. Applying this to the output laws
of hybrids `0, ..., n` turns the one-slot bounds into their accumulated error.
The result is deliberately stated for real sequences so it does not invent a
second total-variation definition. -/
theorem abs_sub_zero_le_sum_range_of_adjacent
(a δ : ℕ → ℝ) (n : ℕ)
(hstep : ∀ i < n, |a (i + 1) - a i| ≤ δ i) :
|a n - a 0| ≤ ∑ i ∈ range n, δ i := by
induction n with
| zero => simp
| succ n ih =>
calc
|a (n + 1) - a 0| ≤ |a (n + 1) - a n| + |a n - a 0| := by
exact abs_sub_le _ _ _
_ ≤ δ n + ∑ i ∈ range n, δ i :=
add_le_add (hstep n (Nat.lt_succ_self n))
(ih fun i hi => hstep i (hi.trans (Nat.lt_succ_self n)))
_ = ∑ i ∈ range (n + 1), δ i := by
rw [sum_range_succ, add_comm]
end AutoSamplingTheory.TechnicalLemmas.Probability.KernelHybridTelescope
Download exact supporting module · Uses the project toolchain and its listed imports; not a standalone replacement QA proof.
This support theorem does not certify the complete QA or its explanatory counterexamples.
What this does—and does not—verify
The counterexample is on the explicitly non-countably-generated measurable output, not \(\mathbb{R}\) with its Borel sets or a standard-Borel state space. It does not refute the source averaging theorem, conditional-law uniqueness with the proper countability assumptions, or measurability of any particular supplied bound. The supporting compiled module is not a formal proof of this QA. No claim about joint diagonal measurability, a measurable total-variation supremum, adaptive process construction or expected query cost is made.
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 ASTIS-authored quantifier exercise and proof, anchored to the exact hbound order in the existing local conditional-kernel averaging theorem (the reusable probability core associated with Gaussian Cloud Lemma 6.3). It is not quoted from that paper and does not assert a flaw in it. The fixed Mathlib file Mathlib/Probability/Kernel/CompProdEqIff.lean supplies Kernel.ae_eq_of_compProd_eq under MeasurableSpace.CountableOrCountablyGenerated plus finite-measure/kernel assumptions; that external interface is context, not an ASTIS-owned new leaf. This QA conservatively shares the public adaptive-hybrid family with sogb-017. No restricted source or external dataset is used.
Exact local source and full context · Locate the existing Lean declaration
AutoSamplingTheory.TechnicalLemmas.Probability.KernelHybridTelescope.abs_real_comp_sub_le_integral_eventBound
ASTIS formal support (not an equivalent QA)
AutoSamplingTheory.TechnicalLemmas.Probability.KernelHybridTelescope.abs_real_comp_sub_le_integral_eventBound
Mathlib facts / definitions
ProbabilityTheory.Kernel.ae_eq_of_compProd_eqMeasurableSpace.CountableOrCountablyGenerated
Binding SHA-256: a64992f051cc8dbb2603c11d72a720f0121aeb064ca12a66d0efd321c5e014da