OAI/MathematicalPhysics/DefocusingNLS/Certificates/RectangleFiniteFactor.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Polynomial factorization and its boundary logarithmic derivative

  1. def OAI.DefocusingNLS.countingDivisorFactor line 11
  2. theorem OAI.DefocusingNLS.countingDivisorFactor_analytic line 14
  3. theorem OAI.DefocusingNLS.countingDivisorFactor_eq_finprod line 20
  4. theorem OAI.DefocusingNLS.rectangle_finite_factorization line 38
  5. theorem OAI.DefocusingNLS.countingDivisorFactor_ne_zero line 50
  6. theorem OAI.DefocusingNLS.countingDivisorFactor_logDeriv line 60