OAI/Analysis/LipschitzHilbert/Geometry/ProjectedPopularityPacking.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual projected-popularity packing estimate for the far-angle rectangle groups, in the finite form needed by the application.

  1. theorem OAI.LipschitzHilbert.projected_popularity_packing line 13