OAI/MathematicalPhysics/DefocusingNLS/Certificates/ExteriorPolynomialDegree.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The K=5 spatial form has the coherent degrees used by its certificate.

  1. theorem OAI.DefocusingNLS.ExteriorCertificate.inputT_degree line 11
  2. theorem OAI.DefocusingNLS.ExteriorCertificate.inputS_degree line 15
  3. theorem OAI.DefocusingNLS.ExteriorCertificate.state_entry_succ_zero line 20
  4. theorem OAI.DefocusingNLS.ExteriorCertificate.state_entry_succ_one line 26
  5. theorem OAI.DefocusingNLS.ExteriorCertificate.state_column_degree line 32
  6. theorem OAI.DefocusingNLS.ExteriorCertificate.form_last_row line 71
  7. theorem OAI.DefocusingNLS.ExteriorCertificate.form_degree line 90

    Source documentation

    In particular d has degree ≤10, and the lower off-diagonal entry degree ≤9.

    theorem form_degree (z₀ : ℤ) (b : ℝ) (j : Fin 2) :
    (formPolynomial z₀ b 1 j).natDegree ≤ 9+j.val := by
…

    Mentions: OAI.DefocusingNLS.ExteriorCertificate.formPolynomial