OAI/MeasureTheory/Falconer/Geometry/CommonUnbalancedProjections.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Common reference projection bounds with an explicit cardinality-ratio loss. This avoids padding the actual planar coordinate sets.

  1. theorem OAI.Falconer.common_unbalanced_ratio_projections line 10