OAI/Algebra/Determinantal/BorderPolars.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PermanentBorder.PolarAnalysis.polynomialSystem line 12
  2. def OAI.PermanentBorder.PolarAnalysis.coefficientSystem line 15
  3. theorem OAI.PermanentBorder.PolarAnalysis.contDiff_coefficientSystem line 20
  4. theorem OAI.PermanentBorder.PolarAnalysis.coefficientSystem_eq line 31
  5. def OAI.PermanentBorder.PolarAnalysis.SimplePolynomialZero line 47
  6. theorem OAI.PermanentBorder.PolarAnalysis.coefficient_limit_simple_zeros line 50
  7. theorem OAI.PermanentBorder.PolarAnalysis.HasBorderDeterminant.exists_simple_approximant line 91
  8. def OAI.PermanentBorder.Polar.affineChartSubstitution line 110
  9. lemma OAI.PermanentBorder.Polar.eval_affineChartSubstitution line 116
  10. def OAI.PermanentBorder.Polar.polarOperator line 134
  11. lemma OAI.PermanentBorder.Polar.polarOperator_eq line 138
  12. def OAI.PermanentBorder.Polar.affinePolarOperators line 142
  13. lemma OAI.PermanentBorder.Polar.polynomialSystem_affinePolarOperators line 148
  14. theorem OAI.PermanentBorder.Polar.HasBorderDeterminant.simple_polar_approximant line 160
  15. lemma OAI.PermanentBorder.Polar.derivative_polar line 187
  16. lemma OAI.PermanentBorder.Polar.polarPair_polynomialSystem line 193
  17. lemma OAI.PermanentBorder.Polar.affineNormChart_add line 205
  18. lemma OAI.PermanentBorder.Polar.eval_matrix line 215
  19. lemma OAI.PermanentBorder.Polar.simple_conjugate line 231
  20. theorem OAI.PermanentBorder.Polar.HasBorderDeterminant.polar_count line 245
  21. theorem OAI.PermanentBorder.Polar.factorial_exp_lower line 294
  22. theorem OAI.PermanentBorder.Polar.choose_exp_bound line 306
  23. theorem OAI.PermanentBorder.Polar.smooth_count_numerical_bound line 317
  24. theorem OAI.PermanentBorder.HasBorderDeterminant.rename line 362
  25. lemma OAI.PermanentBorder.Polar.smooth_rename line 375
  26. theorem OAI.PermanentBorder.Polar.HasBorderDeterminant.smooth_lower_bound line 391