OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingProfileObservation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual torus propagator obeys the compact-observation energy estimate

  1. theorem OAI.DefocusingNLS.expandingProfileTrajectory_observation_estimate line 13