Quadratic bounds for exp and log near zero

Two second-order estimates used in the analysis of multiplicative weights [AHK12]:

• Real.neg_sub_sq_le_log_one_sub: -y - y ^ 2 ≤ log (1 - y) for y ≤ 1 / 2. For 0 ≤ y ≤ 1 / 2 this is the bound -ln (1 - η) ≤ η + η ^ 2 of [AroraHazanKale2012, §1.1, proof of Theorem 1.1]; for negative y it is the bound ln (1 + η) ≥ η - η ^ 2 used in the proof of Theorem 2.1.
• Real.exp_neg_le_one_sub_add_sq: exp (-y) ≤ 1 - y + y ^ 2 for -1 ≤ y, the estimate behind the Hedge bound [AroraHazanKale2012, §2.1, Theorem 2.3].

Main results

• Real.neg_sub_sq_le_log_one_sub: -y - y ^ 2 ≤ log (1 - y) for y ≤ 1 / 2.
• Real.exp_neg_le_one_sub_add_sq: exp (-y) ≤ 1 - y + y ^ 2 for -1 ≤ y.

References

• S. Arora, E. Hazan, S. Kale, The Multiplicative Weights Update Method: a Meta-Algorithm and Applications

theorem Real.neg_sub_sq_le_log_one_sub {y : ℝ} (hy : y ≤ 1 / 2) : -y - y ^ 2 ≤ log (1 - y)

-y - y ^ 2 ≤ log (1 - y) for y ≤ 1 / 2. With y = η ∈ [0, 1 / 2] this is -ln (1 - η) ≤ η + η ^ 2 [AroraHazanKale2012, §1.1].

theorem Real.exp_neg_le_one_sub_add_sq {y : ℝ} (hy : -1 ≤ y) : exp (-y) ≤ 1 - y + y ^ 2

exp (-y) ≤ 1 - y + y ^ 2 for -1 ≤ y: for |y| ≤ 1 from the second-order bound Real.abs_exp_sub_one_sub_id_le, and for y > 1 because exp (-y) ≤ 1 ≤ 1 - y + y ^ 2.