OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingEvaluation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Bounded observation for the exact expanding-torus model

  1. def OAI.DefocusingNLS.expandingPointObservationVector line 11
  2. def OAI.DefocusingNLS.expandingPointEvaluation line 22
  3. theorem OAI.DefocusingNLS.hasSum_expandingPointEvaluation line 27
  4. theorem OAI.DefocusingNLS.expandingTorusFunction_eq_evaluation line 36
  5. theorem OAI.DefocusingNLS.expandingPointEvaluation_norm_le line 44

    Source documentation

    Evaluation has one operator-norm bound for every expanding torus and every point.

    theorem expandingPointEvaluation_norm_le (a k L : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (hL : 1 ≤ L)
    (x : SchrodingerTorus) :
    ‖expandingPointEvaluation a k L ha ha1 hk hL x‖ ≤ expandingEmbeddingBound a k := by
…

    Mentions: OAI.DefocusingNLS.SchrodingerTorus, OAI.DefocusingNLS.expandingPointEvaluation, OAI.DefocusingNLS.expandingEmbeddingBound