OAI/MeasureTheory/FalconerCompletion/Graphs/PairAmbientGoodRadialIffDistanceGood.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Graph energies and pair estimates.

  1. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualPairAmbientGood_radial_iff_distanceGood line 25
  2. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualGridPair_restrict_good line 42
  3. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.gridPairMeasureND_eq_stateCellPair line 62
  4. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualFar_count_eq_coincidence line 72
  5. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.exists_treePath_of_ambientDescendant line 110
  6. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualChildState line 136
  7. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.occupiedFarPair_actual_state line 141