OAI/MeasureTheory/Falconer/Radial/ScalarAffineFibers.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A separated family of scalar parameters cannot have many nearly vanishing affine values. This controls projection-collision fibers.

  1. theorem OAI.Falconer.scalar_affine_fiber_diameter line 9
  2. theorem OAI.Falconer.scalar_affine_fiber_card line 19
  3. theorem OAI.Falconer.scalar_projection_collision_parameter_card line 42
  4. theorem OAI.Falconer.scalar_projection_collision_parameter_bound line 58