ExpandingWeightIdentification.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The two-sided identification between exact expanding Sobolev spaces

The radius-one weight identifies every Y_L, L ≥ 1, with the same Hilbert space. Both this identification and its inverse depend continuously on L.

theorem OAI.DefocusingNLS.expandingSobolevWeight_one_le line 18
Source documentation
The inverse identification loses at most the explicit high-frequency scale factor.
```
theorem expandingSobolevWeight_one_le (a k L : ℝ)
    (ha : 0 < a) (hk : 8 < k) (hL : 1 ≤ L) (n : frequencyLattice) :
    expandingSobolevWeight a k 1 n ≤ L ^ (k - 6) * expandingSobolevWeight a k L n := by
…
```
Mentions: OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.expandingSobolevWeight
def OAI.DefocusingNLS.expandingInverseRatio line 45
theorem OAI.DefocusingNLS.expandingInverseRatio_nonneg line 48
theorem OAI.DefocusingNLS.expandingInverseRatio_le line 53
def OAI.DefocusingNLS.expandingInverseVector line 58
theorem OAI.DefocusingNLS.expandingInverseVector_norm_le line 68
def OAI.DefocusingNLS.expandingInverseTransfer line 83
def OAI.DefocusingNLS.expandingWeightUnit line 102
Source documentation
Two-sided inverse of the canonical radius-one identification.
```
noncomputable def expandingWeightUnit (a k L : ℝ) (ha : 0 < a) (hk : 8 < k)
    (hL : 1 ≤ L) : (FourierL2 →L[ℂ] FourierL2)ˣ where
…
```
Mentions: OAI.DefocusingNLS.FourierL2
theorem OAI.DefocusingNLS.continuous_expandingInverseTransfer line 125