OAI/MeasureTheory/FalconerCompletion/Graphs/FarPairDirectionMeasurable.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Graph energies and pair estimates.

  1. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualFar_pairDirection_measurable line 24
  2. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualPairAmbientGood_radial_measurable line 29
  3. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualFar_scale_eq line 43
  4. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actual_fullFar_symbol_package line 46