OAI/Analysis/LipschitzHilbert/Estimates/TopFamilyException.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

One common moment order sums all actual top exceptional sets with the total top area. This is independent of the number of tops.

  1. def OAI.LipschitzHilbert.topExceptionMoment line 14
  2. theorem OAI.LipschitzHilbert.topExceptionMoment_pos line 16
  3. theorem OAI.LipschitzHilbert.top_family_exception_area line 20
  4. theorem OAI.LipschitzHilbert.topExceptionMoment_le line 49