OAI/MeasureTheory/FalconerCompletion/Graphs/GraphRetainedDirect.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Graph energies and pair estimates.

  1. def OAI.GraphLiteralSupport.Attempt4Near.graphRetainedDirectND line 18
  2. lemma OAI.GraphLiteralSupport.Attempt4Near.graphRetainedDirectND_angular_bound line 26
  3. theorem OAI.GraphLiteralSupport.Attempt4Near.graphRetainedDirectND_integral_bound line 56
  4. lemma OAI.GraphLiteralSupport.Attempt4Near.graph_four_sumND line 105
  5. lemma OAI.GraphLiteralSupport.Attempt4Near.graphRetainedDirectND_complete line 114
  6. lemma OAI.GraphLiteralSupport.Attempt4Near.graphRetainedCrossedND_complete line 126
  7. lemma OAI.GraphLiteralSupport.Attempt4Near.graphExpandedDirectND_integral line 139
  8. lemma OAI.GraphLiteralSupport.Attempt4Near.graphExpandedCrossedND_integral line 156
  9. lemma OAI.GraphLiteralSupport.Attempt4Near.graph_integral_sum_truncateND line 189
  10. lemma OAI.GraphLiteralSupport.Attempt4Near.graph_integral_localizationND line 209
  11. theorem OAI.GraphLiteralSupport.Attempt4Near.graphFiniteDirectEstimateND line 247