Inequalities between quadratic penalties over ℝ

Main results

• Real.le_add_sq_div_two_mul_of_sq_div_le: if m ≤ b + d² / (2σ) and the penalty δ₀² / (2τ) beats c' - m + δ₀² / (2σ) with 0 < τ ≤ σ, then c' ≤ b + d² / (2τ) for every d ≥ δ₀ ≥ 0.

theorem Real.le_add_sq_div_two_mul_of_sq_div_le {δ₀ d τ σ m b c' : ℝ} (hδ₀ : 0 ≤ δ₀) (hdδ : δ₀ ≤ d) (hτ₀ : 0 < τ) (hτσ : τ ≤ σ) (hτK : c' - m + δ₀ ^ 2 / (2 * σ) ≤ δ₀ ^ 2 / 2 * τ⁻¹) (h : m ≤ b + d ^ 2 / (2 * σ)) : c' ≤ b + d ^ 2 / (2 * τ)

A quadratic penalty inequality: if m ≤ b + d² / (2σ) and the penalty δ₀² / (2τ) already beats c' - m + δ₀² / (2σ) with τ ≤ σ, then every point at distance d ≥ δ₀ satisfies c' ≤ b + d² / (2τ).