OAI/MathematicalPhysics/DefocusingNLS/Profile/FreeSlowContinuity.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Joint continuity on the small real parameter rectangle used for the free profile.

  1. def OAI.DefocusingNLS.freeParameterRectangle line 11

    Source documentation

    A fixed rectangle containing the free-profile parameter disk.

    def freeParameterRectangle : Set (ℝ × ℝ) :=
…
  2. def OAI.DefocusingNLS.freeShiftedQ line 14
  3. def OAI.DefocusingNLS.freeSpatialArgument line 15
  4. theorem OAI.DefocusingNLS.continuous_freeShiftedQ line 17
  5. theorem OAI.DefocusingNLS.continuous_freeSpatialArgument line 21
  6. theorem OAI.DefocusingNLS.freeSpatialArgument_slit line 25
  7. theorem OAI.DefocusingNLS.free_parameter_mass_bound line 34
  8. theorem OAI.DefocusingNLS.continuousOn_free_regularizedSlowKernel line 46
  9. theorem OAI.DefocusingNLS.continuousOn_free_regularizedSlowSolution line 69

    Source documentation

    Joint continuity of the actual integral H, including the q=0 normalization.

    theorem continuousOn_free_regularizedSlowSolution (a : ℝ) (ha : 0 ≤ a) (m : ℕ) :
    ContinuousOn (fun p => regularizedSlowSolution (freeShiftedQ a p) m
      (freeSpatialArgument p)) freeParameterRectangle := by
…

    Mentions: OAI.DefocusingNLS.regularizedSlowSolution, OAI.DefocusingNLS.freeShiftedQ, OAI.DefocusingNLS.freeSpatialArgument, OAI.DefocusingNLS.freeParameterRectangle