OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/CutoffProfileModeDerivative.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Time derivative of the actual cutoff-profile Fourier coefficients

The physical volume factor disappears after rescaling to the fixed cutoff. Differentiating then takes place on a fixed compact support.

  1. theorem OAI.DefocusingNLS.cutoffProfile_coefficient_fixed_scale line 19
  2. theorem OAI.DefocusingNLS.hasDerivAt_radius line 35
  3. theorem OAI.DefocusingNLS.positive_radius line 42
  4. theorem OAI.DefocusingNLS.hasDerivAt_cutoffProfile_coefficient line 46

    Source documentation

    An exact scalar Fourier-mode derivative at every real time.

    theorem hasDerivAt_cutoffProfile_coefficient (L s : โ„) (hL : 0 < L)
    (ฯ‡ : ๐“ข(E, โ„‚)) (hฯ‡ : HasCompactSupport (ฯ‡ : E โ†’ โ„‚))
    (Q : E โ†’ โ„‚) (hQ : ContDiff โ„ โˆž Q) (n : frequencyLattice) :
    HasDerivAt
      (fun t => schwartzLatticeCoefficient (expandingRadius L t)
        (radianFourierKernel (cutoffProfileSchwartz (expandingRadius L t)
          (positive_radius L _ hL) ฯ‡ hฯ‡ Q hQ)) n)
      ((((2 * Real.pi) ^ (12 : โ„•))โปยน : โ„) *
        radianFourierIntegral (fun x => ฯ‡ x *
          fderiv โ„ Q ((expandingRadius L s) โ€ข x) ((expandingRadius L s / 2) โ€ข x))
          (n : E)) s := by
โ€ฆ

    Mentions: OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.schwartzLatticeCoefficient, OAI.DefocusingNLS.expandingRadius, OAI.DefocusingNLS.radianFourierKernel, OAI.DefocusingNLS.cutoffProfileSchwartz, OAI.DefocusingNLS.positive_radius, OAI.DefocusingNLS.radianFourierIntegral