OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousSemigroupDecay.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

From a decaying time step to continuous-time decay

Strong continuity gives the bounded propagation on one compact time interval. The remaining estimate is a division of time into integral steps and one bounded remainder interval.

  1. theorem OAI.DefocusingNLS.stronglyContinuous_family_compact_bound line 23
  2. theorem OAI.DefocusingNLS.semigroup_nat_mul line 35
  3. theorem OAI.DefocusingNLS.continuous_decay_of_step_decay line 44