OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingBlowupObservation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Point observations of the actual similarity perturbation

The center of the sampled cutoff profile equals Q 0 exactly. The uniform expanding-space evaluation bound therefore transfers norm decay to the pointwise convergence required by the manuscript's final blowup statement.

  1. theorem OAI.DefocusingNLS.expandingInverseTransfer_function line 21
  2. theorem OAI.DefocusingNLS.expandingSobolev_observation line 34
  3. theorem OAI.DefocusingNLS.sampledCutoffProfile_center line 43
  4. theorem OAI.DefocusingNLS.expanding_observation_difference_le line 63
  5. theorem OAI.DefocusingNLS.expanding_observation_tendsto_of_norm_decay line 75

    Source documentation

    Decay of the similarity perturbation determines the limiting point observation.

    theorem expanding_observation_tendsto_of_norm_decay (a k L : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (hL : 1 ≤ L)
    (u q : ℝ → FourierL2) (x : SchrodingerTorus) (c : ℂ)
    (hq : ∀ s, 0 ≤ s → expandingTorusFunction a k (expandingRadius L s) (q s) x = c)
    (hdecay : Tendsto (fun s => ‖u s - q s‖) atTop (𝓝 0)) :
    Tendsto (fun s => expandingTorusFunction a k (expandingRadius L s) (u s) x)
      atTop (𝓝 c) := by
…

    Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.SchrodingerTorus, OAI.DefocusingNLS.expandingTorusFunction, OAI.DefocusingNLS.expandingRadius