OAI/Analysis/PathSelection/PreparationLimits.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Convergence of contour sums, preparation coefficients and division remainders.

  1. lemma OAI.PathSelection.PreparationLimit.tendstoUniformlyOn_circleIntegral line 18
  2. lemma OAI.PathSelection.PreparationLimit.circleIntegral_tendsto line 43
  3. lemma OAI.PathSelection.PreparationLimit.eventual_uniform_nonzero line 58
  4. lemma OAI.PathSelection.PreparationLimit.tendstoPowerSum line 74
  5. lemma OAI.PathSelection.PreparationLimit.tendsto_newtonEsymm line 110
  6. lemma OAI.PathSelection.PreparationLimit.eventually_count_eq line 129
  7. lemma OAI.PathSelection.PreparationLimit.const_locallyUniform line 148
  8. lemma OAI.PathSelection.PreparationLimit.tendsto_preparation_coeff line 156
  9. lemma OAI.PathSelection.PreparationLimit.locallyUniform_finset_sum line 170
  10. lemma OAI.PathSelection.PreparationLimit.tendsto_preparation_eval line 183
  11. theorem OAI.PathSelection.PreparationLimit.tendsto_divisionQuotient line 200
  12. lemma OAI.PathSelection.PreparationLimit.tendsto_weighted_ratio_integral line 265
  13. theorem OAI.PathSelection.PreparationLimit.tendsto_divisionRemainder_coeff line 297
  14. theorem OAI.PathSelection.PreparationLimit.exists_preparation_circle line 329
  15. lemma OAI.PathSelection.PreparationLimit.analyticOnNhd_iteratedDeriv line 374
  16. lemma OAI.PathSelection.PreparationLimit.tendstoLocallyUniformlyOn_iteratedDeriv line 382