OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialExteriorOutgoing.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A precise outgoing class selected by the nonlinear asymptotic expansion.

  1. theorem OAI.DefocusingNLS.continuous_radialExterior_polynomialCorrection line 12
  2. def OAI.DefocusingNLS.radialExteriorODEField line 19
  3. theorem OAI.DefocusingNLS.radialExteriorODEField_split line 23
  4. def OAI.DefocusingNLS.HasRadialOutgoingExpansion line 33

    Source documentation

    A finite but sufficiently accurate outgoing expansion, including the velocity.

    def HasRadialOutgoingExpansion (ν : ℂ) (n : ℕ) (m : ℂ) (Z : ℝ → ℂ × ℂ) : Prop :=
…
  5. theorem OAI.DefocusingNLS.HasRadialOutgoingExpansion.tendsto line 39
  6. theorem OAI.DefocusingNLS.HasRadialOutgoingExpansion.congr line 53
  7. theorem OAI.DefocusingNLS.radialExterior_outgoing_eventually_eq line 63
  8. theorem OAI.DefocusingNLS.exists_radialExterior_outgoing line 93