OAI/MeasureTheory/FalconerCompletion/Angular/TensorCapTsupportCoord.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Angular cutoffs and derivative estimates.

  1. lemma OAI.GraphLiteralSupport.CurrentFalconer.tensorCapND_tsupport_coord line 18
  2. def OAI.GraphLiteralSupport.CurrentFalconer.localCapGridND line 25
  3. lemma OAI.GraphLiteralSupport.CurrentFalconer.localCapGridND_card line 29
  4. lemma OAI.GraphLiteralSupport.CurrentFalconer.tensorCapND_support_label line 37
  5. lemma OAI.GraphLiteralSupport.CurrentFalconer.tensorCapND_overlap line 52
  6. def OAI.GraphLiteralSupport.CurrentFalconer.selectedCapND line 61
  7. lemma OAI.GraphLiteralSupport.CurrentFalconer.selectedCapND_contDiff line 64
  8. lemma OAI.GraphLiteralSupport.CurrentFalconer.selectedCapND_bounds line 67
  9. lemma OAI.GraphLiteralSupport.CurrentFalconer.selectedCapND_derivative_bound line 75
  10. lemma OAI.GraphLiteralSupport.CurrentFalconer.fullCapGridND_card_bound line 102
  11. lemma OAI.GraphLiteralSupport.CurrentFalconer.selectedCapND_tsupport line 132
  12. def OAI.GraphLiteralSupport.CurrentFalconer.maskCapSelectionND line 139
  13. def OAI.GraphLiteralSupport.CurrentFalconer.bufferedMaskND line 143
  14. lemma OAI.GraphLiteralSupport.CurrentFalconer.bufferedMaskND_contDiff line 146
  15. lemma OAI.GraphLiteralSupport.CurrentFalconer.bufferedMaskND_bounds line 149
  16. lemma OAI.GraphLiteralSupport.CurrentFalconer.bufferedMaskND_eq_one line 154
  17. lemma OAI.GraphLiteralSupport.CurrentFalconer.bufferedMaskND_support_near line 163
  18. def OAI.GraphLiteralSupport.CurrentFalconer.evenBufferedMaskND line 176
  19. lemma OAI.GraphLiteralSupport.CurrentFalconer.evenBufferedMaskND_contDiff line 180
  20. lemma OAI.GraphLiteralSupport.CurrentFalconer.evenBufferedMaskND_even line 185
  21. lemma OAI.GraphLiteralSupport.CurrentFalconer.evenBufferedMaskND_bounds line 190
  22. lemma OAI.GraphLiteralSupport.CurrentFalconer.evenBufferedMaskND_eq_one line 198
  23. lemma OAI.GraphLiteralSupport.CurrentFalconer.evenBufferedMaskND_support_near line 206
  24. lemma OAI.GraphLiteralSupport.CurrentFalconer.smooth_reflect_derivative_boundND line 221
  25. lemma OAI.GraphLiteralSupport.CurrentFalconer.evenBufferedMaskND_derivative_bound line 234