OAI/Analysis/LipschitzHilbert/Estimates/AmplitudeAllWeights.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

All finite collections of actual amplitude levels split into the retained logarithmic cost and the two exponentially small mass tails.

  1. def OAI.LipschitzHilbert.amplitudeTailCost line 14
  2. theorem OAI.LipschitzHilbert.amplitudeLevel_all_weights line 17