proofs
Provedattentiondriftsecond-momentinequality

Sharp pointwise quadratic envelope on an interval

For all a,b,x∈R\htmlData{mx=1}{a, b, x \in \htmlData{mx=0}{\mathbb{R}}}, if a≤x\htmlData{mx=0}{a} \mathrel{\htmlData{mx=2}{\leq}} \htmlData{mx=1}{x} and x≤b\htmlData{mx=0}{x} \mathrel{\htmlData{mx=2}{\leq}} \htmlData{mx=1}{b}, then

x2≤(a+b)⋅x−a⋅b\htmlData{mx=1}{\htmlData{mx=0}{x}^{2}} \mathrel{\htmlData{mx=11}{\leq}} \htmlData{mx=10}{\htmlData{mx=6}{(\htmlData{mx=4}{\htmlData{mx=2}{a} + \htmlData{mx=3}{b}}) \cdot \htmlData{mx=5}{x}} - \htmlData{mx=9}{\htmlData{mx=7}{a} \cdot \htmlData{mx=8}{b}}}
What the notation means · or point at any symbol
RReal numbers
The real numbers: every point on the number line. (ℝ)
x ∈ TVariables
a, b, x range over real numbers: the statement must hold for every choice. ((a b x : ℝ))
≤At most
a is less than or equal to x. (a ≤ x)
aᵇPower
x raised to the power 2. (x ^ 2)
·Multiplication
a + b times x. ((a + b) * x)
-Subtraction
(a + b) · x minus a · b. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. ((a + b) * x - a * b)
+Addition
a plus b. (a + b)

For a ≤ x ≤ b, x² ≤ (a+b)x-ab. This is the pointwise core used to sharpen bounded-tilt second-moment bounds.

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

More proved statements