OAI/Analysis/LipschitzHilbert/Estimates/TopThreshold.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A fixed polynomial threshold pays for both the raw packet constant and the moment order, before choosing any finite family or later mask.

  1. theorem OAI.LipschitzHilbert.topAreaPrefactor_one_le line 12
  2. theorem OAI.LipschitzHilbert.topAreaPrefactor_scale line 16
  3. theorem OAI.LipschitzHilbert.topExceptionMoment_power_le line 21
  4. theorem OAI.LipschitzHilbert.exists_top_threshold line 48