OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialOutgoingBoundary.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Outgoing decay makes every spectral energy boundary trace vanish.

  1. def OAI.DefocusingNLS.HasRadialEnergyDecay line 14

    Source documentation

    The first two outgoing symbol estimates needed when Re λ ≥ 4.

    def HasRadialEnergyDecay (f : ℝ → ℝ) : Prop :=
…
  2. theorem OAI.DefocusingNLS.radialSpectralBoundary_tendsto line 18
  3. theorem OAI.DefocusingNLS.radialHardyBoundary_tendsto line 42
  4. theorem OAI.DefocusingNLS.radialMatched_weight_bigO line 53