Provedattentioncertificateimportance-samplinginequality

Certificate algebra: C + K²/C − 2 is at most K² − 1 when 1 ≤ C ≤ K

For all $\htmlData{mx=1}{K, C \in \htmlData{mx=0}{\mathbb{R}}}$ , if $1 \mathrel{\htmlData{mx=1}{\leq}} \htmlData{mx=0}{K}$ , $1 \mathrel{\htmlData{mx=1}{\leq}} \htmlData{mx=0}{C}$ and $\htmlData{mx=0}{C} \mathrel{\htmlData{mx=2}{\leq}} \htmlData{mx=1}{K}$ , then

\htmlData{mx=6}{\htmlData{mx=5}{\htmlData{mx=0}{C} + \htmlData{mx=4}{\frac{\htmlData{mx=2}{\htmlData{mx=1}{K}^{2}}}{\htmlData{mx=3}{C}}}} - 2} \mathrel{\htmlData{mx=10}{\leq}} \htmlData{mx=9}{\htmlData{mx=8}{\htmlData{mx=7}{K}^{2}} - 1}

What the notation means · or point at any symbol

RReal numbers: The real numbers: every point on the number line. (ℝ)
x ∈ TVariables: K, C range over real numbers: the statement must hold for every choice. ((K C : ℝ))
≤At most: 1 is less than or equal to K. (1 ≤ K)
+Addition: C plus K^2/C. (C + K ^ 2 / C)
-Subtraction: C + K^2/C minus 2. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (C + K ^ 2 / C - 2)
aᵇPower: K raised to the power 2. (K ^ 2)
a/bDivision: K^2 divided by C. In Lean, dividing by 0 gives 0. (K ^ 2 / C)

theorem audit-certificate-quadratic-k-bound (K C : ℝ) (hK : 1 ≤ K) (hC1 : 1 ≤ C) (hCK : C ≤ K) :
    C + K ^ 2 / C - 2 ≤ K ^ 2 - 1

Algebraic core of the sharper finite-sample certificate union bound. Under 1≤C≤K, the variance-prefactor C+K²/C−2 is bounded by K²−1, improving the paper's crude cubic-in-K worst-case simplification.

How it was proved

Proved: 5 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: 15 lines of Lean

Certificate algebra: C + K²/C − 2 is at most K² − 1 when 1 ≤ C ≤ K

How it was proved

More proved statements