OAI/MathematicalPhysics/DefocusingNLS/Certificates/BoundaryEnclosureStateLink.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The coherent enclosure state is the polynomial forward matrix

  1. def OAI.DefocusingNLS.BoundaryCertificate.stateMatrix line 14
  2. def OAI.DefocusingNLS.BoundaryCertificate.scaledConstant line 17
  3. def OAI.DefocusingNLS.BoundaryCertificate.scaledMass line 20
  4. def OAI.DefocusingNLS.BoundaryCertificate.scaledShift line 22
  5. def OAI.DefocusingNLS.BoundaryCertificate.variableScale line 24
  6. theorem OAI.DefocusingNLS.BoundaryCertificate.polynomialStep_matrix line 26
  7. theorem OAI.DefocusingNLS.BoundaryCertificate.inputT_eq_comp line 34
  8. theorem OAI.DefocusingNLS.BoundaryCertificate.boundaryForwardStep_scaled_comp line 42
  9. theorem OAI.DefocusingNLS.BoundaryCertificate.polynomialState_matrix line 53

    Source documentation

    This identity connects the exact uncertain-coefficient recursion to the parameter-uniform polynomial degree and parity theorems.

    theorem polynomialState_matrix (ell : ℕ) (b Z : ℝ) (K : ℕ) (i j : Fin 2) :
    stateMatrix (polynomialState ell b Z K) i j =
      (boundaryForwardProduct (scaledMass ell) (scaledShift Z)
        (fun n => scaledConstant ell n b) K i j).comp variableScale := by
…

    Mentions: OAI.DefocusingNLS.BoundaryCertificate.stateMatrix, OAI.DefocusingNLS.BoundaryCertificate.polynomialState, OAI.DefocusingNLS.boundaryForwardProduct, OAI.DefocusingNLS.BoundaryCertificate.scaledMass, OAI.DefocusingNLS.BoundaryCertificate.scaledShift, OAI.DefocusingNLS.BoundaryCertificate.scaledConstant, OAI.DefocusingNLS.BoundaryCertificate.variableScale