OAI/Analysis/LipschitzHilbert/Trees/AmplitudeMassTails.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The numerical small- and large-measure tails for the amplitude levels after bin projection. The constants are independent of dimension and of the finite set of retained levels.

  1. theorem OAI.LipschitzHilbert.amplitude_small_mass_tail line 12
  2. theorem OAI.LipschitzHilbert.amplitude_large_mass_tail line 28