ExpandingNonlinearity.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

The actual odd-power map on the expanding-torus norm

theorem OAI.DefocusingNLS.expandingFourierCoefficient_conjugate line 12
theorem OAI.DefocusingNLS.expandingTorusFunction_conjugate line 21
def OAI.DefocusingNLS.expandingRealBilinearProduct line 33
theorem OAI.DefocusingNLS.expandingRealBilinearProduct_apply line 38
def OAI.DefocusingNLS.expandingAlgebraBound line 43
theorem OAI.DefocusingNLS.expandingAlgebraBound_nonneg line 46
theorem OAI.DefocusingNLS.expandingRealBilinearProduct_norm_le line 50

def OAI.DefocusingNLS.expandingOddPower line 58

Source documentation

The Fourier realization of the scalar polynomial |u|^(2m) u.

noncomputable def expandingOddPower (a k L : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (hL : 1 ≤ L) :
    ℕ → FourierL2 → FourierL2
  | 0, f => f
  | m + 1, f => expandingProduct a k L ha ha1 hk hL
      (expandingProduct a k L ha ha1 hk hL
        (expandingOddPower a k L ha ha1 hk hL m f) (fourierConjugate f)) f

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.expandingProduct

theorem OAI.DefocusingNLS.expandingOddPower_apply line 66
theorem OAI.DefocusingNLS.contDiff_expandingOddPower line 80
Source documentation
The expanding-torus nonlinearity is smooth as a real Banach-space map.
```
theorem contDiff_expandingOddPower (a k L : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (hL : 1 ≤ L) (m : ℕ) :
    ContDiff ℝ ⊤ (expandingOddPower a k L ha ha1 hk hL m) := by
…
```
Mentions: OAI.DefocusingNLS.expandingOddPower

theorem OAI.DefocusingNLS.norm_expandingOddPower_le line 93

Source documentation

Polynomial growth has a constant independent of the expanding radius.

theorem norm_expandingOddPower_le (a k L : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (hL : 1 ≤ L) (m : ℕ) (f : FourierL2) :
    ‖expandingOddPower a k L ha ha1 hk hL m f‖ ≤
      expandingAlgebraBound a k ^ (2 * m) * ‖f‖ ^ (2 * m + 1) := by
…

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.expandingOddPower, OAI.DefocusingNLS.expandingAlgebraBound