HomogeneousYSpace.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The homogeneous space Y as a completed Fourier Hilbert space

The weighted L² model is complete. The radian Fourier image of Schwartz is dense and injective, so this is precisely a completion of the Schwartz domain with the homogeneous norm, rather than an added global L² requirement.

abbrev OAI.DefocusingNLS.HomogeneousY line 20
def OAI.DefocusingNLS.radianFourierCLM line 22
theorem OAI.DefocusingNLS.radianFourierCLM_apply line 27
theorem OAI.DefocusingNLS.radianFourierKernel_injective line 30
theorem OAI.DefocusingNLS.radianFourierKernel_surjective line 42
def OAI.DefocusingNLS.homogeneousSchwartzEmbedding line 54
theorem OAI.DefocusingNLS.homogeneousSchwartzEmbedding_apply line 59
theorem OAI.DefocusingNLS.homogeneousSchwartzEmbedding_dense line 66
Source documentation
The Schwartz Fourier domain is dense in the completed homogeneous space.
```
theorem homogeneousSchwartzEmbedding_dense (a k : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) :
    DenseRange (homogeneousSchwartzEmbedding a k ha ha1 hk) := by
…
```
Mentions: OAI.DefocusingNLS.homogeneousSchwartzEmbedding
theorem OAI.DefocusingNLS.homogeneousSchwartzEmbedding_injective line 77
Source documentation
No nonzero Schwartz function is identified with zero in this completion.
```
theorem homogeneousSchwartzEmbedding_injective (a k : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) :
    Function.Injective (homogeneousSchwartzEmbedding a k ha ha1 hk) := by
…
```
Mentions: OAI.DefocusingNLS.homogeneousSchwartzEmbedding