SchwartzCompactContinuity.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Continuity of smooth families with a common compact support

The support is fixed only after rescaling the physical cutoff. No decay or symbol hypothesis on the smooth coefficient is needed for this local result.

theorem OAI.DefocusingNLS.continuous_spatial_iteratedFDeriv line 20

Source documentation

Spatial derivatives of a jointly smooth family vary jointly continuously.

theorem continuous_spatial_iteratedFDeriv (F : ℝ × E → ℂ)
    (hF : ContDiff ℝ ∞ F) (n : ℕ) :
    Continuous (fun p : ℝ × E => iteratedFDeriv ℝ n (fun x => F (p.1, x)) p.2) := by
…

theorem OAI.DefocusingNLS.continuous_schwartz_of_common_compact_support line 38

Source documentation

Jointly continuous spatial jets and a fixed compact support give Schwartz continuity.

theorem continuous_schwartz_of_common_compact_support
    {P : Type*} [UniformSpace P] [WeaklyLocallyCompactSpace P]
    (f : P → 𝓢(E, ℂ)) (K : Set E) (hK : IsCompact K)
    (hs : ∀ t, tsupport (f t : E → ℂ) ⊆ K)
    (hj : ∀ n : ℕ, Continuous
      (fun p : P × E => iteratedFDeriv ℝ n (f p.1) p.2)) : Continuous f := by
…

def OAI.DefocusingNLS.compactSmoothFamily line 91

Source documentation

Multiplication of a jointly smooth family by a fixed compact cutoff.

noncomputable def compactSmoothFamily (κ : 𝓢(E, ℂ))
    (hκ : HasCompactSupport (κ : E → ℂ)) (F : ℝ × E → ℂ)
    (hF : ContDiff ℝ ∞ F) (t : ℝ) : 𝓢(E, ℂ) :=
…

theorem OAI.DefocusingNLS.compactSmoothFamily_apply line 97
theorem OAI.DefocusingNLS.continuous_compactSmoothFamily line 102