OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousTimeObservation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Integrated compact observation for the actual linearized evolution

Bounded weakly null data have vanishing local observation integrated over any fixed time interval. This is the compact term used in the time-one energy argument; no spectral-decay assumption occurs here.

  1. theorem OAI.DefocusingNLS.tendsto_homogeneousLinearized_timeObservation line 17