OAI/MeasureTheory/Falconer/Geometry/CommonProjectionLosses.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A single weak constant controls every loss from selecting the common projection bases and restricting to their intersection.

  1. theorem OAI.Falconer.common_projection_losses line 9
  2. theorem OAI.Falconer.common_projection_direction_count line 32