OAI/Analysis/PathSelection/ContourDivision.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Analytic contour moments and fixed-contour polynomial division.

  1. theorem OAI.DegeneratingTrees.analytic_contourMoment line 19
  2. theorem OAI.DegeneratingTrees.contour_fiber_factorization line 51
  3. theorem OAI.DegeneratingTrees.nat_eq_of_complex_dist_lt_one line 83
  4. theorem OAI.DegeneratingTrees.fixed_circle_data line 94
  5. theorem OAI.DegeneratingTrees.analytic_contourNewtonCoeff line 185
  6. theorem OAI.DegeneratingTrees.analytic_contourPolynomial_coeff line 204
  7. def OAI.DegeneratingTrees.contourPolynomialProfile line 216
  8. theorem OAI.DegeneratingTrees.contourPolynomialProfile_apply line 222
  9. theorem OAI.DegeneratingTrees.analytic_contourPolynomialProfile line 227
  10. def OAI.DegeneratingTrees.cauchyKernelProfile line 240
  11. theorem OAI.DegeneratingTrees.cauchyKernelProfile_apply line 243
  12. theorem OAI.DegeneratingTrees.cauchyKernelProfile_isUnit line 246
  13. theorem OAI.DegeneratingTrees.analytic_cauchyKernelProfile line 257
  14. def OAI.DegeneratingTrees.cauchyTransformProfile line 263
  15. theorem OAI.DegeneratingTrees.analytic_cauchyTransformProfile line 268
  16. theorem OAI.DegeneratingTrees.cauchyTransformProfile_eq line 281
  17. theorem OAI.DegeneratingTrees.fixed_contour_preparation_on_ball line 300
  18. theorem OAI.DegeneratingTrees.fixed_contour_preparation line 380
  19. def OAI.DegeneratingTrees.normalizedCircleFunctional line 391
  20. def OAI.DegeneratingTrees.dividedCoeffProfile line 396
  21. theorem OAI.DegeneratingTrees.dividedCoeffProfile_apply line 402
  22. theorem OAI.DegeneratingTrees.analytic_dividedCoeffProfile line 408
  23. def OAI.DegeneratingTrees.divisionRemainder line 419
  24. theorem OAI.DegeneratingTrees.divisionRemainder_degree_lt line 424
  25. theorem OAI.DegeneratingTrees.analytic_divisionRemainder_coeff line 428
  26. theorem OAI.DegeneratingTrees.eval_sum_of_degree_lt line 441
  27. def OAI.DegeneratingTrees.dividedEvaluationProfile line 448
  28. theorem OAI.DegeneratingTrees.dividedEvaluationProfile_apply line 451
  29. theorem OAI.DegeneratingTrees.divisionRemainder_eval line 465
  30. theorem OAI.DegeneratingTrees.fixed_circle_division line 478