ExpandingWeightAddition.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The uniform weight inequality for multiplication in Y_L

def OAI.DefocusingNLS.expandingSobolevWeight line 11
Source documentation
The positive Fourier weight whose ℓ² norm is exactly the manuscript's Y_L norm.
```
noncomputable def expandingSobolevWeight (a k L : ℝ) (n : frequencyLattice) : ℝ :=
…
```
Mentions: OAI.DefocusingNLS.frequencyLattice
theorem OAI.DefocusingNLS.expandingSobolevWeight_pos line 14
theorem OAI.DefocusingNLS.expandingSobolevWeight_sq line 20
theorem OAI.DefocusingNLS.norm_rpow_add_le line 26

theorem OAI.DefocusingNLS.expandingSobolevWeightSq_add_le line 46

Source documentation

The squared weight has an addition constant independent of the growing torus scale.

theorem expandingSobolevWeightSq_add_le (a k L : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (hL : 1 ≤ L) (m n : frequencyLattice) :
    expandingSobolevWeightSq a k L (m + n) ≤
      4 ^ k * (expandingSobolevWeightSq a k L m + expandingSobolevWeightSq a k L n) := by
…

Mentions: OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.expandingSobolevWeightSq

theorem OAI.DefocusingNLS.expandingSobolevWeight_add_le line 71

Source documentation

The exact positive weight satisfies the two-term Young convolution inequality.

theorem expandingSobolevWeight_add_le (a k L : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (hL : 1 ≤ L) (m n : frequencyLattice) :
    expandingSobolevWeight a k L (m + n) ≤
      Real.sqrt (4 ^ k) * (expandingSobolevWeight a k L m + expandingSobolevWeight a k L n) := by
…

Mentions: OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.expandingSobolevWeight