OAI/MeasureTheory/FalconerCompletion/Angular/CoordNormBound.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Angular cutoffs and derivative estimates.

  1. lemma OAI.CurrentFalconer.coord_norm_boundND line 20
  2. def OAI.CurrentFalconer.tensorCapKernelND line 38
  3. lemma OAI.CurrentFalconer.tensorCapKernelND_contDiff line 41
  4. lemma OAI.CurrentFalconer.tensorCapKernelND_nonneg line 46
  5. lemma OAI.CurrentFalconer.tensorCapKernelND_le_one line 50
  6. lemma OAI.CurrentFalconer.tensorCapKernelND_support line 55
  7. lemma OAI.CurrentFalconer.tensorCapKernelND_compact line 62
  8. lemma OAI.CurrentFalconer.tensorCapKernelND_derivative_bound line 70
  9. def OAI.CurrentFalconer.tensorCapND line 82
  10. lemma OAI.CurrentFalconer.tensorCapND_apply line 86
  11. lemma OAI.CurrentFalconer.tensorCapND_contDiff line 90
  12. lemma OAI.CurrentFalconer.tensorCapND_derivative_bound line 94