RadialNonstationary.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Arbitrary-power decay for radial discarded terms

After rescaling the radial shell variable, a discarded longitudinal edge has a Fourier frequency bounded below by a positive power of R. The fixed radial cutoff is Schwartz. Its library Fourier seminorm estimates therefore supply the arbitrary-power error required by graph:localization. The Fourier convention includes 2π; a fixed conversion of frequency is absorbed into the displayed constant.

theorem OAI.Falconer.schwartz_fourier_decay line 20

theorem OAI.Falconer.radial_nonstationary_arbitrary_power line 40

Source documentation

A fixed positive gain in rescaled phase frequency gives every requested power of decay by choosing a finite Schwartz seminorm order.

theorem radial_nonstationary_arbitrary_power (Ψ : 𝓢(ℝ, ℂ))
    {a : ℝ} (ha : 0 < a) (T : ℝ) :
    ∃ C : ℝ, 0 < C ∧ ∀ R : ℝ, 1 ≤ R → ∀ ξ : ℝ, R^a ≤ |ξ| →
      ‖(𝓕 Ψ) ξ‖ ≤ C * R^(-T) := by
…