Provedattentionadaptive-informationfinite-probability
Adaptive fresh-probe bound from pointwise mean and MSE
For all , , , , , , and , if , , , and (given ), then
What the notation means · or point at any symbol
- 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) - ·Multiplication
- Type times . (
Type*) - x : TVariables
- ι, κ range over Type*: the statement must hold for every choice. (
(ι κ : Type*)) - DecidableEq
- DecidableEq: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
DecidableEq) - f(x)Function application
- DecidableEq applied to ι. Lean writes f x; papers write f(x). (
DecidableEq ι) - 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) - ⟹Implies
- If κ, then ℝ. (Between types, A → B is the type of functions from A to B.) (
κ → ℝ) - <Less than
- 0 is strictly smaller than epsilon. (
0 < epsilon) - ∀For all
- The statement after the comma holds for every r. (
∀ r ∈ A, 0 ≤ w r) - ∑Summation
- Add up w(r) for each r in A. (
∑ r ∈ A, w r) - =Equality
- ∑ r, w(r) and 1 are the same. (
∑ r ∈ A, w r=1) - a/bDivision
- (∑ j, |a(j)|)^2 divided by epsilon^2 + (∑ j, a(j)^2). In Lean, dividing by 0 gives 0. (
(∑ j ∈ s, |a j|)^2/(epsilon^2+∑ j ∈ s, …) - RReal numbers
- The real numbers: every point on the number line. (
ℝ) - RevealTree
- RevealTree: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
RevealTree) - e.fpowerset
- powerset of s: Lean's dot notation e.powerset means powerset applied to e. (
s.powerset) - ≤At most
- 0 is less than or equal to w(r). (
0 ≤ w r) - |x|Absolute value
- The size of a(j) without its sign. (
|a j|) - +Addition
- epsilon^2 plus ∑ j, a(j)^2. (
epsilon^2+∑ j ∈ s, (a j)^2) - execute
- execute: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
execute) - aᵇPower
- Y(r, execute(t(r), u)) − signTarget(s, a, u) raised to the power 2. (
(Y r (execute (t r) u)-signTarget s a u…) - -Subtraction
- Y(r, execute(t(r), u)) minus signTarget(s, a, u). On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
Y r (execute (t r) u)-signTarget s a u) - signTarget
- signTarget: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
signTarget) - revealCount
- revealCount: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
revealCount)
theorem attention-frontier-finite-randomized-probes {ι κ : Type*} [DecidableEq ι] {s : Finset ι} (A : Finset κ) (w : κ → ℝ)
(t : κ → RevealTree ι s) (Y : κ → (ι → ℝ) → ℝ)
(a : ι → ℝ) (epsilon : ℝ) (hepsilon : 0 < epsilon)
(hw0 : ∀ r ∈ A, 0 ≤ w r) (hw : ∑ r ∈ A, w r=1)
(hu : ∀ u ∈ s.powerset, (∑ r ∈ A, w r*Y r (execute (t r) u))=signTarget s a u)
(hmse : ∀ u ∈ s.powerset,
(∑ r ∈ A, w r*(Y r (execute (t r) u)-signTarget s a u)^2) ≤ epsilon^2) :
(∑ j ∈ s, |a j|)^2/(epsilon^2+∑ j ∈ s, (a j)^2) ≤
∑ r ∈ A, w r*revealCount (t r)Complete finite independent-seed execution: unread-sign covariance, adaptive orthogonality and billed read count are derived. Pointwise unbiasedness and MSE are the statistical hypotheses. This is the finite sign-information core, not the whole exponential-attention lower bound.
How it was proved
- Proved
- 8 October 2026
- By
- Ajax
- Checked by
- Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
- Axioms
- Classical.choice, Quot.sound, propext
- Proof
- 20 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.