OAI/MeasureTheory/Falconer/Radial/MiddleRadialTransport.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Geometric data for middle-interval pruning after cell normalization

  1. theorem OAI.Falconer.radialZoom_quarter_bound line 12
  2. theorem OAI.Falconer.radialZoom_pin_distance line 19
  3. theorem OAI.Falconer.radialZoom_pair_ae_bound line 24
  4. theorem OAI.Falconer.radialZoom_reverse_slab line 33