OAI/MathematicalPhysics/DefocusingNLS/Profile/ProfileTaylorStep.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The entrywise two-parameter Taylor step underlying the K=34 certificate.

  1. abbrev OAI.DefocusingNLS.ProfileCertificate.CMatrix line 10
  2. abbrev OAI.DefocusingNLS.ProfileCertificate.RealMatrix line 11
  3. def OAI.DefocusingNLS.ProfileCertificate.linearModel line 13
  4. theorem OAI.DefocusingNLS.ProfileCertificate.linearModel_step_identity line 15
  5. theorem OAI.DefocusingNLS.ProfileCertificate.taylor_step_dominates line 25

    Source documentation

    The real matrix E is exactly the manuscript's second-order majorant.

    theorem taylor_step_dominates (F G H U X Y A : CMatrix)
    (Fbound Gbound Hbound Xbound Ybound E : RealMatrix)
    (b z δ r : ℝ) (hr : 0 ≤ r) (hb : |b| ≤ δ) (hz : |z| ≤ δ)
    (hF : Dominates Fbound F) (hG : Dominates Gbound G)
    (hH : Dominates Hbound H) (hX : Dominates Xbound X) (hY : Dominates Ybound Y)
    (hE : Dominates (δ^2 • E) (A-linearModel U X Y b z)) :
    Dominates
      (δ^2 • (r • ((Fbound+δ • (Gbound+Hbound))*E +
        (Gbound+Hbound)*(Xbound+Ybound))))
      (r • ((F+b • G+z • H)*A) -
        linearModel (r • (F*U)) (r • (G*U+F*X)) (r • (H*U+F*Y)) b z) := by
…

    Mentions: OAI.DefocusingNLS.ProfileCertificate.CMatrix, OAI.DefocusingNLS.ProfileCertificate.RealMatrix, OAI.DefocusingNLS.ProfileCertificate.Dominates, OAI.DefocusingNLS.ProfileCertificate.linearModel