SobolevNonlinearity.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The odd-power nonlinearity on the Fourier Sobolev space

The convolution product and frequency-reversing conjugation realize the actual pointwise polynomial |u|^(2m) u. The induced map is smooth and locally Lipschitz on H^k whenever k > 6.

def OAI.DefocusingNLS.sobolevRealBilinearProduct line 20
Source documentation
Pointwise multiplication viewed as a continuous real-bilinear operation.
```
noncomputable def sobolevRealBilinearProduct (k : ℝ) (hk : 6 < k) :
    FourierL2 →L[ℝ] FourierL2 →L[ℝ] FourierL2 :=
…
```
Mentions: OAI.DefocusingNLS.FourierL2
theorem OAI.DefocusingNLS.sobolevRealBilinearProduct_apply line 24
def OAI.DefocusingNLS.sobolevOddPower line 29
Source documentation
The actual odd-power map on H^k, built from its bounded algebra operations.
Distinct definitions of this name: ComparatorChallenges/DefocusingNLS.lean:120 (different declaration text). Qualify references as OAI.DefocusingNLS.sobolevOddPower@path.
```
noncomputable def sobolevOddPower (k : ℝ) (hk : 6 < k) : ℕ → FourierL2 → FourierL2
  | 0, f => f
  | m + 1, f => sobolevProduct k hk
      (sobolevProduct k hk (sobolevOddPower k hk m f) (fourierConjugate f)) f

/-- Sobolev odd powers have exactly the claimed pointwise values on the torus. -/
```
Mentions: OAI.DefocusingNLS.FourierL2
theorem OAI.DefocusingNLS.sobolevOddPower_apply line 35
Source documentation
Sobolev odd powers have exactly the claimed pointwise values on the torus.
```
theorem sobolevOddPower_apply (k : ℝ) (hk : 6 < k) (m : ℕ)
    (f : FourierL2) (x : SchrodingerTorus) :
    sobolevTorusFunction k (sobolevOddPower k hk m f) x =
      oddPowerNonlinearity m (sobolevTorusFunction k f x) := by
…
```
Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.SchrodingerTorus, OAI.DefocusingNLS.oddPowerNonlinearity
theorem OAI.DefocusingNLS.contDiff_sobolevOddPower line 48
Source documentation
The Banach-space nonlinearity is smooth as a real map.
```
theorem contDiff_sobolevOddPower (k : ℝ) (hk : 6 < k) (m : ℕ) :
    ContDiff ℝ ⊤ (sobolevOddPower k hk m) := by
…
```
theorem OAI.DefocusingNLS.locallyLipschitz_sobolevOddPower line 60
Source documentation
Local Lipschitz continuity needed for the semilinear Cauchy problem.
```
theorem locallyLipschitz_sobolevOddPower (k : ℝ) (hk : 6 < k) (m : ℕ) :
    LocallyLipschitz (sobolevOddPower k hk m) :=
…
```
theorem OAI.DefocusingNLS.norm_sobolevOddPower_le line 65
Source documentation
The algebra norm controls the polynomial growth of the nonlinearity.
```
theorem norm_sobolevOddPower_le (k : ℝ) (hk : 6 < k) (m : ℕ) (f : FourierL2) :
    ‖sobolevOddPower k hk m f‖ ≤
      ‖sobolevBilinearProduct k hk‖ ^ (2 * m) * ‖f‖ ^ (2 * m + 1) := by
…
```
Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.sobolevBilinearProduct