OAI/NumberTheory/Catalan/Analysis/BlaschkeAnalytic.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InternalCatalan.blaschkeFactor_denominator_ne_zero line 11
  2. theorem OAI.InternalCatalan.blaschkeFactor_imaginary_denominator_ne_zero line 23
  3. theorem OAI.InternalCatalan.blaschkeFactor_imaginary_ne_zero_of_node_ne_zero line 29
  4. theorem OAI.InternalCatalan.blaschkeFactor_analyticAt line 39
  5. theorem OAI.InternalCatalan.finiteBlaschke_analyticAt line 47
  6. theorem OAI.InternalCatalan.finiteBlaschke_analyticOnNhd_closedDisk line 71
  7. theorem OAI.InternalCatalan.finiteBlaschke_imaginary_ne_zero line 79
  8. theorem OAI.InternalCatalan.finiteBlaschke_quotient_analyticAt_imaginary line 86
  9. theorem OAI.InternalCatalan.finiteBlaschke_quotient_analyticOnNhd_imaginary line 97
  10. theorem OAI.InternalCatalan.blaschkeFactor_norm_eq_one line 104
  11. theorem OAI.InternalCatalan.finiteBlaschke_norm_eq_one line 124
  12. theorem OAI.InternalCatalan.finiteBlaschke_eval_node line 132