OAI/MeasureTheory/Falconer/Geometry/TwoProjectionPiecePair.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The first auxiliary pair and its inherited root geometry

  1. def OAI.Falconer.TwoProjectionPieces.firstPair line 17
  2. theorem OAI.Falconer.TwoProjectionPieces.first_support_left line 50
  3. theorem OAI.Falconer.TwoProjectionPieces.first_support_right line 56
  4. theorem OAI.Falconer.TwoProjectionPieces.first_noncharging line 62
  5. theorem OAI.Falconer.TwoProjectionPieces.first_pair_separation line 70
  6. theorem OAI.Falconer.TwoProjectionPieces.second_direction_lower line 81