OAI/MathematicalPhysics/DefocusingNLS/Profile/ProfileProductMatching.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The four-real-dimensional degree step for simultaneous value and slope matching.

  1. abbrev OAI.DefocusingNLS.ProfileCertificate.ProfileMatchingBall line 11
  2. def OAI.DefocusingNLS.ProfileCertificate.profileMatchingParameter line 13
  3. def OAI.DefocusingNLS.ProfileCertificate.profileProductLinearEquiv line 20
  4. theorem OAI.DefocusingNLS.ProfileCertificate.profileProductLinearEquiv_inverse_bound line 23
  5. theorem OAI.DefocusingNLS.ProfileCertificate.zero_of_profile_product_error line 33
  6. theorem OAI.DefocusingNLS.ProfileCertificate.zero_of_profile_product_limit line 47