SobolevProductWeights.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The weight inequality needed for multiplication in the Sobolev Fourier model

def OAI.DefocusingNLS.sobolevProductWeight line 10
Source documentation
The positive Sobolev weight, inverse to the coefficient normalization.
Distinct definitions of this name: ComparatorChallenges/DefocusingNLS.lean:96 (same statement text; different proof or body). Qualify references as OAI.DefocusingNLS.sobolevProductWeight@path.
```
noncomputable def sobolevProductWeight (k : ℝ) (n : frequencyLattice) : ℝ :=
…
```
Mentions: OAI.DefocusingNLS.frequencyLattice
theorem OAI.DefocusingNLS.sobolevProductWeight_pos line 13

theorem OAI.DefocusingNLS.sobolevProductWeight_add_le line 17

Source documentation

A frequency sum costs at most a fixed multiple of either input weight.

theorem sobolevProductWeight_add_le (k : ℝ) (hk : 0 ≤ k) (m n : frequencyLattice) :
    sobolevProductWeight k (m + n) ≤ 4 ^ (k / 2) *
      (sobolevProductWeight k m + sobolevProductWeight k n) := by
…

Mentions: OAI.DefocusingNLS.frequencyLattice