HomogeneousInverseWeight.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Integrability of the inverse homogeneous Fourier weight

The low-frequency exponent is strictly below dimension twelve and the high-frequency exponent is strictly above it. This is the continuous counterpart of the checked expanding-torus inverse-weight sum.

theorem OAI.DefocusingNLS.homogeneousFourierWeight_inv_bound line 19
theorem OAI.DefocusingNLS.integrable_homogeneousFourierWeight_inv line 35
Source documentation
The inverse of the exact Y Fourier weight is integrable over all frequencies.
```
theorem integrable_homogeneousFourierWeight_inv (a k : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) :
    Integrable (fun ξ => (homogeneousFourierWeight a k ξ)⁻¹) := by
…
```
Mentions: OAI.DefocusingNLS.homogeneousFourierWeight