HomogeneousLocalizationPhysical.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The map into the completed homogeneous space represents the actual cutoff χ(y/L)v(y) at every point, not only almost everywhere in Fourier variables.

theorem OAI.DefocusingNLS.continuous_expandingPhysicalLocalization line 20
theorem OAI.DefocusingNLS.homogeneousLocalization_physical line 28
Source documentation
The completed-space localization is pointwise the cutoff of the actual torus function.
```
theorem homogeneousLocalization_physical (a k L : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (hL : 1 ≤ L)
    (χ : 𝓢(E, ℂ)) (f : FourierL2) (y : E) :
    homogeneousPhysicalCLM a k ha ha1 hk
      (homogeneousLocalizationCLM a k L ha ha1 hk hL χ f) y =
        expandingPhysicalLocalization a k L χ f y := by
…
```
Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.homogeneousPhysicalCLM, OAI.DefocusingNLS.homogeneousLocalizationCLM, OAI.DefocusingNLS.expandingPhysicalLocalization