OAI/MathematicalPhysics/DefocusingNLS/Linear/SchwartzSampleTranslation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DefocusingNLS.continuous_normalizedTranslation line 17
2. theorem OAI.DefocusingNLS.hasDerivAt_translated_schwartzSample line 28

   Source documentation

   Translation by t*v/L of the sampled vector differentiates to the sample of the physical directional derivative.

   theorem hasDerivAt_translated_schwartzSample (a k L : ℝ) (ha1 : a < 1)
       (hk : 8 < k) (hL : 1 ≤ L) (ψ : 𝓢(E, ℂ)) (v : E) (s : ℝ) :
       HasDerivAt (fun t : ℝ => sobolevTranslation (euclideanToTorus ((t / L) • v))
         (physicalSchwartzTorusSamplingCLM a k L ha1 hk hL ψ))
         (sobolevTranslation (euclideanToTorus ((s / L) • v))
           (physicalSchwartzTorusSamplingCLM a k L ha1 hk hL (∂_{v} ψ))) s := by
   …

   Mentions: OAI.DefocusingNLS.sobolevTranslation, OAI.DefocusingNLS.euclideanToTorus, OAI.DefocusingNLS.physicalSchwartzTorusSamplingCLM

3. theorem OAI.DefocusingNLS.translated_schwartzSample_taylor line 61