ExpandingModeEquation.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The actual Fourier-mode equation on an expanding torus

At fixed normalized torus position, each physical coefficient solves the Schrödinger equation with the expected frequency factor L_s⁻² |n|².

def OAI.DefocusingNLS.expandingModeRate line 18
theorem OAI.DefocusingNLS.hasDerivAt_expandingFreeTime line 22
theorem OAI.DefocusingNLS.hasDerivAt_expandingFreeAmplitude line 31
theorem OAI.DefocusingNLS.hasDerivAt_expandingFreeMode line 52
theorem OAI.DefocusingNLS.continuous_expandingFreeMode line 66
theorem OAI.DefocusingNLS.continuous_expandingFourierCoefficient line 72
Source documentation
Physical coefficient evaluation is jointly continuous in the radius and vector.
```
theorem continuous_expandingFourierCoefficient (a k : ℝ) (n : frequencyLattice) :
    Continuous (fun p : {L : ℝ // 1 ≤ L} × FourierL2 =>
      expandingFourierCoefficient a k p.1.1 p.2 n) := by
…
```
Mentions: OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.expandingFourierCoefficient
theorem OAI.DefocusingNLS.continuousOn_expandingPhysicalCoefficient line 90

theorem OAI.DefocusingNLS.hasDerivAt_expandingMild_coefficient line 99

Source documentation

Differentiating the exact mild formula gives the actual moving Fourier equation.

theorem hasDerivAt_expandingMild_coefficient (a b k L T : ℝ)
    (ha : 0 < a) (hk : 8 < k) (hL : 1 ≤ L)
    (u r : ℝ → FourierL2) (u₀ : FourierL2) (hr : ContinuousOn r (Icc 0 T))
    (hu : ∀ (s : ℝ) (hs : s ∈ Icc 0 T), u s = expandingFreeStep a b k L s ha hk hL hs.1 u₀ +
      expandingDuhamel a b k L ha hk hL s r)
    (t : ℝ) (ht : t ∈ Ioo 0 T) (n : frequencyLattice) :
    HasDerivAt (fun s => expandingFourierCoefficient a k (expandingRadius L s) (u s) n)
      (expandingModeRate a b L t n *
        expandingFourierCoefficient a k (expandingRadius L t) (u t) n +
        expandingFourierCoefficient a k (expandingRadius L t) (r t) n) t := by
…

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.expandingFreeStep, OAI.DefocusingNLS.expandingDuhamel, OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.expandingFourierCoefficient, OAI.DefocusingNLS.expandingRadius, OAI.DefocusingNLS.expandingModeRate