OAI/MeasureTheory/FalconerCompletion/Graphs/NormIteratedFDerivSmoothStar.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Graph energies and pair estimates.

  1. lemma OAI.GraphLiteralSupport.CurrentFalconer.norm_iteratedFDeriv_smoothStarND line 22
  2. lemma OAI.GraphLiteralSupport.CurrentFalconer.tsupport_smoothStarND line 32
  3. def OAI.GraphLiteralSupport.CurrentFalconer.pairSmoothSymbolsND line 38
  4. lemma OAI.GraphLiteralSupport.CurrentFalconer.pairSmoothSymbolsND_support line 41
  5. lemma OAI.GraphLiteralSupport.CurrentFalconer.pairSmoothSymbolsND_derivatives line 50
  6. lemma OAI.GraphLiteralSupport.CurrentFalconer.pairSmoothSymbolsND_measurable line 58
  7. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualPairSourceSymbol line 82
  8. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualPairSourceSymbol_measurable line 90
  9. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualPairAmbientGood line 101
  10. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualPairAmbientGood_even line 107
  11. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualPairAmbientGood_measurable line 115
  12. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.uniform_actualPairSourceSymbol_support line 131
  13. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.uniform_actualPairSourceSymbol_derivatives line 156