OAI/Analysis/LipschitzHilbert/Geometry/LaceyLiPacking.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Weighted distribution bounds for disjoint popularity witnesses, derived directly from the cited finite-rectangle Lacey--Li input.

  1. theorem OAI.LipschitzHilbert.laceyLi_weighted_tail line 13
  2. theorem OAI.LipschitzHilbert.laceyLi_weighted_tail_fintype line 65