OAI/MeasureTheory/Falconer/Angular/AngularLengthPartition.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarFalconer.angularLengthLeft line 8
  2. def OAI.PlanarFalconer.angularLengthRight line 11
  3. def OAI.PlanarFalconer.angularLengthComparable line 14
  4. def OAI.PlanarFalconer.angularLengthShell line 18
  5. theorem OAI.PlanarFalconer.measurable_angularLengthLeft line 23
  6. theorem OAI.PlanarFalconer.measurable_angularLengthRight line 27
  7. theorem OAI.PlanarFalconer.measurable_angularLengthComparable line 31
  8. theorem OAI.PlanarFalconer.measurable_angularLengthShell line 36
  9. theorem OAI.PlanarFalconer.angular_length_trichotomy line 45
  10. theorem OAI.PlanarFalconer.angular_length_left_right_disjoint line 53
  11. theorem OAI.PlanarFalconer.angular_length_left_comparable_disjoint line 60
  12. theorem OAI.PlanarFalconer.angular_length_right_comparable_disjoint line 64
  13. theorem OAI.PlanarFalconer.angularLengthShell_lengths line 68
  14. theorem OAI.PlanarFalconer.angularLengthShell_disjoint line 80