OAI/MathematicalPhysics/DefocusingNLS/Profile/ProfileMatrixProduct.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The rational profile product is the actual normalized backward matrix.

  1. def OAI.DefocusingNLS.ProfileCertificate.complexMatrix line 11
  2. theorem OAI.DefocusingNLS.ProfileCertificate.complexMatrix_one line 14
  3. theorem OAI.DefocusingNLS.ProfileCertificate.complexMatrix_mul line 17
  4. theorem OAI.DefocusingNLS.ProfileCertificate.complexMatrix_scale line 21
  5. def OAI.DefocusingNLS.ProfileCertificate.profileFactor line 27

    Source documentation

    Each factor in the finite product, including its manuscript normalization.

    noncomputable def profileFactor (b Z : ℝ) (n : ℕ) : Matrix (Fin 2) (Fin 2) ℂ :=
…
  6. def OAI.DefocusingNLS.ProfileCertificate.profileProduct line 30
  7. theorem OAI.DefocusingNLS.ProfileCertificate.factor_complex line 33
  8. theorem OAI.DefocusingNLS.ProfileCertificate.inverse_complex line 40
  9. theorem OAI.DefocusingNLS.ProfileCertificate.complexMatrix_step line 46
  10. theorem OAI.DefocusingNLS.ProfileCertificate.complexMatrix_foldr line 52
  11. theorem OAI.DefocusingNLS.ProfileCertificate.profileFactor_product line 59
  12. theorem OAI.DefocusingNLS.ProfileCertificate.result_value_eq_profileProduct line 74