OAI/MeasureTheory/Falconer/Incidence/AngularTubeCount.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The mean and exceptional mass of a finite original tube count

  1. def OAI.Falconer.angularTubeEvent line 12
  2. theorem OAI.Falconer.angularTubeEvent_measurable line 15
  3. def OAI.Falconer.finiteTubeCount line 21
  4. theorem OAI.Falconer.finiteTubeCount_eq_sum line 26
  5. theorem OAI.Falconer.finiteTubeCount_measurable line 33
  6. theorem OAI.Falconer.finiteTubeCount_mean line 40
  7. theorem OAI.Falconer.finiteTubeCount_exceptional line 51
  8. theorem OAI.Falconer.finiteTubeCount_mean_bound line 64