OAI/MeasureTheory/FalconerCompletion/Estimates/TreeCenter2.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Quantitative estimates for the distance-set construction.

  1. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.treeCenter line 18
  2. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.treeCenter_mem line 21
  3. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.occupiedCenterCells line 24
  4. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.treeCenter_ball_card line 29
  5. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.occupied_center_count_le line 48
  6. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.sourceClass_local_count line 107
  7. structure OAI.GraphLiteralSupport.CurrentFalconer.TreeND.RegularizedProfileData line 148
  8. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actual_profile_regularization line 167