Global quadratic upper bound for the negative exponential remainder
ProvedAvramDividend.Classical.exp_neg_sub_one_add_le_sqavram-classicalexponentiallevy-khintchinem2m4real-analysisunbounded-variation
For every nonnegative real u, exp(-u)-1+u is at most u squared.
Preamble
import Mathlib
Formal statement
namespace AvramDividend.Classical
theorem exp_neg_sub_one_add_le_sq (u : ℝ) (hu : 0 ≤ u) :
Real.exp (-u) - 1 + u ≤ u ^ 2 := by
sorry
end AvramDividend.ClassicalSource
Pinned Mathlib quadratic exponential remainder bound on the unit interval, combined with the elementary large-u bound.