ExpandingSequentialObservation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A local observation threshold from the expanding-domain sequence criterion

theorem OAI.DefocusingNLS.exists_expanding_observation_threshold line 17

Source documentation

A functional vanishing on all bounded, locally null sequences has a uniform smallness threshold on a sufficiently large physical ball.

theorem exists_expanding_observation_threshold (a k : ℝ)
    (F : Radius → FourierL2 → ℝ)
    (hseq : ∀ (L : ℕ → Radius), Tendsto (fun n => (L n).1) atTop atTop →
      ∀ (f : ℕ → FourierL2), (∀ n, ‖f n‖ ≤ 1) →
      (∀ R ε : ℝ, 0 < ε → ∀ᶠ n in atTop, ∀ y : E, ‖y‖ ≤ R →
        ‖expandingTorusFunction a k (L n).1 (f n)
          (euclideanToTorus ((L n).1⁻¹ • y))‖ < ε) →
      Tendsto (fun n => F (L n) (f n)) atTop (𝓝 0))
    (ε : ℝ) (hε : 0 < ε) :
    ∃ n : ℕ, ∀ (L : Radius), (n : ℝ) ≤ L.1 → ∀ f : FourierL2,
      ‖f‖ ≤ 1 →
      (∀ y : E, ‖y‖ ≤ (n : ℝ) →
…

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.expandingTorusFunction, OAI.DefocusingNLS.euclideanToTorus