HomogeneousFourierMeasure.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The Fourier measure of the manuscript's homogeneous Hilbert space

Its L² norm is exactly the sum of the two homogeneous Sobolev energies, with the radian Plancherel factor (2π)^(-12). The measure is locally finite and has temperate growth, which permits the library's Schwartz density theorem.

def OAI.DefocusingNLS.homogeneousFourierWeight line 20
def OAI.DefocusingNLS.homogeneousFourierMeasure line 23
theorem OAI.DefocusingNLS.homogeneousFourierWeight_nonneg line 26
theorem OAI.DefocusingNLS.homogeneousFourierWeight_pos line 29
theorem OAI.DefocusingNLS.continuous_homogeneousFourierWeight line 35
theorem OAI.DefocusingNLS.homogeneousFourierMeasure_locallyFinite line 43
theorem OAI.DefocusingNLS.homogeneousFourierMeasure_openPos line 47
theorem OAI.DefocusingNLS.homogeneousFourierWeight_le line 59
theorem OAI.DefocusingNLS.homogeneousFourierMeasure_temperate line 75
Source documentation
The exact Fourier measure has the growth property required for Schwartz density.
```
theorem homogeneousFourierMeasure_temperate (a k : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) :
    (homogeneousFourierMeasure a k).HasTemperateGrowth := by
…
```
Mentions: OAI.DefocusingNLS.homogeneousFourierMeasure