OAI/MeasureTheory/FalconerCompletion/Graphs/RetainedCenterTests.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Graph energies and pair estimates.

  1. def OAI.CurrentFalconer.TreeND.retainedCenterTests line 20
  2. lemma OAI.CurrentFalconer.TreeND.retainedCenterTests_symm line 24
  3. lemma OAI.CurrentFalconer.TreeND.mem_retainedPairs_iff line 36
  4. def OAI.CurrentFalconer.TreeND.retainedHGraph line 43
  5. def OAI.CurrentFalconer.TreeND.retainedHFGraph line 50
  6. lemma OAI.CurrentFalconer.TreeND.retainedHGraph_row_card line 59
  7. lemma OAI.CurrentFalconer.TreeND.retainedHGraph_col_card line 70
  8. lemma OAI.CurrentFalconer.TreeND.retainedHFGraph_row_card line 80
  9. lemma OAI.CurrentFalconer.TreeND.retainedHFGraph_col_card line 99
  10. def OAI.CurrentFalconer.TreeND.graphDegreeBound line 121
  11. theorem OAI.CurrentFalconer.TreeND.eligibleGraphDegrees line 124
  12. lemma OAI.CurrentFalconer.TreeND.graph_height_mono_left line 189
  13. lemma OAI.CurrentFalconer.TreeND.graph_ancestor_scale line 198
  14. lemma OAI.CurrentFalconer.TreeND.graph_ball_scale line 209
  15. lemma OAI.CurrentFalconer.TreeND.graph_profile_factor_scale line 225
  16. theorem OAI.CurrentFalconer.TreeND.graphDegreeBound_source_scale line 240
  17. lemma OAI.CurrentFalconer.TreeND.graph_width_coverage line 288
  18. lemma OAI.CurrentFalconer.TreeND.graph_testWidth_lower line 316
  19. def OAI.CurrentFalconer.TreeND.graphCapScale line 329
  20. def OAI.CurrentFalconer.TreeND.graphTolerance line 331
  21. lemma OAI.CurrentFalconer.TreeND.graphCapScale_le line 334
  22. lemma OAI.CurrentFalconer.TreeND.graphCapScale_nonneg line 340
  23. lemma OAI.CurrentFalconer.TreeND.graphTolerance_eq line 345
  24. lemma OAI.CurrentFalconer.TreeND.graph_eventually_large line 360
  25. lemma OAI.CurrentFalconer.TreeND.graph_source_degree_scale_absorb line 372
  26. lemma OAI.CurrentFalconer.TreeND.graph_source_width line 393