CutoffMovingPath.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Actual cutoff profiles and residuals along the expanding radius

The sampled profile and its exact PDE residual are continuous histories on any finite time slab. The residual decay retains the starting-scale factor.

def OAI.DefocusingNLS.sampledCutoffProfilePath line 19
def OAI.DefocusingNLS.sampledCutoffResidualPath line 29
theorem OAI.DefocusingNLS.expandingRadius_residual_power line 41

theorem OAI.DefocusingNLS.exists_sampledCutoffResidualPath_bound line 50

Source documentation

The same constant controls every starting radius and every time slab.

theorem exists_sampledCutoffResidualPath_bound (a k : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k)
    (χ : 𝓢(E, ℝ)) (hχ : HasCompactSupport (χ : E → ℝ))
    (hχone : ∀ x : E, ‖x‖ < 1 / 2 → χ x = 1)
    (hχzero : ∀ x : E, 2 < ‖x‖ → χ x = 0) (m : ℕ) :
    ∃ N : ℕ, ∀ (Q : E → ℂ) (hQ : ContDiff ℝ ∞ Q) (D : ℝ), 0 ≤ D →
      (∀ n ≤ N, ∀ y : E, y ≠ 0 →
        ‖iteratedFDeriv ℝ n Q y‖ ≤ D * ‖y‖ ^ (-2 * a - (n : ℝ))) →
      ∃ C : ℝ, 0 ≤ C ∧ ∀ (L T : ℝ) (hL : 1 ≤ L) (t : Icc (0 : ℝ) T),
        ‖sampledCutoffResidualPath a k L T ha ha1 hk hL χ hχ hχone hχzero m Q hQ t‖ ≤
          C * L ^ (-2 - a) * Real.exp (-(2 + a) * (t : ℝ) / 2) := by
…

Mentions: OAI.DefocusingNLS.sampledCutoffResidualPath