proofs
Provedattentionfinite-probabilityreview-v7

Adaptive original-coordinate lower bound with exact independent-inclusion attainment

For all B∈N\htmlData{mx=1}{B \in \htmlData{mx=0}{\mathbb{N}}}, lambda,ε∈R\htmlData{mx=1}{\mathit{lambda}, \varepsilon \in \htmlData{mx=0}{\mathbb{R}}}, Ω:Type⁡⋅\htmlData{mx=2}{\Omega : \htmlData{mx=1}{\htmlData{mx=0}{\operatorname{Type}} \cdot }}, ν∈Measure⁡ Ω\htmlData{mx=3}{\nu \in \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Measure}}\,\htmlData{mx=1}{\Omega}}}, policy:Ω→Policy⁡ Fin⁡ B univ⁡\htmlData{mx=8}{\mathit{policy} : \htmlData{mx=0}{\Omega} \mathrel{\htmlData{mx=7}{\to}} \htmlData{mx=6}{\htmlData{mx=1}{\operatorname{Policy}}\,\htmlData{mx=4}{\htmlData{mx=2}{\operatorname{Fin}}\,\htmlData{mx=3}{B}}\,\htmlData{mx=5}{\operatorname{univ}}}}, hY:∀σ, Integrable⁡ ω↦answer⁡(run⁡(policy(ω),σ)) ν\htmlData{mx=18}{\mathit{hY} : \htmlData{mx=17}{\forall \sigma,\ \htmlData{mx=16}{\htmlData{mx=0}{\operatorname{Integrable}}\,\htmlData{mx=14}{\omega \mapsto \htmlData{mx=13}{\operatorname{answer}\left(\htmlData{mx=12}{\htmlData{mx=7}{\operatorname{run}}(\htmlData{mx=10}{\htmlData{mx=8}{\mathit{policy}}(\htmlData{mx=9}{\omega})}, \htmlData{mx=11}{\sigma})}\right)}}\,\htmlData{mx=15}{\nu}}}}, hYY:∀σ, Integrable⁡ ω↦answer⁡(run⁡(policy(ω),σ))2 ν\htmlData{mx=19}{\mathit{hYY} : \htmlData{mx=18}{\forall \sigma,\ \htmlData{mx=17}{\htmlData{mx=0}{\operatorname{Integrable}}\,\htmlData{mx=15}{\omega \mapsto \htmlData{mx=14}{\htmlData{mx=13}{\operatorname{answer}\left(\htmlData{mx=12}{\htmlData{mx=7}{\operatorname{run}}(\htmlData{mx=10}{\htmlData{mx=8}{\mathit{policy}}(\htmlData{mx=9}{\omega})}, \htmlData{mx=11}{\sigma})}\right)}^{2}}}\,\htmlData{mx=16}{\nu}}}}, hYS:∀σ, Integrable⁡ ω↦answer⁡(run⁡(policy(ω),σ))⋅observed⁡(run⁡(policy(ω),σ)) ν\htmlData{mx=32}{\mathit{hYS} : \htmlData{mx=31}{\forall \sigma,\ \htmlData{mx=30}{\htmlData{mx=0}{\operatorname{Integrable}}\,\htmlData{mx=28}{\omega \mapsto \htmlData{mx=27}{\htmlData{mx=13}{\operatorname{answer}\left(\htmlData{mx=12}{\htmlData{mx=7}{\operatorname{run}}(\htmlData{mx=10}{\htmlData{mx=8}{\mathit{policy}}(\htmlData{mx=9}{\omega})}, \htmlData{mx=11}{\sigma})}\right)} \cdot \htmlData{mx=26}{\operatorname{observed}\left(\htmlData{mx=25}{\htmlData{mx=20}{\operatorname{run}}(\htmlData{mx=23}{\htmlData{mx=21}{\mathit{policy}}(\htmlData{mx=22}{\omega})}, \htmlData{mx=24}{\sigma})}\right)}}}\,\htmlData{mx=29}{\nu}}}}, hSS:∀σ, Integrable⁡ ω↦observed⁡(run⁡(policy(ω),σ))2 ν\htmlData{mx=19}{\mathit{hSS} : \htmlData{mx=18}{\forall \sigma,\ \htmlData{mx=17}{\htmlData{mx=0}{\operatorname{Integrable}}\,\htmlData{mx=15}{\omega \mapsto \htmlData{mx=14}{\htmlData{mx=13}{\operatorname{observed}\left(\htmlData{mx=12}{\htmlData{mx=7}{\operatorname{run}}(\htmlData{mx=10}{\htmlData{mx=8}{\mathit{policy}}(\htmlData{mx=9}{\omega})}, \htmlData{mx=11}{\sigma})}\right)}^{2}}}\,\htmlData{mx=16}{\nu}}}}, hN:∀σ, Integrable⁡ ω↦probes⁡(run⁡(policy(ω),σ)) ν\htmlData{mx=19}{\mathit{hN} : \htmlData{mx=18}{\forall \sigma,\ \htmlData{mx=17}{\htmlData{mx=0}{\operatorname{Integrable}}\,\htmlData{mx=15}{\omega \mapsto \htmlData{mx=14}{\htmlData{mx=13}{\operatorname{probes}\left(\htmlData{mx=12}{\htmlData{mx=7}{\operatorname{run}}(\htmlData{mx=10}{\htmlData{mx=8}{\mathit{policy}}(\htmlData{mx=9}{\omega})}, \htmlData{mx=11}{\sigma})}\right)}}}\,\htmlData{mx=16}{\nu}}}}, hunbiased∈∀σ, (∫answer⁡(run⁡(policy(ω),σ)) dω) ∂ν)=       lambda∗total Finset.univ σ/(B : R)\htmlData{mx=16}{\mathit{hunbiased} \in \htmlData{mx=15}{\htmlData{mx=14}{\forall \sigma,\ \left(\htmlData{mx=13}{\int \htmlData{mx=12}{\operatorname{answer}\left(\htmlData{mx=11}{\htmlData{mx=6}{\operatorname{run}}(\htmlData{mx=9}{\htmlData{mx=7}{\mathit{policy}}(\htmlData{mx=8}{\omega})}, \htmlData{mx=10}{\sigma})}\right)} \, d\omega}\right)}\,\mathtt{\text{∂}{\nu})=\ \ \ \ \ \ \ lambda*total\ Finset.univ\ {\sigma}/(B\ :\ \text{ℝ})}}} and herror∈∀σ, (∫(answer⁡(run⁡(policy(ω),σ))−lambda⋅total⁡(univ⁡,σ)B)2 dω) ∂ν)≤ε2ˆ\htmlData{mx=27}{\mathit{herror} \in \htmlData{mx=26}{\htmlData{mx=25}{\forall \sigma,\ \left(\htmlData{mx=24}{\int \htmlData{mx=23}{\left(\htmlData{mx=22}{\htmlData{mx=12}{\operatorname{answer}\left(\htmlData{mx=11}{\htmlData{mx=6}{\operatorname{run}}(\htmlData{mx=9}{\htmlData{mx=7}{\mathit{policy}}(\htmlData{mx=8}{\omega})}, \htmlData{mx=10}{\sigma})}\right)} - \htmlData{mx=21}{\frac{\htmlData{mx=18}{\htmlData{mx=13}{\mathit{lambda}} \cdot \htmlData{mx=17}{\htmlData{mx=14}{\operatorname{total}}(\htmlData{mx=15}{\operatorname{univ}}, \htmlData{mx=16}{\sigma})}}}{\htmlData{mx=20}{\htmlData{mx=19}{B}}}}}\right)^{2}} \, d\omega}\right)}\,\mathtt{\text{∂}{\nu})\leq {\varepsilon}\^2}}}, if 0<B0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{B}, 0<lambda0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{\mathit{lambda}} and 0<ε0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{\varepsilon} (given MeasurableSpace⁡ Ω\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{MeasurableSpace}}\,\htmlData{mx=1}{\Omega}} and IsProbabilityMeasure⁡ ν\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{IsProbabilityMeasure}}\,\htmlData{mx=1}{\nu}}), then

