SchwartzNonlinearPeriodization.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Odd-power nonlinearity commutes with the cutoff periodization

The support radius is at most twice the scale, whereas distinct lattice translates are separated by at least 2π times the scale.

theorem OAI.DefocusingNLS.oddPowerNonlinearity_tsum_disjoint line 18
theorem OAI.DefocusingNLS.cutoff_periodization_disjoint line 32
theorem OAI.DefocusingNLS.oddPowerNonlinearity_periodization line 59

theorem OAI.DefocusingNLS.sampled_oddPower_periodization line 68

Source documentation

The actual torus polynomial is the periodization of the physical polynomial.

theorem sampled_oddPower_periodization (a k L : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (hL : 1 ≤ L)
    (m : ℕ) (ψ : 𝓢(E, ℂ)) (hψ : ∀ x : E, 2 * L < ‖x‖ → ψ x = 0) (y : E) :
    expandingTorusFunction a k L
      (expandingOddPower a k L ha ha1 hk hL m
        (schwartzTorusSample a k L ha1 hk hL (radianFourierKernel ψ)))
      (euclideanToTorus (L⁻¹ • y)) =
      ∑' n : frequencyLattice,
        oddPowerNonlinearity m (ψ (y + (2 * Real.pi * L) • (n : E))) := by
…

Mentions: OAI.DefocusingNLS.expandingTorusFunction, OAI.DefocusingNLS.expandingOddPower, OAI.DefocusingNLS.schwartzTorusSample, OAI.DefocusingNLS.radianFourierKernel, OAI.DefocusingNLS.euclideanToTorus, OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.oddPowerNonlinearity