OAI/MeasureTheory/Falconer/Radial/RadialCollisionDeletion.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Threshold deletion for the full conditional radial collision mass

  1. theorem OAI.Falconer.radial_collision_pair_integral line 14
  2. theorem OAI.Falconer.radial_collision_bad_mass line 27
  3. theorem OAI.Falconer.radial_collision_pruning line 48