OAI/MeasureTheory/FalconerCompletion/Graphs/AngularMoment.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Graph energies and pair estimates.

  1. def OAI.GraphLiteralSupport.Attempt4Near.sourceAngularMomentND line 20
  2. def OAI.GraphLiteralSupport.Attempt4Near.sourceAngularHND line 23
  3. def OAI.GraphLiteralSupport.Attempt4Near.sourceAngularHFND line 28
  4. lemma OAI.GraphLiteralSupport.Attempt4Near.graph_radial_normalizationND line 33
  5. lemma OAI.GraphLiteralSupport.Attempt4Near.sourceAngularHND_normalized line 42
  6. lemma OAI.GraphLiteralSupport.Attempt4Near.sourceAngularHFND_normalized line 52
  7. lemma OAI.GraphLiteralSupport.Attempt4Near.sourceAngularMomentND_measurable line 59
  8. lemma OAI.GraphLiteralSupport.Attempt4Near.sourceAngularMomentND_nonneg line 63
  9. lemma OAI.GraphLiteralSupport.Attempt4Near.sourceAngularMomentND_bound line 66
  10. lemma OAI.GraphLiteralSupport.Attempt4Near.angular_square_integrableND line 76
  11. lemma OAI.GraphLiteralSupport.Attempt4Near.graph_weighted_moments_integrableND line 84
  12. lemma OAI.GraphLiteralSupport.Attempt4Near.sourceAngularMomentND_pair line 103
  13. theorem OAI.GraphLiteralSupport.Attempt4Near.finset_bipartite_schur line 122
  14. lemma OAI.GraphLiteralSupport.Attempt4Near.graph_discarded_sumND line 150
  15. lemma OAI.GraphLiteralSupport.Attempt4Near.graph_complex_schurND line 168
  16. lemma OAI.GraphLiteralSupport.Attempt4Near.graph_partition_schurND line 185
  17. lemma OAI.GraphLiteralSupport.Attempt4Near.graph_product_square_sumND line 203
  18. lemma OAI.GraphLiteralSupport.Attempt4Near.graph_partition_product_schurND line 214
  19. lemma OAI.GraphLiteralSupport.Attempt4Near.graph_pair_partitionND line 228
  20. def OAI.GraphLiteralSupport.Attempt4Near.graphChildSquareND line 248
  21. lemma OAI.GraphLiteralSupport.Attempt4Near.graphChildSquareND_integrable line 252
  22. lemma OAI.GraphLiteralSupport.Attempt4Near.graphChildSquareND_integral line 267
  23. def OAI.GraphLiteralSupport.Attempt4Near.graphRetainedCrossedND line 283
  24. lemma OAI.GraphLiteralSupport.Attempt4Near.graphRetainedCrossedND_angular_bound line 291
  25. theorem OAI.GraphLiteralSupport.Attempt4Near.graphRetainedCrossedND_integral_bound line 323