ExpandingSobolevWeights.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Exact weights of the expanding-torus Sobolev norm

The norm from manuscript (lin:YL), after extracting (2π)^12, has squared Fourier weight L^(2a) ⟨n⟩^(12-2a) + L^(12-2k) |n|^(2k). The auxiliary one-dimensional weights will control its inverse sum.

def OAI.DefocusingNLS.expandingSobolevWeightSq line 18
def OAI.DefocusingNLS.expandingOneDimWeight line 21
def OAI.DefocusingNLS.expandingOneDimKernel line 25
theorem OAI.DefocusingNLS.expandingSobolevWeightSq_pos line 28
theorem OAI.DefocusingNLS.expandingOneDimWeight_pos line 34
theorem OAI.DefocusingNLS.expandingOneDimKernel_nonneg line 40
theorem OAI.DefocusingNLS.expandingOneDimKernel_even line 44
theorem OAI.DefocusingNLS.expandingOneDimKernel_zero_le line 48
theorem OAI.DefocusingNLS.expandingOneDimKernel_antitone line 56
theorem OAI.DefocusingNLS.expandingOneDimKernel_le_low line 71
Source documentation
Below the scale, the inverse weight is controlled by the locally integrable power.
```
theorem expandingOneDimKernel_le_low (a k L x : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hL : 1 ≤ L) (hx : 0 < x) :
    expandingOneDimKernel a k L x ≤ L ^ (-a / 6) * x ^ (a / 6 - 1) := by
…
```
Mentions: OAI.DefocusingNLS.expandingOneDimKernel
theorem OAI.DefocusingNLS.expandingOneDimKernel_le_high line 95
Source documentation
Above the scale, the inverse weight has an integrable high-order tail.
```
theorem expandingOneDimKernel_le_high (a k L x : ℝ) (hL : 1 ≤ L) (hx : 0 < x) :
    expandingOneDimKernel a k L x ≤ L ^ (k / 6 - 1) * x ^ (-k / 6) := by
…
```
Mentions: OAI.DefocusingNLS.expandingOneDimKernel

theorem OAI.DefocusingNLS.expandingSobolevWeightSq_original line 112

Source documentation

The normalized weight is exactly the manuscript's volume-weighted Fourier density.

theorem expandingSobolevWeightSq_original (a k L : ℝ) (hL : 1 ≤ L) (n : frequencyLattice) :
    (2 * Real.pi * L) ^ 12 *
        ((L ^ (-2 : ℝ) + (‖n‖ / L) ^ 2) ^ (6 - a) + (‖n‖ / L) ^ (2 * k)) =
      (2 * Real.pi) ^ 12 * expandingSobolevWeightSq a k L n := by
…

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