OAI/Analysis/LipschitzHilbert/Estimates/AmplitudeClassBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Amplitude levels of comparable support measure have a bounded sum-to-energy ratio, independently of their number.

  1. theorem OAI.LipschitzHilbert.amplitude_class_bound line 12