OAI/Analysis/LipschitzHilbert/Estimates/WeightedExceptionalArea.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Raising the box threshold by the reciprocal lattice weight gives summable exceptional areas, with a fixed spatial decay order.

  1. theorem OAI.LipschitzHilbert.weighted_quarter_area_of_even_moment line 15
  2. theorem OAI.LipschitzHilbert.weighted_quarter_area_le line 33
  3. theorem OAI.LipschitzHilbert.boxVariationWeight_le_one line 43
  4. theorem OAI.LipschitzHilbert.global_weighted_even_moment_area line 50