OAI/MathematicalPhysics/DefocusingNLS/Certificates/ExteriorFormPolynomial.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DefocusingNLS.ExteriorCertificate.formPolynomial line 15
2. theorem OAI.DefocusingNLS.ExteriorCertificate.hermitian_sound line 20
3. theorem OAI.DefocusingNLS.ExteriorCertificate.diagonal_sound line 34
4. theorem OAI.DefocusingNLS.ExteriorCertificate.lowerOffDiagonal_sound line 39
5. theorem OAI.DefocusingNLS.ExteriorCertificate.forwardFormEntry_real_scaling line 44
6. theorem OAI.DefocusingNLS.ExteriorCertificate.formPolynomial_eval line 53

   Source documentation

   The degree-truncated checks must be applied to this same coherent form.

   theorem formPolynomial_eval (z₀ : ℤ) (b v : ℝ) (i j : Fin 2) :
       (formPolynomial z₀ b i j).eval (v : ℂ) =
         (100000000 : ℂ)^11*
           forwardFormEntry 5 (Complex.I*(((z₀ : ℝ)/100000000+v : ℝ) : ℂ))
             (forwardProduct 5 (Complex.I*(((z₀ : ℝ)/100000000+v : ℝ) : ℂ))
               (-Complex.I*(b : ℂ)) 5) i j := by
   …

   Mentions: OAI.DefocusingNLS.ExteriorCertificate.formPolynomial, OAI.DefocusingNLS.forwardFormEntry, OAI.DefocusingNLS.forwardProduct