OAI/MathematicalPhysics/DefocusingNLS/Certificates/RootDiskArithmetic.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Rational disk data for the degree-fifteen separator polynomials

Centers are Gaussian integers divided by one million; disk radius is 100 / 1000000. The coefficient bounds are exact integer inequalities.

  1. def OAI.DefocusingNLS.SeparatorArithmetic.diskScale line 14
  2. def OAI.DefocusingNLS.SeparatorArithmetic.diskRadius line 15
  3. def OAI.DefocusingNLS.SeparatorArithmetic.diskCenters line 17
  4. def OAI.DefocusingNLS.SeparatorArithmetic.centeredCoefficient line 40

    Source documentation

    Coefficients of D^15 P((c + X)/D); all denominators are cleared.

    def centeredCoefficient (ℓ : ℕ) (c : GaussianInt) (i : ℕ) : GaussianInt :=
…
  5. def OAI.DefocusingNLS.SeparatorArithmetic.coefficientUpper line 45
  6. def OAI.DefocusingNLS.SeparatorArithmetic.coefficientLower line 46
  7. def OAI.DefocusingNLS.SeparatorArithmetic.diskErrorBound line 48
  8. def OAI.DefocusingNLS.SeparatorArithmetic.diskBound line 53
  9. instance OAI.DefocusingNLS.SeparatorArithmetic.(instance at line 57) line 57
  10. theorem OAI.DefocusingNLS.SeparatorArithmetic.disk_bounds_zero line 61
  11. theorem OAI.DefocusingNLS.SeparatorArithmetic.disk_bounds_one line 62
  12. theorem OAI.DefocusingNLS.SeparatorArithmetic.disk_bounds_two line 63
  13. theorem OAI.DefocusingNLS.SeparatorArithmetic.disk_bounds_three line 64
  14. theorem OAI.DefocusingNLS.SeparatorArithmetic.disk_bound line 66
  15. theorem OAI.DefocusingNLS.SeparatorArithmetic.disk_linear_nonzero line 73
  16. theorem OAI.DefocusingNLS.SeparatorArithmetic.disk_centers_separated line 77
  17. theorem OAI.DefocusingNLS.SeparatorArithmetic.disk_centers_avoid_axis line 82
  18. def OAI.DefocusingNLS.SeparatorArithmetic.positiveRootCount line 86
  19. theorem OAI.DefocusingNLS.SeparatorArithmetic.positive_disk_count line 88