OAI/MathematicalPhysics/DefocusingNLS/Certificates/ContinuousHalfLineBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Bounded extensions of continuous functions with a bounded tail.

  1. theorem OAI.DefocusingNLS.continuous_halfLine_bound line 15
  2. theorem OAI.DefocusingNLS.exists_bounded_extension_nonneg line 29
  3. theorem OAI.DefocusingNLS.continuous_tendsto_halfLine_bounded line 41