OAI/Analysis/LipschitzHilbert/Estimates/AmplitudeErrorDecay.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The full discarded-amplitude error is smaller than L^-19 for the source's allowed amplitude growth, uniformly over the level cutoffs.

  1. theorem OAI.LipschitzHilbert.retainedAmplitudeCost_le_linear line 11
  2. theorem OAI.LipschitzHilbert.eventually_amplitude_error_decay line 36