OAI/Analysis/PathSelection/TaylorCutoffs.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Uniform Taylor cutoffs, compact family holomorphy and moving Taylor polynomials.

  1. def OAI.DegeneratingTrees.TaylorCutoff.extend line 17
  2. lemma OAI.DegeneratingTrees.TaylorCutoff.extend_on line 21
  3. lemma OAI.DegeneratingTrees.TaylorCutoff.extend_continuousOn line 25
  4. def OAI.DegeneratingTrees.TaylorCutoff.circleMap line 35
  5. lemma OAI.DegeneratingTrees.TaylorCutoff.circleMap_eq line 63
  6. lemma OAI.DegeneratingTrees.TaylorCutoff.sphere_ne_zero line 71
  7. lemma OAI.DegeneratingTrees.TaylorCutoff.sphere_sub_ball_ne_zero line 77
  8. def OAI.DegeneratingTrees.TaylorCutoff.tailProfile line 87
  9. def OAI.DegeneratingTrees.TaylorCutoff.tail line 95
  10. lemma OAI.DegeneratingTrees.TaylorCutoff.continuous_tailProfile line 99
  11. lemma OAI.DegeneratingTrees.TaylorCutoff.continuous_tail line 113
  12. theorem OAI.DegeneratingTrees.TaylorCutoff.tail_tendsto line 121
  13. theorem OAI.DegeneratingTrees.TaylorCutoff.tail_tendsto_zero line 133
  14. lemma OAI.DegeneratingTrees.TaylorCutoff.tail_kernel_step line 142
  15. lemma OAI.DegeneratingTrees.TaylorCutoff.tail_step line 147
  16. theorem OAI.DegeneratingTrees.TaylorCutoff.finite_cutoff line 162
  17. lemma OAI.DegeneratingTrees.TaylorCutoff.tail_zero_eq line 175
  18. lemma OAI.DegeneratingTrees.Clock.clm_circleIntegral line 198
  19. lemma OAI.DegeneratingTrees.Clock.compact_family_analyticAt line 206
  20. lemma OAI.DegeneratingTrees.Clock.compact_family_analyticAt_of_joint line 241
  21. def OAI.DegeneratingTrees.TaylorCutoff.scalarTailCLM line 261
  22. def OAI.DegeneratingTrees.TaylorCutoff.shiftedBoundary line 279
  23. lemma OAI.DegeneratingTrees.TaylorCutoff.continuous_shiftedBoundary line 282
  24. lemma OAI.DegeneratingTrees.TaylorCutoff.shift_mem_disc line 286
  25. lemma OAI.DegeneratingTrees.TaylorCutoff.shiftedBoundary_analyticAt line 300
  26. lemma OAI.DegeneratingTrees.TaylorCutoff.local_continuous_extension line 315
  27. theorem OAI.DegeneratingTrees.TaylorCutoff.analytic_moving_taylor line 341