Expected-probe lower bound: an adaptive sampler with a history-determined stopping time obeys |o₁−o₂|(1 − E[τ₀](k+1)/n) ≤ 2√(E[τ₀](k+1)V/n) against a random plant
For all n,k∈N, Ω∈Type, w:Ω→R, g:N→Ω→ListR→Finn, out:Ω→ListR→R, hist:(Finn→R)→Ω→N→ListR, τ:(Finn→R)→Ω→N, y1:Finn→R, y2:FinsetFinn→Finn→R and o1,o2,V∈R, if ∀ω,0≤w(ω), ∑ωw(ω)=1, ∀y,ω,hist(y,ω,0)=[], ∀y,ω,t,hist(y,ω,t+1)=hist(y,ω,t)++([y(g(t,ω,hist(y,ω,t)))]), ∀y,y′,ω,(∀t,t≤τ(y,ω)⟹hist(y′,ω,t)=hist(y,ω,t))⟹τ(y′,ω)=τ(y,ω), ∀S,j,j∈/S⟹y2(S,j)=y1(j), ∑ωw(ω)⋅out(ω,hist(y1,ω,τ(y1,ω)))=o1, ∑ωw(ω)⋅(out(ω,hist(y1,ω,τ(y1,ω)))−o1)2≤V, ∀S∈powersetCard(k+1,univ),∑ωw(ω)⋅out(ω,hist(y2(S),ω,τ(y2(S),ω)))=o2, ∀S∈powersetCard(k+1,univ),∑ωw(ω)⋅(out(ω,hist(y2(S),ω,τ(y2(S),ω)))−o2)2≤V and k+1≤n (given FintypeΩ), then
The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
x ∈ TVariables
n, k range over natural numbers: the statement must hold for every choice. ((n k : ℕ))
Type
Type: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Type)
Fintype
Fintype: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Fintype)
f(x)Function application
Fintype applied to Ω. Lean writes f x; papers write f(x). (Fintype Ω)
⟹Implies
If Ω, then ℝ. (Between types, A → B is the type of functions from A to B.) (Ω → ℝ)
∀For all
The statement after the comma holds for every ω. (∀ ω, 0 ≤ w ω)
∑Summation
Add up w(ω) for every ω. (∑ ω, w ω)
=Equality
∑ ω, w(ω) and 1 are the same. (∑ ω, w ω = 1)
Finset
Finset: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Finset)
|x|Absolute value
The size of o₁ − o₂ without its sign. (|o₁ - o₂|)
RReal numbers
The real numbers: every point on the number line. (ℝ)
≤At most
0 is less than or equal to w(ω). (0 ≤ w ω)
·Multiplication
w(ω) times out(ω, hist(y₁, ω, τ(y₁, ω))). (w ω * out ω (hist y₁ ω (τ y₁ ω)))
powersetCard
Finset.powersetCard: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Finset.powersetCard)
∉Not an element of
j is not a member of S. (j ∉ S)
List
List: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (List)
aᵇPower
out(ω, hist(y₁, ω, τ(y₁, ω))) − o₁ raised to the power 2. ((out ω (hist y₁ ω (τ y₁ ω)) - o₁) ^ 2)
-Subtraction
out(ω, hist(y₁, ω, τ(y₁, ω))) minus o₁. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (out ω (hist y₁ ω (τ y₁ ω)) - o₁)
Fin
Fin: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Fin)
a/bDivision
(∑ ω, w(ω) · τ(y₁, ω)) · (k + 1) divided by n. In Lean, dividing by 0 gives 0. (((∑ ω, w ω * (τ y₁ ω : ℝ)) * (k + 1)) /…)
+Addition
t plus 1. (t + 1)
[a, b]List
The list of , in order. ([])
(x : T)As real numbers
τ(y₁, ω) read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((τ y₁ ω : ℝ))
(x : T)Type ascription
univ read as a Finset(Fin(n)). Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((Finset.univ : Finset (Fin n)))
univ
Finset.univ: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Finset.univ)
√Square root
The non-negative number whose square is (∑ ω, w(ω) · τ(y₁, ω)) · (k + 1)/n · V. (Real.sqrt (((∑ ω, w ω * (τ y₁ ω : ℝ)) *…)
theorem ua-adaptive-expected-probe-lower-bound {n k : ℕ} {Ω : Type} [Fintype Ω] (w : Ω → ℝ) (hw : ∀ ω, 0 ≤ w ω) (hsum : ∑ ω, w ω = 1) (g : ℕ → Ω → List ℝ → Fin n) (out : Ω → List ℝ → ℝ) (hist : (Fin n → ℝ) → Ω → ℕ → List ℝ) (hhist0 : ∀ y ω, hist y ω 0 = []) (hhistS : ∀ y ω t, hist y ω (t + 1) = hist y ω t ++ [y (g t ω (hist y ω t))]) (τ : (Fin n → ℝ) → Ω → ℕ) (hτ : ∀ y y' ω, (∀ t, t ≤ τ y ω → hist y' ω t = hist y ω t) → τ y' ω = τ y ω) (y₁ : Fin n → ℝ) (y₂ : Finset (Fin n) → Fin n → ℝ) (hy : ∀ S j, j ∉ S → y₂ S j = y₁ j) (o₁ o₂ V : ℝ) (h1 : ∑ ω, w ω * out ω (hist y₁ ω (τ y₁ ω)) = o₁) (hV1 : ∑ ω, w ω * (out ω (hist y₁ ω (τ y₁ ω)) - o₁) ^ 2 ≤ V) (h2 : ∀ S ∈ Finset.powersetCard (k + 1) (Finset.univ : Finset (Fin n)), ∑ ω, w ω * out ω (hist (y₂ S) ω (τ (y₂ S) ω)) = o₂) (hV2 : ∀ S ∈ Finset.powersetCard (k + 1) (Finset.univ : Finset (Fin n)), ∑ ω, w ω * (out ω (hist (y₂ S) ω (τ (y₂ S) ω)) - o₂) ^ 2 ≤ V) (hk : k + 1 ≤ n) :
|o₁ - o₂| * (1 - ((∑ ω, w ω * (τ y₁ ω : ℝ)) * (k + 1)) / n) ≤ 2 * Real.sqrt (((∑ ω, w ω * (τ y₁ ω : ℝ)) * (k + 1)) / n * V)
Closes the gap between the fixed-budget probe lower bound and expected-work upper bounds, as proposed by an external reviewer (2026-10-05). The sampler may stop after a random number of probes τ(y, ω) determined by its coins and the history it has seen (hypothesis: if two inputs produce the same history up to τ(y, ω) then they stop at the same time). Coupling: on the unplanted input the probes form a set Q(ω) of size τ(y₁, ω); if the random (k+1)-plant misses Q(ω), the planted run has the identical history, the identical stopping time and the identical output. The hit probability is at most (k+1)/n times the expected probe count, and the centred Cauchy–Schwarz two-point bound gives the stated inequality. Generalises ua-adaptive-sampler-lower-bound (fixed s) to E[τ₀].
How it was proved
Proved
5 October 2026
By
Ajax, with the agent “Baguette math & proofs (Claude Code, 2026-10-03)”
Checked by
Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline