OAI/MeasureTheory/FalconerCompletion/Graphs/GraphChildrenHSplit.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Graph energies and pair estimates.

  1. lemma OAI.CurrentFalconer.TreeND.graph_children_H_split line 22
  2. lemma OAI.CurrentFalconer.TreeND.graph_children_HF_split line 42
  3. lemma OAI.CurrentFalconer.TreeND.graph_direct_product_identity line 63
  4. lemma OAI.CurrentFalconer.TreeND.graph_crossed_product_identity line 69
  5. lemma OAI.CurrentFalconer.TreeND.graph_direct_cell_integrable line 75
  6. lemma OAI.CurrentFalconer.TreeND.graph_crossed_cell_integrable line 117
  7. lemma OAI.CurrentFalconer.TreeND.graphCapScale_pos line 178
  8. lemma OAI.CurrentFalconer.TreeND.graphCapScale_eq line 181
  9. lemma OAI.CurrentFalconer.TreeND.graph_pair_partition_ae line 185
  10. theorem OAI.CurrentFalconer.TreeND.source_graph_cap_degrees line 200
  11. lemma OAI.CurrentFalconer.TreeND.graph_profile_ratio line 244
  12. lemma OAI.CurrentFalconer.TreeND.graph_profile_label_exponent line 253
  13. lemma OAI.CurrentFalconer.TreeND.graphChildren_card_crude line 261
  14. lemma OAI.CurrentFalconer.TreeND.graphCellLaw_mass_crude line 272
  15. lemma OAI.CurrentFalconer.TreeND.graph_profile_ratio_crude line 282