SchrodingerInteraction.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The interaction representation of the semilinear Schrödinger equation

theorem OAI.DefocusingNLS.continuous_schrodingerFlow_uncurry line 13
Source documentation
Strong continuity and the uniform isometry bound give joint continuity.
```
theorem continuous_schrodingerFlow_uncurry :
    Continuous (fun p : ℝ × FourierL2 => schrodingerFlow p.1 p.2) := by
…
```
Mentions: OAI.DefocusingNLS.FourierL2
def OAI.DefocusingNLS.schrodingerInteractionField line 35
Source documentation
The derivative field for v(t) = S(-t)u(t) in the defocusing equation.
Distinct definitions of this name: ComparatorChallenges/DefocusingNLS.lean:204 (same statement text; different proof or body). Qualify references as OAI.DefocusingNLS.schrodingerInteractionField@path.
```
noncomputable def schrodingerInteractionField (k : ℝ) (hk : 6 < k) (m : ℕ)
    (t : ℝ) (f : FourierL2) : FourierL2 :=
…
```
Mentions: OAI.DefocusingNLS.FourierL2
theorem OAI.DefocusingNLS.continuous_schrodingerInteractionField line 39
theorem OAI.DefocusingNLS.norm_schrodingerInteractionField line 47
theorem OAI.DefocusingNLS.norm_schrodingerInteractionField_sub line 53

theorem OAI.DefocusingNLS.exists_schrodingerInteractionField_ball_bounds line 63

Source documentation

The interaction vector field has time-uniform bounds and Lipschitz constants on norm balls.

theorem exists_schrodingerInteractionField_ball_bounds (k : ℝ) (hk : 6 < k) (m : ℕ)
    (R : ℝ) (hR : 0 ≤ R) :
    ∃ A K : ℝ, 0 ≤ A ∧ 0 ≤ K ∧
      (∀ t (f : FourierL2), ‖f‖ ≤ R → ‖schrodingerInteractionField k hk m t f‖ ≤ A) ∧
      (∀ t (f g : FourierL2), ‖f‖ ≤ R → ‖g‖ ≤ R →
        ‖schrodingerInteractionField k hk m t f -
          schrodingerInteractionField k hk m t g‖ ≤ K * ‖f - g‖) := by
…

Mentions: OAI.DefocusingNLS.FourierL2