OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/CutoffFamilyContinuity.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Continuous cutoff-profile and residual paths

These are the actual sampled physical functions. The fixed-support rescaling makes their Schwartz and Hilbert continuity independent of any symbol bounds. The symbol bounds remain responsible for the separate uniform norm estimates.

  1. def OAI.DefocusingNLS.compactDilationFamily line 22
  2. theorem OAI.DefocusingNLS.compactDilationFamily_apply line 28
  3. theorem OAI.DefocusingNLS.continuous_compactDilationFamily line 32
  4. theorem OAI.DefocusingNLS.continuous_scale_rpow line 38
  5. def OAI.DefocusingNLS.normalizedCompactProfile line 43
  6. theorem OAI.DefocusingNLS.normalizedCompactProfile_apply line 48
  7. theorem OAI.DefocusingNLS.continuous_normalizedCompactProfile line 57
  8. theorem OAI.DefocusingNLS.family_gradient_compact line 70
  9. theorem OAI.DefocusingNLS.family_laplacian_compact line 75
  10. theorem OAI.DefocusingNLS.family_power_compact line 80
  11. theorem OAI.DefocusingNLS.continuous_normalizedCutoffResidualSchwartz line 85

    Source documentation

    The normalized three-term residual is a continuous Schwartz family.

    theorem continuous_normalizedCutoffResidualSchwartz (a : ℝ) (m : ℕ)
    (Q : E → ℂ) (hQ : ContDiff ℝ ∞ Q) :
    Continuous (fun L : Scale =>
      normalizedCutoffResidualSchwartz χ hχ hχone hχzero a L.1 m Q hQ) := by
…

    Mentions: OAI.DefocusingNLS.normalizedCutoffResidualSchwartz

  12. theorem OAI.DefocusingNLS.continuous_cutoffProfile_sample line 138

    Source documentation

    The actual cutoff-profile sample varies continuously with the physical radius.

    theorem continuous_cutoffProfile_sample (a k : ℝ) (ha : 0 < a)
    (ha1 : a < 1) (hk : 8 < k) (χ : 𝓢(E, ℂ))
    (hχ : HasCompactSupport (χ : E → ℂ)) (Q : E → ℂ) (hQ : ContDiff ℝ ∞ Q) :
    Continuous (fun L : Scale => schwartzTorusSample a k L.1 ha1 hk L.2
      (radianFourierKernel
        (cutoffProfileSchwartz L.1 (lt_of_lt_of_le zero_lt_one L.2) χ hχ Q hQ))) := by
…

    Mentions: OAI.DefocusingNLS.schwartzTorusSample, OAI.DefocusingNLS.radianFourierKernel, OAI.DefocusingNLS.cutoffProfileSchwartz

  13. theorem OAI.DefocusingNLS.continuous_cutoffResidual_sample line 166

    Source documentation

    The exact PDE residual is a continuous forcing path in the sampled Hilbert model.

    theorem continuous_cutoffResidual_sample (a k : ℝ) (ha : 0 < a)
    (ha1 : a < 1) (hk : 8 < k) (χ : 𝓢(E, ℝ))
    (hχ : HasCompactSupport (χ : E → ℝ))
    (hχone : ∀ x : E, ‖x‖ < 1 / 2 → χ x = 1)
    (hχzero : ∀ x : E, 2 < ‖x‖ → χ x = 0)
    (m : ℕ) (Q : E → ℂ) (hQ : ContDiff ℝ ∞ Q) :
    Continuous (fun L : Scale => schwartzTorusSample a k L.1 ha1 hk L.2
      (radianFourierKernel (cutoffResidualSchwartz χ hχ hχone hχzero a L.1
        (lt_of_lt_of_le zero_lt_one L.2) m Q hQ))) := by
…

    Mentions: OAI.DefocusingNLS.schwartzTorusSample, OAI.DefocusingNLS.radianFourierKernel, OAI.DefocusingNLS.cutoffResidualSchwartz