OAI/Analysis/LipschitzHilbert/Estimates/GeometricTailExponential.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A geometric distribution bound gives an exponential moment by summing the level strips. The factor is absolute and no boundedness hypothesis is needed for the function.

  1. theorem OAI.LipschitzHilbert.geometric_tail_exponential line 20