Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Tests and a sieve tail imply posterior contraction from a denominator bound

Statement

For each n, let Pθ,n and P0,n have jointly measurable densities pθ,n and p0,n relative to a common sigma-finite measure, and let Π be a prior. Let Θn be a measurable sieve, let An={θ:dn(θ,θ0)>rn}, and let Dn=∫pθ,n(Y)/p0,n(Y) Π(dθ) be the likelihood-ratio denominator on the P0,n-full set where p0,n(Y)>0. Suppose ϵn>0, nϵn2→∞, and constants A<B, T>A satisfy P0,n{Dn<e−Anϵn2}→0,Π(Θnc)≤e−Bnϵn2, and there are measurable tests ϕn with P0,n(ϕn=1)≤e−Tnϵn2,sup⁡θ∈An∩ΘnPθ,n(ϕn=0)≤e−Tnϵn2. Then the posterior mass of An tends to zero in P0,n-probability.

Facts & Assumptions

Given: The displayed dominated model, measurable sieve and tested alternative, denominator lower bound, sieve-tail bound, and test errors.

[F1]

Tonelli's theorem for nonnegative measurable functions on a sigma-finite product: nonnegative likelihood-ratio integrands may be integrated in either order.

[F2]

Markov's inequality for random variables: for nonnegative X and u>0, P(X>u)≤EX/u.

Proof

1.1F1givenalgebra

Define Nn=∫An∩Θnpθ,n(Y)p0,n(Y) Π(dθ),Tn=∫An∩Θncpθ,n(Y)p0,n(Y) Π(dθ). By change of density on {p0,n>0} and Tonelli [F1], E0,n[(1−ϕn)Nn]≤∫An∩ΘnPθ,n(ϕn=0)Π(dθ)≤e−Tnϵn2. For every θ, E0,n[pθ,n(Y)/p0,n(Y)]=∫{p0,n>0}pθ,n≤1, so Tonelli also gives E0,nTn≤Π(Θnc)≤e−Bnϵn2. Integrating the same bound over all Θ gives E0,nDn≤1, hence Dn<∞ almost surely.

2.1F2step 1.1givenalgebra∎

Fix δ>0. By step 1.1 the denominator is finite almost surely. On fibers with Dn=0, assign the posterior mass any value in [0,1]; these fibers lie in {Dn<e−Anϵn2}. On the event Dn≥e−Anϵn2 and ϕn=0, posterior mass Π(An∣Y)>δ implies Nn+Tn>δe−Anϵn2. The union bound and Markov [F2] therefore give P0,n{Π(An∣Y)>δ}≤P0,n{Dn<e−Anϵn2}+e−Tnϵn2+δ−1 ⁣(e−(T−A)nϵn2+e−(B−A)nϵn2). Every term tends to zero because T>A, B>A and nϵn2→∞. Since this holds for every δ>0, posterior mass on An converges to zero in probability.

Depends on

Used by

Dependency tree · two levels

19 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources