OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/GaussianEnclosure.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Sound Gaussian-integer error balls

The center is a Gaussian integer and the radius is an integer. The product radius bounds the error arising from both factors.

  1. structure OAI.DefocusingNLS.GaussianEnclosure line 13
  2. def OAI.DefocusingNLS.GaussianEnclosure.magnitude line 20
  3. def OAI.DefocusingNLS.GaussianEnclosure.Encloses line 22
  4. def OAI.DefocusingNLS.GaussianEnclosure.add line 25
  5. def OAI.DefocusingNLS.GaussianEnclosure.neg line 28
  6. def OAI.DefocusingNLS.GaussianEnclosure.mul line 30
  7. def OAI.DefocusingNLS.GaussianEnclosure.conj line 33
  8. theorem OAI.DefocusingNLS.GaussianEnclosure.magnitude_nonneg line 35
  9. theorem OAI.DefocusingNLS.GaussianEnclosure.norm_center_le_magnitude line 37
  10. theorem OAI.DefocusingNLS.GaussianEnclosure.error_nonneg line 45
  11. theorem OAI.DefocusingNLS.GaussianEnclosure.add_sound line 49
  12. theorem OAI.DefocusingNLS.GaussianEnclosure.neg_sound line 58
  13. theorem OAI.DefocusingNLS.GaussianEnclosure.conj_sound line 66
  14. theorem OAI.DefocusingNLS.GaussianEnclosure.mul_sound line 73