OAI/Analysis/LipschitzHilbert/Estimates/RestrictedTopWeakTwo.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Restricted testing gives the top-count bound on the localization strip, without extending the short-side geometry beyond that strip.

  1. theorem OAI.LipschitzHilbert.top_count_weak_two_on_set line 13