CutoffNormalizedEquation.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The cutoff defect in the fixed normalized spatial coordinate

theorem OAI.DefocusingNLS.laplacian_complex_dilation line 13

theorem OAI.DefocusingNLS.cutoff_normalized_similarity_defect line 28

Source documentation

Exact fixed-coordinate equation, with both the profile defect and cutoff residual visible.

theorem cutoff_normalized_similarity_defect (a b R : ℝ) (hR : 0 < R) (m : ℕ)
    (χ : E → ℝ) (hχ : ContDiff ℝ ∞ χ) (Q : E → ℂ) (hQ : ContDiff ℝ ∞ Q) (x : E) :
    Complex.I * ((χ x : ℂ) * fderiv ℝ Q (R • x) ((R / 2) • x)) +
      ((R ^ (2 : ℕ))⁻¹ : ℝ) • Δ (fun z => (χ z : ℂ) * Q (R • z)) x +
      (Complex.I * (a : ℂ) + (b : ℂ)) * ((χ x : ℂ) * Q (R • x)) -
      oddPowerNonlinearity m ((χ x : ℂ) * Q (R • x)) =
        (χ x : ℂ) * stationarySimilarityDefect a b m Q (R • x) +
          cutoffResidual m R χ Q (R • x) := by
…

Mentions: OAI.DefocusingNLS.oddPowerNonlinearity, OAI.DefocusingNLS.stationarySimilarityDefect, OAI.DefocusingNLS.cutoffResidual