ExpandingFreeStep.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

The exact free step on expanding tori

This is the normalized-coordinate form of manuscript (lin:free-flow), including the amplitude and the change from Y_L to Y_(L exp(s/2)).

def OAI.DefocusingNLS.expandingRadius line 13
theorem OAI.DefocusingNLS.expandingRadius_ge line 15
def OAI.DefocusingNLS.expandingFreeTime line 20
def OAI.DefocusingNLS.expandingFreeAmplitude line 23
theorem OAI.DefocusingNLS.expandingFreeAmplitude_norm line 26
theorem OAI.DefocusingNLS.expandingRadius_add line 30
theorem OAI.DefocusingNLS.expandingFreeAmplitude_add line 37
theorem OAI.DefocusingNLS.expandingFreeTime_add line 46
def OAI.DefocusingNLS.expandingFreeStep line 59
Source documentation
The free moving-scale operator, including the scalar similarity factor.
```
noncomputable def expandingFreeStep (a b k L s : ℝ)
    (ha : 0 < a) (hk : 8 < k) (hL : 1 ≤ L) (hs : 0 ≤ s) :
    FourierL2 →L[ℂ] FourierL2 :=
…
```
Mentions: OAI.DefocusingNLS.FourierL2
theorem OAI.DefocusingNLS.expandingFreeStep_apply line 67
theorem OAI.DefocusingNLS.expandingFreeStep_factor line 75
Source documentation
The exact cancellation of the amplitude against the changing Sobolev weight.
```
theorem expandingFreeStep_factor (a L s : ℝ) (hL : 1 ≤ L) :
    Real.exp (-a * s) * (expandingRadius L s / L) ^ a = Real.exp (-a * s / 2) := by
…
```
Mentions: OAI.DefocusingNLS.expandingRadius

theorem OAI.DefocusingNLS.expandingFreeStep_norm_bound line 86

Source documentation

The free step decays in the exact Y_L norms, uniformly in the starting scale.

theorem expandingFreeStep_norm_bound (a b k L s : ℝ)
    (ha : 0 < a) (hk : 8 < k) (hL : 1 ≤ L) (hs : 0 ≤ s) (f : FourierL2) :
    ‖expandingFreeStep a b k L s ha hk hL hs f‖ ≤ Real.exp (-a * s / 2) * ‖f‖ := by
…

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.expandingFreeStep

theorem OAI.DefocusingNLS.expandingFreeStep_opNorm_le line 99
theorem OAI.DefocusingNLS.expandingFourierCoefficient_schrodingerFlow line 105
theorem OAI.DefocusingNLS.expandingFreeStep_coefficient line 113
Source documentation
The physical coefficients have exactly the phase in the manuscript's free formula.
```
theorem expandingFreeStep_coefficient (a b k L s : ℝ)
    (ha : 0 < a) (hk : 8 < k) (hL : 1 ≤ L) (hs : 0 ≤ s)
    (f : FourierL2) (n : frequencyLattice) :
    expandingFourierCoefficient a k (expandingRadius L s)
        (expandingFreeStep a b k L s ha hk hL hs f) n =
      expandingFreeAmplitude a b s * schrodingerMultiplier (expandingFreeTime L s) n *
        expandingFourierCoefficient a k L f n := by
…
```
Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.expandingFourierCoefficient, OAI.DefocusingNLS.expandingRadius, OAI.DefocusingNLS.expandingFreeStep, OAI.DefocusingNLS.expandingFreeAmplitude, OAI.DefocusingNLS.schrodingerMultiplier, OAI.DefocusingNLS.expandingFreeTime
theorem OAI.DefocusingNLS.expandingFreeStep_zero line 123
theorem OAI.DefocusingNLS.freeStep_coefficients_injective line 129

theorem OAI.DefocusingNLS.expandingFreeStep_add line 138

Source documentation

The free steps form the forward propagator on the moving family of tori.

theorem expandingFreeStep_add (a b k L s t : ℝ)
    (ha : 0 < a) (hk : 8 < k) (hL : 1 ≤ L) (hs : 0 ≤ s) (ht : 0 ≤ t) :
    (expandingFreeStep a b k (expandingRadius L s) t ha hk
        (hL.trans (expandingRadius_ge L s hL hs)) ht).comp
      (expandingFreeStep a b k L s ha hk hL hs) =
      expandingFreeStep a b k L (s + t) ha hk hL (add_nonneg hs ht) := by
…

Mentions: OAI.DefocusingNLS.expandingFreeStep, OAI.DefocusingNLS.expandingRadius, OAI.DefocusingNLS.expandingRadius_ge