ExpandingLocalizationEnergy.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform two-order localization energy bound

This combines the mixed Fourier estimate with precisely the manuscript's Y_L weights at s₀ = 6-a and k. It is the finite Fourier energy estimate; the physical cutoff and Fourier-normalization identification is separate.

theorem OAI.DefocusingNLS.exists_expanding_localization_energy_bound line 18