OAI/MathematicalPhysics/DefocusingNLS/Linear/ObservationDecay.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Decay of the scalar observation term in the energy inequality

  1. def OAI.DefocusingNLS.observationDecayIntegral line 12
  2. theorem OAI.DefocusingNLS.observationDecayIntegral_nonneg line 15
  3. theorem OAI.DefocusingNLS.observationDecayIntegral_le line 19
  4. theorem OAI.DefocusingNLS.tendsto_observationDecayIntegral line 35
  5. def OAI.DefocusingNLS.escapedEnergyBound line 45
  6. theorem OAI.DefocusingNLS.tendsto_escapedEnergyBound line 48