HomogeneousEulerBounds.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Leading high-derivative row of the radial spectral equation

The original logarithmic damping is an exponential diagonal plus a bounded matrix. Repeated falling-Euler differentiation produces its powers as the leading velocity coefficient. The remaining coefficient is two powers of radius smaller; this is an operator statement for both channels together.

theorem OAI.DefocusingNLS.eulerRows_one line 22
theorem OAI.DefocusingNLS.homogeneousEulerRows_bound line 27
def OAI.DefocusingNLS.homogeneousEulerLeading line 61
theorem OAI.DefocusingNLS.homogeneousEulerLeading_step line 64
theorem OAI.DefocusingNLS.homogeneousEulerRows_leading line 78

theorem OAI.DefocusingNLS.homogeneousEulerRows_norm_lower line 123

Source documentation

The actual leading diagonal has a positive lower stretch. The operator error is uniformly smaller, simultaneously for all vectors in both channels.

theorem homogeneousEulerRows_norm_lower (B C : ℝ → End) (D : End) (B₀ : ℝ → End)
    (hB₀ : HasLogJetBound 0 B₀) (hC : HasLogJetBound 2 C)
    (hB : ∀ t, B t = B₀ t + Real.exp (2 * t) • D)
    (c : ℝ) (hc : 0 < c) (hD : ∀ w : V, ‖D w‖ = c * ‖w‖) (n : ℕ) :
    ∀ᶠ t : ℝ in atTop, ∀ w : V,
      (c ^ n / 2) * Real.exp (2 * (n : ℝ) * t) * ‖w‖ ≤
        ‖(homogeneousEulerRows B C (n + 1)).2 t w‖ := by
…

Mentions: OAI.DefocusingNLS.HasLogJetBound, OAI.DefocusingNLS.homogeneousEulerRows