OAI/MathematicalPhysics/DefocusingNLS/Certificates/ExteriorPolynomial.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The coherent spatial polynomial enclosed by the K=5 exterior computation.

  1. def OAI.DefocusingNLS.ExteriorCertificate.inputS line 14
  2. def OAI.DefocusingNLS.ExteriorCertificate.inputT line 17
  3. def OAI.DefocusingNLS.ExteriorCertificate.polynomialState line 20
  4. theorem OAI.DefocusingNLS.ExteriorCertificate.inputS_sound line 25
  5. theorem OAI.DefocusingNLS.ExteriorCertificate.inputT_sound line 33
  6. theorem OAI.DefocusingNLS.ExteriorCertificate.step_sound line 49
  7. theorem OAI.DefocusingNLS.ExteriorCertificate.state_sound line 64
  8. theorem OAI.DefocusingNLS.ExteriorCertificate.inputT_eval_scaled line 74
  9. theorem OAI.DefocusingNLS.ExteriorCertificate.inputS_eval_scaled line 81
  10. theorem OAI.DefocusingNLS.ExteriorCertificate.polynomialState_eval_scaled line 91

    Source documentation

    Evaluation gives the actual forward matrix, with its exact integer scale.

    theorem polynomialState_eval_scaled (z₀ : ℤ) (b v : ℝ) (N : ℕ) (i j : Fin 2) :
    (stateMatrix (polynomialState z₀ b N) i j).eval (v : ℂ) =
      (100000000 : ℂ)^N*
        forwardProduct 5 (Complex.I*(((z₀ : ℝ)/100000000+v : ℝ) : ℂ))
          (-Complex.I*(b : ℂ)) N i j := by
…

    Mentions: OAI.DefocusingNLS.ExteriorCertificate.polynomialState, OAI.DefocusingNLS.forwardProduct