OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousEulerRecurrence.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact finite recurrence for high physical radial derivatives

In logarithmic radius the falling Euler derivatives are represented by two operator rows. This is an identity for the original second-order equation, not an asymptotic ansatz for a fast solution.

  1. def OAI.DefocusingNLS.homogeneousEulerDeriv line 21
  2. def OAI.DefocusingNLS.homogeneousEulerRows line 26
  3. theorem OAI.DefocusingNLS.homogeneousEulerRows_smooth line 34
  4. theorem OAI.DefocusingNLS.homogeneousEulerRows_identity line 46
  5. theorem OAI.DefocusingNLS.homogeneousEulerRows_outgoing_remainder line 82

    Source documentation

    At each derivative order the value-row remainder is exactly the corresponding derivative of the two outgoing columns.

    theorem homogeneousEulerRows_outgoing_remainder
    (B C : ℝ → End) (u v du dv : ℝ → V) (L : ℝ)
    (hB : ContDiffOn ℝ ∞ B (Ioi L)) (hC : ContDiffOn ℝ ∞ C (Ioi L))
    (hu : ∀ t, L < t → HasDerivAt u (du t) t)
    (hv : ∀ t, L < t → HasDerivAt v (dv t) t)
    (hdu : ∀ t, L < t → HasDerivAt du (-B t (du t) - C t (u t)) t)
    (hdv : ∀ t, L < t → HasDerivAt dv (-B t (dv t) - C t (v t)) t)
    (n : ℕ) (t : ℝ) (ht : L < t) (hdet : spectralValueDet (u t) (v t) ≠ 0) :
    (homogeneousEulerRows B C n).1 t +
        (homogeneousEulerRows B C n).2 t * spectralRobinOperator (u t) (v t) (du t) (dv t) =
      spectralTwoColumns (homogeneousEulerDeriv u n t) (homogeneousEulerDeriv v n t) *
        spectralValueInverse (u t) (v t) := by
…

    Mentions: OAI.DefocusingNLS.spectralValueDet, OAI.DefocusingNLS.homogeneousEulerRows, OAI.DefocusingNLS.spectralRobinOperator, OAI.DefocusingNLS.spectralTwoColumns, OAI.DefocusingNLS.homogeneousEulerDeriv, OAI.DefocusingNLS.spectralValueInverse