SobolevPhase.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Unit-phase covariance of the Sobolev Schrödinger equation

def OAI.DefocusingNLS.sobolevPhase line 12
Source documentation
Multiplication by a constant unit complex phase is an isometry.
```
noncomputable def sobolevPhase (c : Circle) : FourierL2 →ₗᵢ[ℂ] FourierL2 where
…
```
Mentions: OAI.DefocusingNLS.FourierL2
theorem OAI.DefocusingNLS.sobolevPhase_apply line 20
theorem OAI.DefocusingNLS.continuous_sobolevPhase_uncurry line 23
theorem OAI.DefocusingNLS.fourierConjugate_smul line 27
theorem OAI.DefocusingNLS.sobolevOddPower_phase line 33
Source documentation
Odd powers commute with every constant phase of modulus one.
```
theorem sobolevOddPower_phase (k : ℝ) (hk : 6 < k) (m : ℕ) (c : Circle) (f : FourierL2) :
    sobolevOddPower k hk m (sobolevPhase c f) =
      sobolevPhase c (sobolevOddPower k hk m f) := by
…
```
Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.sobolevPhase
theorem OAI.DefocusingNLS.sobolevTorusFunction_phase line 50

theorem OAI.DefocusingNLS.hasDerivAt_sobolevSchrodinger_phase line 56

Source documentation

The actual strong equation is invariant under unit phase.

theorem hasDerivAt_sobolevSchrodinger_phase
    (k : ℝ) (hk : 6 < k) (m : ℕ) (c : Circle) (u : ℝ → FourierL2) (t : ℝ)
    (hu : HasDerivAt (fun s => lowerSobolevInclusion (u s))
      (lowerSobolevGenerator (u t) -
        Complex.I • lowerSobolevInclusion (sobolevOddPower k hk m (u t))) t) :
    HasDerivAt (fun s => lowerSobolevInclusion (sobolevPhase c (u s)))
      (lowerSobolevGenerator (sobolevPhase c (u t)) -
        Complex.I • lowerSobolevInclusion
          (sobolevOddPower k hk m (sobolevPhase c (u t)))) t := by
…

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.lowerSobolevInclusion, OAI.DefocusingNLS.sobolevPhase