(B⋅lambda2B⋅ε2+lambda2≤joint⁡(ν,σ,ω↦probes⁡(run⁡(policy(ω),σ)))∧∀σ:Input⁡ Fin⁡ B, let⁡(p))(:=fun _ : Fin B => optimalInclusion B lambda ε       let w:=inclusionWeight p       let y:=inclusionOutput p (equalCoefficient lambda σ)       (∀ ξ,0≤w ξ) ∧ (Finset.sum Finset.univ (fun ξ => w ξ))=1 ∧       mean w y=lambda∗total Finset.univ σ/(B : R) ∧       mse w y (lambda∗total Finset.univ σ/(B : R))=ε2ˆ ∧       mean w inclusionReads=(B : R)∗lambda2ˆ/((B : R)∗ε2ˆ+lambda2ˆ)))\htmlData{mx=43}{\left(\htmlData{mx=13}{\frac{\htmlData{mx=4}{\htmlData{mx=1}{\htmlData{mx=0}{B}} \cdot \htmlData{mx=3}{\htmlData{mx=2}{\mathit{lambda}}^{2}}}}{\htmlData{mx=12}{\htmlData{mx=9}{\htmlData{mx=6}{\htmlData{mx=5}{B}} \cdot \htmlData{mx=8}{\htmlData{mx=7}{\varepsilon}^{2}}} + \htmlData{mx=11}{\htmlData{mx=10}{\mathit{lambda}}^{2}}}}} \mathrel{\htmlData{mx=32}{\leq}} \htmlData{mx=31}{\htmlData{mx=14}{\operatorname{joint}}(\htmlData{mx=15}{\nu}, \htmlData{mx=30}{\sigma, \omega \mapsto \htmlData{mx=29}{\htmlData{mx=28}{\operatorname{probes}\left(\htmlData{mx=27}{\htmlData{mx=22}{\operatorname{run}}(\htmlData{mx=25}{\htmlData{mx=23}{\mathit{policy}}(\htmlData{mx=24}{\omega})}, \htmlData{mx=26}{\sigma})}\right)}}})} \mathbin{\htmlData{mx=42}{\land}} \htmlData{mx=41}{\forall \sigma : \htmlData{mx=40}{\htmlData{mx=36}{\operatorname{Input}}\,\htmlData{mx=39}{\htmlData{mx=37}{\operatorname{Fin}}\,\htmlData{mx=38}{B}}},\ \htmlData{mx=35}{\htmlData{mx=33}{\operatorname{let}}(\htmlData{mx=34}{p})}}\right)(\mathtt{:=fun\ \_\ :\ Fin\ B\ =>\ optimalInclusion\ B\ lambda\ {\varepsilon}\ \ \ \ \ \ \ let\ w:=inclusionWeight\ p\ \ \ \ \ \ \ let\ y:=inclusionOutput\ p\ (equalCoefficient\ lambda\ {\sigma})\ \ \ \ \ \ \ (\forall \ {\xi},0\leq w\ {\xi})\ \text{∧}\ (Finset.sum\ Finset.univ\ (fun\ {\xi}\ =>\ w\ {\xi}))=1\ \text{∧}\ \ \ \ \ \ \ mean\ w\ y=lambda*total\ Finset.univ\ {\sigma}/(B\ :\ \text{ℝ})\ \text{∧}\ \ \ \ \ \ \ mse\ w\ y\ (lambda*total\ Finset.univ\ {\sigma}/(B\ :\ \text{ℝ}))={\varepsilon}\^2\ \text{∧}\ \ \ \ \ \ \ mean\ w\ inclusionReads=(B\ :\ \text{ℝ})*lambda\^2/((B\ :\ \text{ℝ})*{\varepsilon}\^2+lambda\^2))})}
What the notation means · or point at any symbol
NNatural numbers
The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
<Less than
0 is strictly smaller than B. (0<B)
RReal numbers
The real numbers: every point on the number line. (ℝ)
x ∈ TVariables
lambda, ε range over real numbers: the statement must hold for every choice. ((lambda ε : ℝ))
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*)
MeasurableSpace
MeasurableSpace: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (MeasurableSpace)
f(x)Function application
MeasurableSpace applied to Ω. Lean writes f x; papers write f(x). (MeasurableSpace Ω)
Measure
Measure: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Measure)
IsProbabilityMeasure
IsProbabilityMeasure: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (IsProbabilityMeasure)
⟹Implies
If Ω, then Policy(Fin(B), univ). (Between types, A → B is the type of functions from A to B.) (Ω → Policy (Fin B) Finset.univ)
∀For all
The statement after the comma holds for every σ. (∀ σ,Integrable (fun ω => (run (policy ω…)
Policy
Policy: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Policy)
Integrable
Integrable: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Integrable)
∫Integral
The integral of answer(run(policy(ω), σ)) over ω: the signed area under it. (∫ ω,(run (policy ω) σ).answer)
≤At most
B · lambda^2/(B · ε^2 + lambda^2) is less than or equal to joint(ν, σ, ω ↦ probes(run(policy(ω), σ))). ((B : ℝ)*lambda^2/((B : ℝ)*ε^2+lambda^2)…)
∧And
Both hold: B · lambda^2/(B · ε^2 + lambda^2) ≤ joint(ν, σ, ω ↦ probes…, and ∀ σ, let(p). ((B : ℝ)*lambda^2/((B : ℝ)*ε^2+lambda^2)…)
-Subtraction
answer(run(policy(ω), σ)) minus lambda · total(univ, σ)/B. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. ((run (policy ω) σ).answer- lambda*total…)
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)
x ↦ f(x)Function (λ-abstraction)
The function sending ω to answer(run(policy(ω), σ)). Lean writes fun x => …; papers write x ↦ …. (fun ω => (run (policy ω) σ).answer)
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)
+Addition
B · ε^2 plus lambda^2. ((B : ℝ)*ε^2+lambda^2)
e.fanswer
answer of run(policy(ω), σ): Lean's dot notation e.answer means answer applied to e. ((run (policy ω) σ).answer)
aᵇPower
answer(run(policy(ω), σ)) raised to the power 2. ((run (policy ω) σ).answer^2)
(x : T)As real numbers
probes(run(policy(ω), σ)) read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. (((run (policy ω) σ).probes : ℝ))
run
run: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (run)
e.fprobes
probes of run(policy(ω), σ): Lean's dot notation e.probes means probes applied to e. ((run (policy ω) σ).probes)
a/bDivision
lambda · total(univ, σ) divided by B. In Lean, dividing by 0 gives 0. (lambda*total Finset.univ σ/(B : ℝ))
total
total: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (total)
e.fobserved
observed of run(policy(ω), σ): Lean's dot notation e.observed means observed applied to e. ((run (policy ω) σ).observed)
joint
joint: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (joint)
Input
Input: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Input)
let
let: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (let)

Exact finite formal target reconstructed from the supplied version-7 review. Proof resides in the pinned additive library. Standard Lean axioms only. Does not certify floating-point implementation, full RAM runtime, weighted adaptive frontier, or unrestricted attention hardness.

How it was proved

Proved
6 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
30 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.

More proved statements