OAI/Analysis/LipschitzHilbert/Phase/GaussianPhaseDamping.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Gaussian damping of the finite shift parameters. Its exact norm removes the crude exp(C√L) growth outside the imaginary ball of radius L².

  1. def OAI.LipschitzHilbert.gaussianPhaseDamping line 15
  2. theorem OAI.LipschitzHilbert.gaussianPhaseDamping_norm line 17
  3. theorem OAI.LipschitzHilbert.gaussianPhaseDamping_affine_entire line 28
  4. theorem OAI.LipschitzHilbert.gaussianPhaseDamping_simplex_le line 37
  5. theorem OAI.LipschitzHilbert.eventually_gaussian_imaginary_tail line 47