CutoffApproximateMode.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The actual sampled cutoff profile satisfies the forced mode equation

The smooth stationary-profile premise is explicit. The forcing is the already constructed three-term cutoff residual, with the same physical normalization.

theorem OAI.DefocusingNLS.cutoffProfileSchwartz_dilation_zero line 17
theorem OAI.DefocusingNLS.schwartzOddPower_dilation_zero line 27
theorem OAI.DefocusingNLS.cutoffProfileSchwartz_zero_outside line 35
theorem OAI.DefocusingNLS.cutoff_normalized_nonlinearity_coefficient line 47
theorem OAI.DefocusingNLS.cutoff_normalized_defect_coefficient line 68
def OAI.DefocusingNLS.cutoffSampledMode line 92
theorem OAI.DefocusingNLS.cutoffSampledMode_eq_physical line 97
theorem OAI.DefocusingNLS.hasDerivAt_cutoffSampledMode line 107

theorem OAI.DefocusingNLS.hasDerivAt_cutoffSampledMode_equation line 127

Source documentation

The sampled profile has the actual Fourier mode derivative, including the same sampled residual used in the decaying Duhamel estimate.

theorem hasDerivAt_cutoffSampledMode_equation (a b k L s : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (hL : 0 < L)
    (hRs : 1 ≤ expandingRadius L s) (m : ℕ) (ham : 2 * a * (m : ℝ) = 1)
    (χ : 𝓢(E, ℝ)) (hχ : HasCompactSupport (χ : E → ℝ))
    (hχone : ∀ x : E, ‖x‖ < 1 / 2 → χ x = 1)
    (hχzero : ∀ x : E, 2 < ‖x‖ → χ x = 0)
    (Q : E → ℂ) (hQ : ContDiff ℝ ∞ Q)
    (hstationary : ∀ y, stationarySimilarityDefect a b m Q y = 0) (n : frequencyLattice) :
    let R := expandingRadius L s
…

Mentions: OAI.DefocusingNLS.expandingRadius, OAI.DefocusingNLS.stationarySimilarityDefect, OAI.DefocusingNLS.frequencyLattice