OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousFreeJointContinuity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Joint continuity of time and data for the whole-space free group

  1. theorem OAI.DefocusingNLS.continuous_homogeneousFreeOperator_uncurry line 12

    Source documentation

    Strong continuity and the local uniform bound give joint continuity in time and data.

    theorem continuous_homogeneousFreeOperator_uncurry (a b k : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) :
    Continuous (fun p : ℝ × HomogeneousY a k =>
      homogeneousFreeOperator a b k p.1 ha ha1 hk p.2) := by
…

    Mentions: OAI.DefocusingNLS.HomogeneousY, OAI.DefocusingNLS.homogeneousFreeOperator