ExpandingModeDuhamel.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Fourier-mode variation of constants on the moving torus

The normalized Hilbert-space Duhamel construction has the exact physical Fourier integrating factor. The Fourier modes refer to fixed y/L_s, as in the manuscript's interpretation of the expanding-torus equation.

def OAI.DefocusingNLS.expandingFreeMode line 17
theorem OAI.DefocusingNLS.expandingFreeMode_ne_zero line 20
theorem OAI.DefocusingNLS.expandingFreeMode_add line 25
theorem OAI.DefocusingNLS.expandingFreeMode_kernel line 32
def OAI.DefocusingNLS.expandingCoefficientCLM line 41
Source documentation
Physical coefficient evaluation at a fixed radius is continuous linear.
```
noncomputable def expandingCoefficientCLM (a k L : ℝ) (n : frequencyLattice) :
    FourierL2 →L[ℂ] ℂ :=
…
```
Mentions: OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.FourierL2
theorem OAI.DefocusingNLS.expandingCoefficientCLM_apply line 46

theorem OAI.DefocusingNLS.expandingDuhamel_coefficient line 51

Source documentation

The physical Fourier coefficient of Duhamel is its scalar variation of constants.

theorem expandingDuhamel_coefficient (a b k L t : ℝ)
    (ha : 0 < a) (hk : 8 < k) (hL : 1 ≤ L) (r : ℝ → FourierL2)
    (hr : ContinuousOn r (Icc 0 t)) (n : frequencyLattice) :
    expandingFourierCoefficient a k (expandingRadius L t)
        (expandingDuhamel a b k L ha hk hL t r) n =
      expandingFreeMode a b L t n * ∫ τ in Icc 0 t,
        (expandingFreeMode a b L τ n)⁻¹ *
          expandingFourierCoefficient a k (expandingRadius L τ) (r τ) n := by
…

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.expandingFourierCoefficient, OAI.DefocusingNLS.expandingRadius, OAI.DefocusingNLS.expandingDuhamel, OAI.DefocusingNLS.expandingFreeMode

theorem OAI.DefocusingNLS.expandingMild_coefficient line 81

Source documentation

Every continuous mild trajectory satisfies the exact modewise integral equation.

theorem expandingMild_coefficient (a b k L t : ℝ)
    (ha : 0 < a) (hk : 8 < k) (hL : 1 ≤ L) (ht : 0 ≤ t)
    (r : ℝ → FourierL2) (hr : ContinuousOn r (Icc 0 t))
    (u₀ : FourierL2) (n : frequencyLattice) :
    expandingFourierCoefficient a k (expandingRadius L t)
      (expandingFreeStep a b k L t ha hk hL ht u₀ +
        expandingDuhamel a b k L ha hk hL t r) n =
      expandingFreeMode a b L t n *
        (expandingFourierCoefficient a k L u₀ n + ∫ τ in Icc 0 t,
          (expandingFreeMode a b L τ n)⁻¹ *
            expandingFourierCoefficient a k (expandingRadius L τ) (r τ) n) := by
…