HomogeneousWeakObservation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Weakly null data have vanishing local observation

This is the compact observation step in the time-one semigroup argument. Weak convergence is stated using bounded real-linear functionals, matching the real-linear Schrödinger linearization.

theorem OAI.DefocusingNLS.tendsto_homogeneousLocalObservation_of_weakNull line 19
theorem OAI.DefocusingNLS.tendsto_homogeneousLocalL2Observation_of_weakNull line 40

theorem OAI.DefocusingNLS.tendsto_homogeneousLinearized_localL2_of_weakNull line 58

Source documentation

At each fixed time the actual linearized evolution preserves weak nullity, so its local observation converges strongly to zero.

theorem tendsto_homogeneousLinearized_localL2_of_weakNull (a b k T R M : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (hT : 0 ≤ T)
    (m : ℕ) (q : HomogeneousY a k) (t : Icc (0 : ℝ) T)
    (u : ℕ → HomogeneousY a k) (hu : ∀ n, ‖u n‖ ≤ M)
    (hweak : ∀ ℓ : HomogeneousY a k →L[ℝ] ℂ,
      Tendsto (fun n => ℓ (u n)) atTop (𝓝 0)) :
    Tendsto (fun n => homogeneousLocalL2Observation a k R ha ha1 hk
      (homogeneousLinearizedPropagator a b k T ha ha1 hk hT m q (u n) t))
      atTop (𝓝 0) := by
…

Mentions: OAI.DefocusingNLS.HomogeneousY, OAI.DefocusingNLS.homogeneousLocalL2Observation, OAI.DefocusingNLS.homogeneousLinearizedPropagator