OAI/MeasureTheory/Falconer/Geometry/TwoProjectionPieces.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Positive compact pieces in the normalized two-projection frame

  1. structure OAI.Falconer.TwoProjectionPieces line 11
  2. theorem OAI.Falconer.exists_two_projection_pieces line 35
  3. def OAI.Falconer.TwoProjectionPieces.left line 46
  4. def OAI.Falconer.TwoProjectionPieces.right line 49
  5. theorem OAI.Falconer.TwoProjectionPieces.left_support line 52
  6. theorem OAI.Falconer.TwoProjectionPieces.right_support line 55
  7. theorem OAI.Falconer.TwoProjectionPieces.left_support_compact line 58
  8. theorem OAI.Falconer.TwoProjectionPieces.right_support_compact line 61
  9. theorem OAI.Falconer.TwoProjectionPieces.left_ac line 64
  10. theorem OAI.Falconer.TwoProjectionPieces.right_ac line 67
  11. theorem OAI.Falconer.TwoProjectionPieces.first_lower line 70
  12. def OAI.Falconer.TwoProjectionPieces.constant line 79
  13. theorem OAI.Falconer.TwoProjectionPieces.constant_pos line 83
  14. theorem OAI.Falconer.TwoProjectionPieces.projected_frostman line 87