OAI/MeasureTheory/FalconerCompletion/Graphs/LiteralDyadicPaths.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Graph energies and pair estimates.

  1. lemma OAI.CurrentFalconer.TreeND.literal_dyadicPaths line 21
  2. lemma OAI.CurrentFalconer.TreeND.literal_pathIndex line 26
  3. lemma OAI.CurrentFalconer.TreeND.literal_treeCell line 34
  4. lemma OAI.CurrentFalconer.TreeND.literal_treeCenter line 39
  5. lemma OAI.CurrentFalconer.TreeND.literal_fullParallelCount line 44
  6. lemma OAI.CurrentFalconer.TreeND.literal_occupiedCenterCells line 65
  7. lemma OAI.CurrentFalconer.TreeND.literal_regularizedProfileData_iff line 72
  8. lemma OAI.CurrentFalconer.graph_fixed_radial_budget line 98