OAI/Analysis/LipschitzHilbert/Geometry/TopDilationPacking.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual intersection averages, weighted by top area, satisfy the cubic dilation testing estimate. No cardinality factor occurs.

  1. theorem OAI.LipschitzHilbert.top_dilation_packing line 15