OAI/MeasureTheory/FalconerCompletion/Graphs/GraphDegrees.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Graph energies and pair estimates.

  1. theorem OAI.CurrentFalconer.TreeND.source_graph_degrees line 21
  2. theorem OAI.CurrentFalconer.zero_cap_energy_transform line 82
  3. lemma OAI.CurrentFalconer.cap_energy_nonneg line 123
  4. theorem OAI.CurrentFalconer.nonpositive_cap_pair_zero line 134
  5. def OAI.Attempt4Near.sourceAngularMomentND line 165
  6. def OAI.Attempt4Near.sourceAngularHND line 168
  7. def OAI.Attempt4Near.sourceAngularHFND line 173
  8. lemma OAI.Attempt4Near.graph_radial_normalizationND line 178
  9. lemma OAI.Attempt4Near.sourceAngularHND_normalized line 187
  10. lemma OAI.Attempt4Near.sourceAngularHFND_normalized line 197
  11. lemma OAI.Attempt4Near.sourceAngularMomentND_measurable line 204
  12. lemma OAI.Attempt4Near.sourceAngularMomentND_nonneg line 208
  13. lemma OAI.Attempt4Near.sourceAngularMomentND_bound line 211
  14. lemma OAI.Attempt4Near.angular_square_integrableND line 221
  15. lemma OAI.Attempt4Near.graph_weighted_moments_integrableND line 229
  16. lemma OAI.Attempt4Near.sourceAngularMomentND_pair line 248
  17. theorem OAI.Attempt4Near.finset_bipartite_schur line 265
  18. lemma OAI.Attempt4Near.graph_discarded_sumND line 293
  19. lemma OAI.Attempt4Near.graph_complex_schurND line 311
  20. lemma OAI.Attempt4Near.graph_partition_schurND line 328
  21. lemma OAI.Attempt4Near.graph_product_square_sumND line 346
  22. lemma OAI.Attempt4Near.graph_partition_product_schurND line 357
  23. lemma OAI.Attempt4Near.graph_pair_partitionND line 371