OAI/MeasureTheory/Falconer/Angular/AngularDifferentialExpr.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.PlanarFalconer.AngularDifferentialExpr line 10
  2. def OAI.PlanarFalconer.AngularDifferentialExpr.order line 17
  3. def OAI.PlanarFalconer.AngularDifferentialExpr.apply line 22
  4. def OAI.PlanarFalconer.AngularDifferentialExpr.cost line 27
  5. theorem OAI.PlanarFalconer.AngularDifferentialExpr.cost_nonneg line 32
  6. theorem OAI.PlanarFalconer.AngularDifferentialExpr.smooth_iteratedDeriv line 38
  7. theorem OAI.PlanarFalconer.AngularDifferentialExpr.apply_contDiff line 44
  8. theorem OAI.PlanarFalconer.AngularDifferentialExpr.iteratedDeriv_iterated line 51
  9. theorem OAI.PlanarFalconer.AngularDifferentialExpr.apply_germ line 55
  10. theorem OAI.PlanarFalconer.AngularDifferentialExpr.apply_zero line 64
  11. def OAI.PlanarFalconer.AngularDifferentialExpr.sum line 70
  12. theorem OAI.PlanarFalconer.AngularDifferentialExpr.sum_apply line 74
  13. theorem OAI.PlanarFalconer.AngularDifferentialExpr.sum_order_le line 80