OAI/MathematicalPhysics/DefocusingNLS/Profile/ProfileDeterminantBound.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The scalar determinant bound holds for the actual parameter-dependent product.

  1. theorem OAI.DefocusingNLS.ProfileCertificate.backward_det_normSq line 13
  2. theorem OAI.DefocusingNLS.ProfileCertificate.profile_det_normSq line 26
  3. theorem OAI.DefocusingNLS.ProfileCertificate.profile_det_bound line 35
  4. theorem OAI.DefocusingNLS.ProfileCertificate.certificate_as_real line 50
  5. theorem OAI.DefocusingNLS.ProfileCertificate.actual_profile_determinant_bound line 62

    Source documentation

    Uniform determinant modulus bound throughout the certificate square.

    theorem actual_profile_determinant_bound (b z : ℝ) (hb : |b| ≤ (radius : ℝ)) :
    ‖(profileProduct ((centerB : ℝ)+b) ((centerZ : ℝ)+z) 34).det‖ <
      (62/10000000000000 : ℝ)*‖RationalComplex.toComplex result.value.b‖^2 := by
…

    Mentions: OAI.DefocusingNLS.ProfileCertificate.radius, OAI.DefocusingNLS.ProfileCertificate.profileProduct, OAI.DefocusingNLS.ProfileCertificate.centerB, OAI.DefocusingNLS.ProfileCertificate.centerZ, OAI.DefocusingNLS.ProfileCertificate.RationalComplex.toComplex