OAI/MathematicalPhysics/DefocusingNLS/Certificates/ForwardHermitianForm.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DefocusingNLS.forwardFormEntry line 11
2. theorem OAI.DefocusingNLS.star_eq_neg_of_re_zero line 16
3. theorem OAI.DefocusingNLS.forwardFormEntry_hermitian line 19
4. theorem OAI.DefocusingNLS.forwardFormEntry_diagonal line 26
5. theorem OAI.DefocusingNLS.coneForm_as_hermitian line 36
6. theorem OAI.DefocusingNLS.hermitianPairForm_eq_quadratic line 43
7. theorem OAI.DefocusingNLS.forwardFormEntry_expansion line 52
8. theorem OAI.DefocusingNLS.forwardFormEntry_pairForm line 64

   Source documentation

   The Hermitian quadratic form is twice the forward cone form.

   theorem forwardFormEntry_pairForm (M : ℝ) (s : ℂ) (T : Matrix (Fin 2) (Fin 2) ℂ)
       (hs : s.re = 0) (u v : ℂ) :
       hermitianPairForm (forwardFormEntry M s T 0 0).re (forwardFormEntry M s T 1 1).re
         (forwardFormEntry M s T 0 1) u v = 2 * matrixCone M s T ![u, v] := by
   …

   Mentions: OAI.DefocusingNLS.hermitianPairForm, OAI.DefocusingNLS.forwardFormEntry, OAI.DefocusingNLS.matrixCone

9. theorem OAI.DefocusingNLS.hermitianPairForm_add line 74
10. theorem OAI.DefocusingNLS.positive_sum_matrixCone line 82

    Source documentation

    Positive leading entry and determinant of the summed Hermitian matrix supply the positivity needed for exclusion of matching zeros.

    theorem positive_sum_matrixCone (M : ℝ) (s₁ s₂ : ℂ)
        (T₁ T₂ : Matrix (Fin 2) (Fin 2) ℂ) (hs₁ : s₁.re = 0) (hs₂ : s₂.re = 0)
        (ha : 0 < (forwardFormEntry M s₁ T₁ 0 0).re + (forwardFormEntry M s₂ T₂ 0 0).re)
        (hdet : 0 <
          ((forwardFormEntry M s₁ T₁ 0 0).re + (forwardFormEntry M s₂ T₂ 0 0).re) *
          ((forwardFormEntry M s₁ T₁ 1 1).re + (forwardFormEntry M s₂ T₂ 1 1).re) -
          Complex.normSq (forwardFormEntry M s₁ T₁ 0 1 + forwardFormEntry M s₂ T₂ 0 1))
        (w : Fin 2 → ℂ) (hw : w ≠ 0) :
        0 < matrixCone M s₁ T₁ w + matrixCone M s₂ T₂ w := by
    …

    Mentions: OAI.DefocusingNLS.forwardFormEntry, OAI.DefocusingNLS.matrixCone