OAI/MeasureTheory/FalconerCompletion/Graphs/GraphChildSquare.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Graph energies and pair estimates.

  1. def OAI.Attempt4Near.graphChildSquareND line 17
  2. lemma OAI.Attempt4Near.graphChildSquareND_integrable line 21
  3. lemma OAI.Attempt4Near.graphChildSquareND_integral line 36
  4. def OAI.Attempt4Near.graphRetainedCrossedND line 52
  5. lemma OAI.Attempt4Near.graphRetainedCrossedND_angular_bound line 60
  6. theorem OAI.Attempt4Near.graphRetainedCrossedND_integral_bound line 92
  7. def OAI.Attempt4Near.graphRetainedDirectND line 138
  8. lemma OAI.Attempt4Near.graphRetainedDirectND_angular_bound line 146
  9. theorem OAI.Attempt4Near.graphRetainedDirectND_integral_bound line 176
  10. lemma OAI.Attempt4Near.graph_four_sumND line 223
  11. lemma OAI.Attempt4Near.graphRetainedDirectND_complete line 232
  12. lemma OAI.Attempt4Near.graphRetainedCrossedND_complete line 244
  13. lemma OAI.Attempt4Near.graphExpandedDirectND_integral line 257
  14. lemma OAI.Attempt4Near.graphExpandedCrossedND_integral line 274
  15. lemma OAI.Attempt4Near.graph_integral_sum_truncateND line 305
  16. lemma OAI.Attempt4Near.graph_integral_localizationND line 325