OAI/MeasureTheory/FalconerCompletion/Graphs/SmoothReciprocalNormCompBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Graph energies and pair estimates.

  1. lemma OAI.Attempt4FullFar.smoothReciprocal_norm_comp_bound line 16
  2. lemma OAI.Attempt4FullFar.angularDerivative_uniform_bound line 52
  3. lemma OAI.Attempt4FullFar.sphere_product_derivative_bound line 91