OAI/Combinatorics/ProgressionColoring/CoshBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The fair-bit exponential moment bound

Finite Taylor approximations with proved remainder bounds suffice for the parameter used in the fair-bit tail bound.

  1. theorem OAI.QuantitativeVanDerWaerden.cosh_half_le_exp_eighth line 17

    Source documentation

    The exponential moment bound at the fair-bit tail parameter.

    theorem cosh_half_le_exp_eighth : Real.cosh (1 / 2 : ℝ) ≤ Real.exp (1 / 8 : ℝ) := by
…