OAI/MeasureTheory/FalconerCompletion/Angular/CoordNormBound2.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Angular cutoffs and derivative estimates.

  1. lemma OAI.GraphLiteralSupport.CurrentFalconer.coord_norm_boundND line 21
  2. def OAI.GraphLiteralSupport.CurrentFalconer.tensorCapKernelND line 39
  3. lemma OAI.GraphLiteralSupport.CurrentFalconer.tensorCapKernelND_contDiff line 42
  4. lemma OAI.GraphLiteralSupport.CurrentFalconer.tensorCapKernelND_nonneg line 47
  5. lemma OAI.GraphLiteralSupport.CurrentFalconer.tensorCapKernelND_le_one line 51
  6. lemma OAI.GraphLiteralSupport.CurrentFalconer.tensorCapKernelND_support line 56
  7. lemma OAI.GraphLiteralSupport.CurrentFalconer.tensorCapKernelND_compact line 63
  8. lemma OAI.GraphLiteralSupport.CurrentFalconer.tensorCapKernelND_derivative_bound line 71
  9. def OAI.GraphLiteralSupport.CurrentFalconer.tensorCapND line 83
  10. lemma OAI.GraphLiteralSupport.CurrentFalconer.tensorCapND_apply line 87
  11. lemma OAI.GraphLiteralSupport.CurrentFalconer.tensorCapND_contDiff line 91
  12. lemma OAI.GraphLiteralSupport.CurrentFalconer.tensorCapND_derivative_bound line 95