OAI/MeasureTheory/FalconerCompletion/Graphs/SuffixDescendants.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Graph energies and pair estimates.

  1. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.suffixDescendants line 27
  2. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.suffixDescendants_subset line 31
  3. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.suffixDescendants_cover line 37
  4. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.suffixDescendants_disjoint line 59
  5. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.suffix_descendant_measure_split line 67
  6. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.suffixRectangles line 81
  7. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.suffixRetained line 84
  8. abbrev OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.suffixData line 89
  9. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.suffixFullDistance line 92
  10. instance OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.suffixFullDistance_finite line 95
  11. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.suffix_retained_spec line 100
  12. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.cellPair_split_suffix line 111
  13. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.pair_zero_of_no_witness line 125
  14. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.pair_split_retained line 138
  15. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.distance_split_retained line 152
  16. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.suffix_full_pair_le_coarse line 159
  17. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.suffix_full_distance_le_coarse line 185
  18. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.suffix_distance_variation line 198
  19. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.distance_bin_witness line 214
  20. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.shared_bin_full_coarse_collision line 223
  21. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.suffix_normalization_ratio line 261
  22. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.coincidence_le_bin_sq line 273
  23. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.uniform_actual_suffix_reduction line 282