OAI/Analysis/LipschitzHilbert/Estimates/DampedSimplexBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The crude analytic bound supplies boundedness on the whole simplex tube. Gaussian decay also extends the vertex estimate from the ball of imaginary radius L² to every imaginary vector, as in manuscript §11.

  1. theorem OAI.LipschitzHilbert.gaussianPhaseDamping_crude_bound line 15
  2. theorem OAI.LipschitzHilbert.damped_simplex_crude_bound line 34
  3. theorem OAI.LipschitzHilbert.eventually_damped_vertex_bound line 52