OAI/Analysis/PathSelection/AnalyticFactors.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Normal root limits and algebraic factorization of analytic scalar families.

  1. theorem OAI.DegeneratingTrees.analyticOrderAt_polynomial_eval line 18
  2. theorem OAI.DegeneratingTrees.analytic_polynomial_cluster line 30
  3. lemma OAI.DegeneratingTrees.ScalarEvaluation.lift_monic_polynomial line 70
  4. lemma OAI.DegeneratingTrees.ScalarEvaluation.factor_of_finite_coeff_limits line 106
  5. lemma OAI.DegeneratingTrees.proper_root_cluster line 197
  6. lemma OAI.DegeneratingTrees.rescale_monic_eq line 227
  7. lemma OAI.DegeneratingTrees.rescale_monic_irreducible line 243
  8. lemma OAI.DegeneratingTrees.irreducible_no_proper_monic_factor line 252