OAI/Analysis/PathSelection/ContourPreparation.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Fixed-contour preparation polynomials, division and stable root counts.

  1. lemma OAI.PathSelection.Preparation.eqOn_closedBall_of_codiscrete line 16
  2. lemma OAI.PathSelection.Preparation.nonnegative_factor_polynomial line 37
  3. theorem OAI.PathSelection.Preparation.exists_preparation_on_disc line 76
  4. def OAI.PathSelection.Preparation.divisionKernel line 120
  5. lemma OAI.PathSelection.Preparation.divisionKernel_eval line 124
  6. lemma OAI.PathSelection.Preparation.divisionKernel_degree line 143
  7. lemma OAI.PathSelection.Preparation.divisionKernel_continuous line 157
  8. theorem OAI.PathSelection.Preparation.fixed_circle_division line 167
  9. def OAI.PathSelection.Preparation.divisionRemainder line 213
  10. lemma OAI.PathSelection.Preparation.divisionRemainder_degree line 219
  11. lemma OAI.PathSelection.Preparation.divisionRemainder_eval line 233
  12. def OAI.PathSelection.Preparation.divisionQuotient line 260
  13. lemma OAI.PathSelection.Preparation.divisionQuotient_analyticOnNhd line 263
  14. theorem OAI.PathSelection.Preparation.fixed_disc_division line 280
  15. lemma OAI.PathSelection.Preparation.eqOn_deriv_closedBall line 296
  16. lemma OAI.PathSelection.Preparation.circleIntegral_root_sum line 304
  17. theorem OAI.PathSelection.Preparation.polynomial_power_sum_contour line 327
  18. theorem OAI.PathSelection.Preparation.preparation_power_sum_contour line 350
  19. def OAI.PathSelection.Preparation.newtonEsymm line 389
  20. lemma OAI.PathSelection.Preparation.multiset_newton_identity line 396
  21. lemma OAI.PathSelection.Preparation.newtonEsymm_eq line 413
  22. def OAI.PathSelection.Preparation.contourPowerSum line 434
  23. def OAI.PathSelection.Preparation.preparationPolynomial line 438
  24. lemma OAI.PathSelection.Preparation.polynomial_newton_formula line 442
  25. lemma OAI.PathSelection.Preparation.preparationPolynomial_eq line 453
  26. lemma OAI.PathSelection.Preparation.divisionQuotient_eq_unit line 464
  27. theorem OAI.PathSelection.Preparation.fixed_contour_preparation line 486
  28. lemma OAI.PathSelection.Preparation.preparation_zero_count line 511
  29. lemma OAI.PathSelection.Preparation.contour_zero_count_nat line 521
  30. lemma OAI.PathSelection.Preparation.continuousOn_circleIntegral line 528
  31. theorem OAI.PathSelection.Preparation.contour_zero_count_constant line 542
  32. theorem OAI.PathSelection.Preparation.contour_zero_count_eq_of_norm_sub_lt line 565
  33. theorem OAI.PathSelection.Preparation.fixed_contour_preparation_of_count line 611