SchrodingerGenerator.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Two-derivative loss for the free Schrödinger evolution

In the common weighted-ℓ² model, the inclusion from H^k to H^(k-2) multiplies by (1+|n|²)⁻¹. The time derivative is the bounded multiplier -i |n|²/(1+|n|²). Finite Fourier sums give the derivative of the full flow by uniform convergence of their derivatives.

def OAI.DefocusingNLS.fourierContraction line 23
Source documentation
A bounded Fourier multiplier of norm at most one.
Also declared: ComparatorChallenges/DefocusingNLS.lean:163 (same declaration text).
```
noncomputable def fourierContraction (m : frequencyLattice → ℂ)
    (hm : ∀ n, ‖m n‖ ≤ 1) : FourierL2 →L[ℂ] FourierL2 :=
…
```
Mentions: OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.FourierL2
theorem OAI.DefocusingNLS.fourierContraction_apply line 49
def OAI.DefocusingNLS.lowerSobolevInclusion line 54
Source documentation
The continuous inclusion from H^k into H^(k-2), in weighted coordinates.
Also declared: ComparatorChallenges/DefocusingNLS.lean:189 (same declaration text).
```
noncomputable def lowerSobolevInclusion : FourierL2 →L[ℂ] FourierL2 :=
…
```
Mentions: OAI.DefocusingNLS.FourierL2
def OAI.DefocusingNLS.lowerSobolevGenerator line 61
Source documentation
The free Schrödinger generator, with the loss of two Sobolev derivatives.
Distinct definitions of this name: ComparatorChallenges/DefocusingNLS.lean:195 (same statement text; different proof or body). Qualify references as OAI.DefocusingNLS.lowerSobolevGenerator@path.
```
noncomputable def lowerSobolevGenerator : FourierL2 →L[ℂ] FourierL2 :=
…
```
Mentions: OAI.DefocusingNLS.FourierL2
theorem OAI.DefocusingNLS.lowerSobolevInclusion_apply line 68
theorem OAI.DefocusingNLS.lowerSobolevGenerator_apply line 71
theorem OAI.DefocusingNLS.sobolevFourierCoefficient_lower_inclusion line 76
Source documentation
The inclusion changes the Sobolev index without changing physical Fourier coefficients.
```
theorem sobolevFourierCoefficient_lower_inclusion (k : ℝ) (f : FourierL2)
    (n : frequencyLattice) :
    sobolevFourierCoefficient (k - 2) (lowerSobolevInclusion f) n =
      sobolevFourierCoefficient k f n := by
…
```
Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.sobolevFourierCoefficient, OAI.DefocusingNLS.lowerSobolevInclusion
theorem OAI.DefocusingNLS.schrodingerFlow_single line 91
Source documentation
Applying the free group to one coordinate keeps that coordinate.
```
theorem schrodingerFlow_single (t : ℝ) (n : frequencyLattice) (c : ℂ) :
    schrodingerFlow t (lp.single 2 n c) =
      lp.single 2 n (schrodingerMultiplier t n * c) := by
…
```
Mentions: OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.schrodingerMultiplier
theorem OAI.DefocusingNLS.tendstoUniformly_schrodingerFlow_partials line 101
Source documentation
Uniform-in-time convergence of the finite Fourier approximations.
```
theorem tendstoUniformly_schrodingerFlow_partials (f : FourierL2) :
    TendstoUniformly
      (fun S : Finset frequencyLattice => fun t : ℝ =>
        ∑ n ∈ S, lp.single 2 n (schrodingerMultiplier t n * f n))
      (fun t => schrodingerFlow t f) atTop := by
…
```
Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.schrodingerMultiplier

theorem OAI.DefocusingNLS.hasDerivAt_schrodingerMultiplier_mul line 118

Source documentation

The scalar phase has the exact Schrödinger derivative.

theorem hasDerivAt_schrodingerMultiplier_mul (n : frequencyLattice) (c : ℂ) (t : ℝ) :
    HasDerivAt (fun s : ℝ => schrodingerMultiplier s n * c)
      (schrodingerMultiplier t n * (-Complex.I * ((‖n‖ ^ 2 : ℝ) : ℂ) * c)) t := by
…

Mentions: OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.schrodingerMultiplier

theorem OAI.DefocusingNLS.hasDerivAt_schrodingerFlow_of_generator line 127
Source documentation
Coordinatewise Schrödinger differentiation yields differentiation in ℓ² when the derivative coordinates also form an ℓ² vector.
```
theorem hasDerivAt_schrodingerFlow_of_generator (f v : FourierL2)
    (hv : ∀ n, v n = -Complex.I * ((‖n‖ ^ 2 : ℝ) : ℂ) * f n) (t : ℝ) :
    HasDerivAt (fun s : ℝ => schrodingerFlow s f) (schrodingerFlow t v) t := by
…
```
Mentions: OAI.DefocusingNLS.FourierL2
theorem OAI.DefocusingNLS.hasDerivAt_lowerSobolev_schrodingerFlow line 142
Source documentation
The free evolution is differentiable as an H^(k-2)-valued function.
```
theorem hasDerivAt_lowerSobolev_schrodingerFlow (f : FourierL2) (t : ℝ) :
    HasDerivAt (fun s => schrodingerFlow s (lowerSobolevInclusion f))
      (schrodingerFlow t (lowerSobolevGenerator f)) t := by
…
```
Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.lowerSobolevInclusion