OAI/Combinatorics/EditApproximation/Probability/BernsteinEnvelope.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The scalar exponential estimate used to discharge the finite Bernstein input. Its rational majorant is proved by a derivative comparison, avoiding any assumption of a concentration theorem.

  1. def OAI.EditApproximation.bernsteinEnvelope line 11
  2. theorem OAI.EditApproximation.bernsteinEnvelope_deriv line 14
  3. theorem OAI.EditApproximation.bernsteinEnvelope_zero line 26
  4. theorem OAI.EditApproximation.bernsteinEnvelope_one_le line 29
  5. theorem OAI.EditApproximation.exp_le_bernstein_envelope line 53

    Source documentation

    Exact Bernstein exponential majorant, valid for all x < 3.

    theorem exp_le_bernstein_envelope (x : ℝ) (hx : x < 3) :
    Real.exp x ≤ 1 + x + x ^ 2 / (2 * (1 - x / 3)) := by
…