OAI/MeasureTheory/Falconer/Estimates/RotatedTubeData.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Rotation of the original measurable tube relation and its finite labels

  1. def OAI.Falconer.rotatedTubeRelation line 11
  2. theorem OAI.Falconer.rotatedTubeRelation_measurable line 15
  3. theorem OAI.Falconer.rotatedTubeRelation_point_bound line 20
  4. theorem OAI.Falconer.rotatedTubeRelation_cover line 28
  5. theorem OAI.Falconer.rotated_point_norm_ae line 42
  6. theorem OAI.Falconer.rotated_direction_cap_ae line 49