ExpandingPhysicalPath.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Continuous identification with a fixed Fourier Sobolev space

Inverse weight transfer keeps physical Fourier coefficients unchanged. It permits strong time derivatives to be stated in one fixed Banach space.

def OAI.DefocusingNLS.expandingPhysicalPath line 15
theorem OAI.DefocusingNLS.expandingPhysicalPath_coefficient line 24

theorem OAI.DefocusingNLS.hasDerivAt_expandingPhysicalPath_coordinate line 36

Source documentation

A physical Fourier-coordinate derivative transports into the fixed weighted model.

theorem hasDerivAt_expandingPhysicalPath_coordinate (a k L T : ℝ)
    (ha : 0 < a) (hk : 8 < k) (hL : 1 ≤ L) (hT : 0 ≤ T)
    (u : C(Icc (0 : ℝ) T, FourierL2)) (t : ℝ) (ht : t ∈ Ioo 0 T)
    (n : frequencyLattice) (d : ℂ)
    (hd : HasDerivAt (fun s => expandingFourierCoefficient a k (expandingRadius L s)
      (u (projIcc 0 T hT s)) n) d t) :
    HasDerivAt (fun s => expandingPhysicalPath a k L T ha hk hL u (projIcc 0 T hT s) n)
      ((expandingSobolevWeight a k 1 n : ℂ) * d) t := by
…

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.expandingFourierCoefficient, OAI.DefocusingNLS.expandingRadius, OAI.DefocusingNLS.expandingPhysicalPath, OAI.DefocusingNLS.expandingSobolevWeight