OAI/MeasureTheory/Falconer/Radial/ReverseRadialGeometry.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Reverse radial caps bound collisions of original source directions

  1. theorem OAI.Falconer.unit_perpendicular_norm_symm line 12
  2. theorem OAI.Falconer.perpendicularPart_neg_left line 21
  3. theorem OAI.Falconer.reverse_radial_angle_identity line 25
  4. theorem OAI.Falconer.reverse_radial_collision_angle line 42