OAI/MathematicalPhysics/DefocusingNLS/Profile/ProfileMatrixMajorant.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DefocusingNLS.ProfileCertificate.Dominates line 11

   Source documentation

   Entrywise complex modulus bounds, retaining the two-term matrix product.

   def Dominates (E : Matrix (Fin 2) (Fin 2) ℝ)
       (A : Matrix (Fin 2) (Fin 2) ℂ) : Prop := ∀ i j, ‖A i j‖ ≤ E i j
   …

2. theorem OAI.DefocusingNLS.ProfileCertificate.Dominates.nonneg line 16
3. theorem OAI.DefocusingNLS.ProfileCertificate.Dominates.add line 19
4. theorem OAI.DefocusingNLS.ProfileCertificate.Dominates.mul line 24
5. theorem OAI.DefocusingNLS.ProfileCertificate.Dominates.smul line 34
6. theorem OAI.DefocusingNLS.ProfileCertificate.Dominates.mono line 40
7. theorem OAI.DefocusingNLS.ProfileCertificate.Dominates.smul_le line 45
8. def OAI.DefocusingNLS.ProfileCertificate.rationalMatrix line 53
9. def OAI.DefocusingNLS.ProfileCertificate.absoluteMatrix line 56
10. theorem OAI.DefocusingNLS.ProfileCertificate.absoluteMatrix_dominates line 59
11. theorem OAI.DefocusingNLS.ProfileCertificate.product_remainder line 64

    Source documentation

    The exact algebraic remainder identity.

    theorem product_remainder (F P U V R : Matrix (Fin 2) (Fin 2) ℂ) :
        (F+P)*(U+V+R)-(F*U+F*V+P*U) = (F+P)*R+P*V := by
    …

12. theorem OAI.DefocusingNLS.ProfileCertificate.product_remainder_dominates line 69

    Source documentation

    Propagate one Taylor remainder without losing the entrywise product structure.

    theorem product_remainder_dominates
        (F P U V R : Matrix (Fin 2) (Fin 2) ℂ)
        (Fbound N Vbound E : Matrix (Fin 2) (Fin 2) ℝ) (δ : ℝ)
        (hF : Dominates Fbound F) (hP : Dominates (δ • N) P)
        (hV : Dominates (δ • Vbound) V) (hR : Dominates (δ^2 • E) R) :
        Dominates (δ^2 • ((Fbound+δ • N)*E+N*Vbound))
          ((F+P)*(U+V+R)-(F*U+F*V+P*U)) := by
    …

    Mentions: OAI.DefocusingNLS.ProfileCertificate.Dominates