OAI/MeasureTheory/FalconerCompletion/Graphs/GraphFixedAngularBudget.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Graph energies and pair estimates.

  1. lemma OAI.CurrentFalconer.graph_fixed_angular_budget line 16
  2. lemma OAI.CurrentFalconer.graph_cap_with_angular_jet line 29
  3. theorem OAI.CurrentFalconer.graph_cap_four_decay line 55
  4. lemma OAI.CurrentFalconer.graph_four_zero_of_ineligible line 152
  5. lemma OAI.CurrentFalconer.TreeND.graph_cell_cap_ineligible line 195
  6. lemma OAI.CurrentFalconer.TreeND.graph_children_transform_split line 209
  7. def OAI.CurrentFalconer.TreeND.graphDirectCellTerm line 241
  8. def OAI.CurrentFalconer.TreeND.graphCrossedCellTerm line 255
  9. lemma OAI.CurrentFalconer.TreeND.graphDirectCellTerm_eq line 269
  10. lemma OAI.CurrentFalconer.TreeND.graphCrossedCellTerm_eq line 285
  11. lemma OAI.CurrentFalconer.TreeND.graph_direct_ineligible_zero line 302
  12. lemma OAI.CurrentFalconer.TreeND.graph_crossed_ineligible_zero line 334