From an energy gap to a norm gap

If 0 ≤ E₂ ≤ E₁ ≤ E₀, K ≥ 0 and E₁ - E₂ ≥ 3.2 K E₀, then K √E₀ ≤ 2 (√E₁ - √E₂).

theorem AVenhance.Infra.FullTheorem.Separation.sqrt_gap {E₀ E₁ E₂ K : ℝ} (h1 : E₁ ≤ E₀) (h2 : 0 ≤ E₂) (h12 : E₂ ≤ E₁) (hK : 0 ≤ K) (hgap : 16 / 5 * K * E₀ ≤ E₁ - E₂) : K * √E₀ ≤ 2 * (√E₁ - √E₂)