SchrodingerFlow.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

The linear Schrödinger group on the Fourier Sobolev model

Multiplication of each frequency by exp(-i t |n|²) defines a strongly continuous unitary group. The same coefficient model is used for every Sobolev index, so these isometries act on the paper's weighted Fourier spaces.

def OAI.DefocusingNLS.schrodingerMultiplier line 20
Source documentation
The exact free Schrödinger phase for a Fourier frequency.
Also declared: ComparatorChallenges/DefocusingNLS.lean:127 (same declaration text).
```
noncomputable def schrodingerMultiplier (t : ℝ) (n : frequencyLattice) : ℂ :=
…
```
Mentions: OAI.DefocusingNLS.frequencyLattice
theorem OAI.DefocusingNLS.schrodingerMultiplier_norm line 23
theorem OAI.DefocusingNLS.schrodingerMultiplier_zero line 29
theorem OAI.DefocusingNLS.schrodingerMultiplier_add line 33
theorem OAI.DefocusingNLS.continuous_schrodingerMultiplier line 42
def OAI.DefocusingNLS.schrodingerFlow line 48
Source documentation
Free evolution preserves the norm of every weighted Fourier vector.
Distinct definitions of this name: ComparatorChallenges/DefocusingNLS.lean:130 (same statement text; different proof or body). Qualify references as OAI.DefocusingNLS.schrodingerFlow@path.
```
noncomputable def schrodingerFlow (t : ℝ) : FourierL2 →ₗᵢ[ℂ] FourierL2 where
…
```
Mentions: OAI.DefocusingNLS.FourierL2
theorem OAI.DefocusingNLS.schrodingerFlow_apply line 66
theorem OAI.DefocusingNLS.schrodingerFlow_zero line 69
theorem OAI.DefocusingNLS.schrodingerFlow_add line 73
def OAI.DefocusingNLS.schrodingerUnitary line 79
Source documentation
Free evolution is a complex-linear isometric equivalence, with inverse time -t.
```
noncomputable def schrodingerUnitary (t : ℝ) : FourierL2 ≃ₗᵢ[ℂ] FourierL2 :=
…
```
Mentions: OAI.DefocusingNLS.FourierL2
theorem OAI.DefocusingNLS.schrodingerUnitary_apply line 86
theorem OAI.DefocusingNLS.continuous_schrodingerFlow line 90
Source documentation
The free evolution is strongly continuous in every Fourier Sobolev norm.
```
theorem continuous_schrodingerFlow (f : FourierL2) :
    Continuous (fun t : ℝ => schrodingerFlow t f) := by
…
```
Mentions: OAI.DefocusingNLS.FourierL2