OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingFreeContinuity.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Strong continuity of the moving-scale free propagator

Continuity is joint in the positive starting scale, forward time, and input. No operator-norm continuity of Schrödinger evolution is asserted.

  1. abbrev OAI.DefocusingNLS.ExpandingFreeParameters line 16
  2. def OAI.DefocusingNLS.expandingFreeFamily line 18
  3. theorem OAI.DefocusingNLS.expandingFreeFamily_apply_coordinate line 22
  4. theorem OAI.DefocusingNLS.continuous_weight_on_positive line 34
  5. theorem OAI.DefocusingNLS.continuous_family_coordinate line 44
  6. theorem OAI.DefocusingNLS.family_coordinate_bound line 76
  7. theorem OAI.DefocusingNLS.continuous_expandingFreeFamily line 104

    Source documentation

    Each fixed input has a strongly continuous free orbit, jointly in scale and time.

    theorem continuous_expandingFreeFamily (a b k : ℝ) (ha : 0 < a) (hk : 8 < k)
    (f : FourierL2) :
    Continuous (fun p : ExpandingFreeParameters => expandingFreeFamily a b k ha hk p f) := by
…

    Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.ExpandingFreeParameters, OAI.DefocusingNLS.expandingFreeFamily

  8. theorem OAI.DefocusingNLS.continuous_expandingFreeFamily_uncurry line 159

    Source documentation

    Strong continuity for varying inputs, without an operator-norm assertion.

    theorem continuous_expandingFreeFamily_uncurry (a b k : ℝ) (ha : 0 < a) (hk : 8 < k) :
    Continuous (fun p : ExpandingFreeParameters × FourierL2 =>
      expandingFreeFamily a b k ha hk p.1 p.2) := by
…

    Mentions: OAI.DefocusingNLS.ExpandingFreeParameters, OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.expandingFreeFamily