OAI/Analysis/LipschitzHilbert/Estimates/TopWeakTwo.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual top count satisfies weak L2 once the geometric dilation packing bounds are available. This is the final analytic part of the popular-top counting argument, with no dependence on the number of tops.

  1. theorem OAI.LipschitzHilbert.top_count_weak_two_of_dilations line 15