OAI/MathematicalPhysics/DefocusingNLS/Certificates/IntegerPolynomialDisk.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

+# Interpreting integer disk bounds over the complex numbers

Integer upper and lower coefficient bounds imply the norm inequality required by the disk root theorem.

  1. theorem OAI.DefocusingNLS.SeparatorArithmetic.norm_toComplex_le_upper line 14
  2. theorem OAI.DefocusingNLS.SeparatorArithmetic.lower_le_norm_toComplex line 20
  3. theorem OAI.DefocusingNLS.SeparatorArithmetic.root_of_integer_coefficient_bound line 26