OAI/MeasureTheory/FalconerCompletion/Estimates/FullParallelCountFilter.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Quantitative estimates for the distance-set construction.

  1. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.fullParallelCount_filter line 22
  2. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.parallel_mean_geometric line 30
  3. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.packing_profile_power line 125
  4. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actual_parallel_mean line 138
  5. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.uniform_actual_parallel_exceptional line 229
  6. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.uniform_actual_exceptional_directions line 300