OAI/Analysis/LipschitzHilbert/Estimates/TopAmplitudeBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The explicit top concentration amplitude is at most quadratic in the raw packet constant, uniformly before all finite packet families.

  1. theorem OAI.LipschitzHilbert.topPairConstant_linear line 11
  2. theorem OAI.LipschitzHilbert.PlanarPacketFamily.normalized_coefficient_budget line 20
  3. theorem OAI.LipschitzHilbert.uniform_topPacketAmplitude_bound line 27