OAI/Analysis/LipschitzHilbert/Estimates/TopShape.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The exact top shape from (src-5) and its seventh-power decay outside the mask's near region.

  1. def OAI.LipschitzHilbert.topShape line 12
  2. theorem OAI.LipschitzHilbert.topShape_nonneg line 15
  3. theorem OAI.LipschitzHilbert.topShape_le line 19
  4. theorem OAI.LipschitzHilbert.topShape_far_seventh line 26