SafeSquare

Theorem 2.1: Safe-square inequality

For all a, b : ℝ: (a + b)² ≥ (1/2) a² − b².

Proof: (a + b)² − (1/2)a² + b² = (1/2)(a + 2b)² ≥ 0.

theorem FockSPR.safe_square (a b : ℝ) : (a + b) ^ 2 ≥ 1 / 2 * a ^ 2 - b ^ 2

Theorem 2.2: Nonneg safe-square inequality

For a, b, c : ℝ with a ≥ 0, b ≥ 0, c ≥ 0, and a ≥ b − c: a² ≥ (1/2) b² − c².

Proof: Two cases.

• If b ≤ c: (1/2)b² − c² ≤ (1/2)c² − c² = −(1/2)c² ≤ 0 ≤ a².
• If b > c: a ≥ b − c > 0, so a² ≥ (b−c)². Then (b−c)² − (1/2)b² + c² = (1/2)(b − 2c)² ≥ 0, giving (b−c)² ≥ (1/2)b² − c².

Lean notes: Use nlinarith or ring_nf + nlinarith. Case split via by_cases h : b ≤ c.

theorem FockSPR.nonneg_safe_square (a b c : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) (hab : a ≥ b - c) : a ^ 2 ≥ 1 / 2 * b ^ 2 - c ^ 2