SimilarityLimit.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Convergence of the similarity-time error, followed by the physical time change and phase cancellation, gives the rescaled pointwise blowup limit.

def OAI.DefocusingNLS.similarityTime line 19
theorem OAI.DefocusingNLS.similarityTime_tendsto line 21
def OAI.DefocusingNLS.similarityCenterValue line 37
Source documentation
The value at the blowup center after restoring amplitude and phase.
```
noncomputable def similarityCenterValue (T a θ b : ℝ) (Q : ℂ)
    (v : ℝ → ℂ) (t : ℝ) : ℂ :=
…
```
theorem OAI.DefocusingNLS.rescaled_similarityCenterValue_norm line 42
theorem OAI.DefocusingNLS.similarityCenterValue_rescaled_limit line 55
Source documentation
Convergence in similarity time yields the exact positive rescaled limit appearing in the main theorem, provided the center profile is nonzero.
```
theorem similarityCenterValue_rescaled_limit (T a θ b : ℝ) (Q : ℂ)
    (v : ℝ → ℂ) (hT : 0 < T) (hv : Tendsto v atTop (𝓝 0)) :
    Tendsto (fun t => (T - t) ^ a * ‖similarityCenterValue T a θ b Q v t‖)
      (𝓝[<] T) (𝓝 ‖Q‖) := by
…
```
Mentions: OAI.DefocusingNLS.similarityCenterValue
theorem OAI.DefocusingNLS.similarityCenterValue_no_left_limit line 66