OAI/Analysis/LipschitzHilbert/Estimates/GlobalTopBoxes.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Glue the measurable box exceptions across the full plane, retaining both the summable area estimate and polynomial decay away from the top.

  1. theorem OAI.LipschitzHilbert.floor_box_mem_Ico line 14
  2. theorem OAI.LipschitzHilbert.global_top_box_gluing line 21