OAI/MeasureTheory/FalconerCompletion/Angular/AngularWordOperatorBound.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Angular cutoffs and derivative estimates.

  1. lemma OAI.GraphLiteralSupport.CurrentFalconer.angularWordOperatorND_bound line 24
  2. lemma OAI.GraphLiteralSupport.CurrentFalconer.normalizedAngularWordND_bound line 46
  3. lemma OAI.GraphLiteralSupport.CurrentFalconer.normalizedAngularWordND_finite_bound line 67
  4. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualEndpointSmooth line 94
  5. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualEndpointSmooth_support line 100
  6. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualEndpointSmooth_derivative_norm line 110
  7. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualEndpointAngular line 119
  8. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualEndpointAngular_derivatives line 127
  9. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.uniform_actualEndpointAngular_support line 147
  10. lemma OAI.GraphLiteralSupport.CurrentFalconer.angularDerivativeND_star line 186
  11. lemma OAI.GraphLiteralSupport.CurrentFalconer.angularDerivativeND_even line 192
  12. def OAI.GraphLiteralSupport.CurrentFalconer.smoothStarND line 205
  13. lemma OAI.GraphLiteralSupport.CurrentFalconer.angularWordOperatorND_star line 211
  14. lemma OAI.GraphLiteralSupport.CurrentFalconer.angularWordOperatorND_even line 221
  15. lemma OAI.GraphLiteralSupport.CurrentFalconer.normalizedAngularWordND_even line 228
  16. lemma OAI.GraphLiteralSupport.CurrentFalconer.normalizedAngularWordND_star line 235