OAI/MeasureTheory/FalconerCompletion/Graphs/AngularMoment2.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Graph energies and pair estimates.

  1. def OAI.GraphLiteralSupport.Attempt4PrefixShell.sourceAngularMomentND line 19
  2. def OAI.GraphLiteralSupport.Attempt4PrefixShell.sourceAngularHND line 22
  3. def OAI.GraphLiteralSupport.Attempt4PrefixShell.sourceAngularHFND line 27
  4. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.graph_radial_normalizationND line 32
  5. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.sourceAngularHND_normalized line 41
  6. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.sourceAngularHFND_normalized line 51
  7. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.sourceAngularMomentND_measurable line 58
  8. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.sourceAngularMomentND_nonneg line 62
  9. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.sourceAngularMomentND_bound line 65
  10. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.angular_square_integrableND line 75
  11. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.graph_weighted_moments_integrableND line 83
  12. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.sourceAngularMomentND_pair line 102