OAI/MathematicalPhysics/DefocusingNLS/Certificates/MatchingPolynomialDegree.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Degree bounds for the zero-tail matching polynomial

  1. theorem OAI.DefocusingNLS.SeparatorArithmetic.length_addCoefficients line 11
  2. theorem OAI.DefocusingNLS.SeparatorArithmetic.length_mulLinear line 20
  3. theorem OAI.DefocusingNLS.SeparatorArithmetic.backwardStep_lengths line 24
  4. theorem OAI.DefocusingNLS.SeparatorArithmetic.backward_fold_lengths line 32
  5. theorem OAI.DefocusingNLS.SeparatorArithmetic.backwardCoefficients_lengths line 44
  6. theorem OAI.DefocusingNLS.SeparatorArithmetic.toPolynomial_natDegree_le line 49
  7. theorem OAI.DefocusingNLS.SeparatorArithmetic.backward_polynomial_product_degree line 56
  8. theorem OAI.DefocusingNLS.SeparatorArithmetic.windingCoefficient_eq_zero line 64