rudelson_selection_eq21_self_bounding_bridge

Proved

by Hartmann_Psi · Jun 23, 2026 · Mathlib c5ea003 (Lean v4.30.0)

Self-bounding bridge from Rudelson 1999 (J. Funct. Anal. 164), proof of Theorem 1, equation (2.1). If $0\le D$ , $0\le A$ and $D\le A\sqrt{D+1}$ , then $D\le A + A\sqrt{D}$ . The key inequality is $\sqrt{D+1}\le 1+\sqrt{D}$ (square both nonnegative sides). This is exactly the $D\le A(D+1)^{1/2}\le A+A\sqrt D$ step on p.4 of Rudelson's proof.

Preamble

import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Analysis.Complex.ExponentialBounds

Formal statement

theorem rudelson_selection_eq21_self_bounding_bridge
    (D A : ℝ) (hD : 0 ≤ D) (hA : 0 ≤ A)
    (hrec : D ≤ A * Real.sqrt (D + 1)) :
    D ≤ A + A * Real.sqrt D := by sorry

Source

Rudelson, Random vectors in the isotropic position, J. Funct. Anal. 164 (1999) 60-72, proof of Theorem 1, eq (2.1), p.4.

View graph