PlanarSliceFourierSupport.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Spectral rectangles and annular bounds for actual planar Schwartz restrictions, using the proved fiber-vanishing identity. Frequencies use the exp(-2πi xξ) convention throughout.

theorem OAI.LipschitzHilbert.frequency_rectangle_bound line 15

theorem OAI.LipschitzHilbert.planarSchwartzSlice_fourier_carrier_bound line 26

Source documentation

The packet spectral rectangle projects to the expected carrier interval on every affine reference line.

theorem planarSchwartzSlice_fourier_carrier_bound
    (f : SchwartzMap (ℝ × ℝ) ℂ) (b s θ η₀ δ ε : ℝ)
    (hspectrum : ∀ ξ η, planarFourier f (ξ, η) ≠ 0 →
      |ξ + θ * η| ≤ δ ∧ |η - η₀| ≤ ε)
    {ω : ℝ} (hω : 𝓕 (planarSchwartzSlice f b s) ω ≠ 0) :
    |ω - η₀ * (s - θ)| ≤ δ + ε * |s - θ| := by
…

Mentions: OAI.LipschitzHilbert.planarFourier, OAI.LipschitzHilbert.planarSchwartzSlice

theorem OAI.LipschitzHilbert.planarSchwartzSlice_support_carrier_interval line 43
theorem OAI.LipschitzHilbert.planarSchwartzSlice_tsupport_carrier_interval line 55

theorem OAI.LipschitzHilbert.planarSchwartzSlice_fourier_annulus line 67

Source documentation

Separating the carrier from zero turns the carrier interval into an annulus; the constants are retained exactly for subsequent rescaling.

theorem planarSchwartzSlice_fourier_annulus
    (f : SchwartzMap (ℝ × ℝ) ℂ) (b s θ η₀ δ ε : ℝ)
    (hspectrum : ∀ ξ η, planarFourier f (ξ, η) ≠ 0 →
      |ξ + θ * η| ≤ δ ∧ |η - η₀| ≤ ε)
    {a A : ℝ} (hlower : a ≤ |η₀ * (s - θ)| - (δ + ε * |s - θ|))
    (hupper : |η₀ * (s - θ)| + (δ + ε * |s - θ|) ≤ A)
    {ω : ℝ} (hω : 𝓕 (planarSchwartzSlice f b s) ω ≠ 0) :
    a ≤ |ω| ∧ |ω| ≤ A := by
…

Mentions: OAI.LipschitzHilbert.planarFourier, OAI.LipschitzHilbert.planarSchwartzSlice