OAI/MeasureTheory/Falconer/Radial/MiddleHeavyRadialMass.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A good witness controls the full conditional heavy radial fiber

  1. theorem OAI.Falconer.radial_collision_le_tube_mass line 14
  2. theorem OAI.Falconer.middle_heavy_radial_mass_lt line 36