OAI/MeasureTheory/Falconer/Estimates/PlanarGainNumerics.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Absorbing the explicit losses in the planar measure obstruction

Only fixed constants, logarithms and ceilings are absorbed here. The underlying incidence estimate has already been proved from the cited published input.

  1. theorem OAI.Falconer.samplingBallLoss_le line 17
  2. theorem OAI.Falconer.rpow_absorb_constant line 25
  3. theorem OAI.Falconer.sampling_point_loss_le line 31
  4. theorem OAI.Falconer.sampling_direction_loss_le line 46
  5. structure OAI.Falconer.PlanarSamplingReady line 58
  6. theorem OAI.Falconer.eventually_planarSamplingReady line 69