OAI/MathematicalPhysics/DefocusingNLS/Profile/ProfileMatchingQuotient.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual logarithmic derivative equals the quotient of the matched column.

  1. def OAI.DefocusingNLS.ProfileCertificate.freeProfileJ line 13
  2. theorem OAI.DefocusingNLS.ProfileCertificate.freeProfileJ_eq_matched line 19

    Source documentation

    The normalization of the finite matrix cancels in the component ratio.

    theorem freeProfileJ_eq_matched (b z : ℝ)
    (hz : |z| ≤ (radius : ℝ)) :
    let q : ℂ := -Complex.I*(((centerB : ℝ)+b : ℝ) : ℂ)
…

    Mentions: OAI.DefocusingNLS.ProfileCertificate.radius, OAI.DefocusingNLS.ProfileCertificate.centerB