LocalizationWeightComparison.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Exact expanding-weight comparisons for localization

The high-order localized norm produces a harmless additional zero-frequency term. It is absorbed by the regularized low-order part of the exact Y_L weight.

theorem OAI.DefocusingNLS.localization_high_bessel_le line 13
theorem OAI.DefocusingNLS.localization_low_weight_le line 28
theorem OAI.DefocusingNLS.localization_high_weight_le line 34
Source documentation
The extra high-order Bessel term is uniformly absorbed by the exact Y_L weight.
```
theorem localization_high_weight_le (a k L : ℝ) (ha : 0 < a) (ha1 : a < 1)
    (hk : 8 < k) (hL : 1 ≤ L) (n : frequencyLattice) :
    L ^ (12 - 2 * k) * (1 + ‖n‖ ^ 2) ^ k ≤
      2 ^ k * expandingSobolevWeightSq a k L n := by
…
```
Mentions: OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.expandingSobolevWeightSq