OAI/Analysis/LipschitzHilbert/Estimates/GlobalExceptionalArea.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Sum the decaying top-box exceptional areas over the entire plane. This uses the actual summable lattice weight, rather than discarding the boxes outside the top rectangle.

  1. theorem OAI.LipschitzHilbert.boxVariationWeight_tsum line 16
  2. theorem OAI.LipschitzHilbert.global_exceptional_area line 26