OAI/Analysis/LipschitzHilbert/Estimates/RetainedAmplitudeMatrix.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The retained pair sum loses only one logarithmic factor, as in the source amplitude reduction. This concerns the actual measurable levels.

  1. def OAI.LipschitzHilbert.retainedAmplitudeCost line 12
  2. theorem OAI.LipschitzHilbert.retained_amplitude_matrix_bound line 15