OAI/MeasureTheory/FalconerCompletion/Graphs/SphereAxisIntegralZero.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Graph energies and pair estimates.

  1. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereAxisIntegralND_zeroND line 19
  2. theorem OAI.GraphLiteralSupport.Attempt4FullFar.sphere_noncomparable_zero_rapidND line 23
  3. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphere_radial_pair_swap_normND line 43
  4. theorem OAI.GraphLiteralSupport.Attempt4FullFar.original_far_noncomparable_pointND line 54
  5. theorem OAI.GraphLiteralSupport.Attempt4FullFar.sphere_noncomparable_zero_rapid_euclideanND line 111
  6. lemma OAI.GraphLiteralSupport.Attempt4FullFar.euclidean_radial_pair_swap_normND line 137
  7. theorem OAI.GraphLiteralSupport.Attempt4FullFar.euclidean_far_noncomparable_pointND line 148