OAI/MeasureTheory/FalconerCompletion/Graphs/GraphDescendants.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Graph energies and pair estimates.

  1. def OAI.CurrentFalconer.TreeND.graphDescendants line 18
  2. def OAI.CurrentFalconer.TreeND.graphChildren line 22
  3. lemma OAI.CurrentFalconer.TreeND.graphDescendants_subset line 27
  4. lemma OAI.CurrentFalconer.TreeND.graphDescendants_cover line 33
  5. lemma OAI.CurrentFalconer.TreeND.graphDescendants_disjoint line 55
  6. lemma OAI.CurrentFalconer.TreeND.graphChildren_integral line 63
  7. lemma OAI.CurrentFalconer.TreeND.graphChildren_mass line 82
  8. lemma OAI.CurrentFalconer.TreeND.graphChildren_nonempty line 90
  9. lemma OAI.CurrentFalconer.TreeND.graphChildren_card_le line 99
  10. lemma OAI.CurrentFalconer.TreeND.treeCell_diameter line 125
  11. lemma OAI.CurrentFalconer.TreeND.graphChildren_length line 132
  12. lemma OAI.CurrentFalconer.TreeND.graphChildren_subset line 137
  13. lemma OAI.CurrentFalconer.TreeND.graphChildren_center_error line 142
  14. lemma OAI.CurrentFalconer.TreeND.graphChildren_direct_size line 155
  15. lemma OAI.CurrentFalconer.TreeND.graphChildren_cross_size line 163
  16. lemma OAI.CurrentFalconer.TreeND.graphChildren_profile_card line 178
  17. lemma OAI.CurrentFalconer.TreeND.graphChildren_pair_profile_card line 188
  18. lemma OAI.CurrentFalconer.tensorCapND_nonneg line 216
  19. lemma OAI.CurrentFalconer.tensorCapND_le_one line 219
  20. lemma OAI.CurrentFalconer.sphereCapGridND_card_bound line 222
  21. lemma OAI.CurrentFalconer.sphereCap_pair_partition line 243
  22. structure OAI.CurrentFalconer.GraphSymbolJet line 276
  23. lemma OAI.CurrentFalconer.GraphSymbolJet.norm_le line 283
  24. lemma OAI.CurrentFalconer.graph_uneligible_transform line 287
  25. lemma OAI.CurrentFalconer.TreeND.graphChildren_eligible_iff line 318
  26. lemma OAI.CurrentFalconer.graphCellLaw_four_ae line 341
  27. lemma OAI.CurrentFalconer.graph_radial_budget line 363
  28. lemma OAI.CurrentFalconer.graph_symbol_pair_budget line 387