PlanarSliceFourier.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Fourier support of affine-line restrictions

Fubini and the area-preserving shear identify the transverse Fourier transform of a slice coefficient with the planar transform on the fiber ξ+sη=ω. One-dimensional Fourier inversion then proves exact vanishing when this fiber misses the planar spectrum. No tensor representation is used.

theorem OAI.LipschitzHilbert.planar_phase_integrable line 21
theorem OAI.LipschitzHilbert.planarSliceFourier_fourier line 32
theorem OAI.LipschitzHilbert.planarSchwartzSlice_fourier_eq_zero line 68
Source documentation
A frequency fiber missing the planar spectrum gives exact vanishing of every affine slice Fourier coefficient at that frequency.
```
theorem planarSchwartzSlice_fourier_eq_zero (f : SchwartzMap (ℝ × ℝ) ℂ)
    (b s ω : ℝ) (hfiber : ∀ η, planarFourier f (ω - s * η, η) = 0) :
    𝓕 (planarSchwartzSlice f b s) ω = 0 := by
…
```
Mentions: OAI.LipschitzHilbert.planarFourier, OAI.LipschitzHilbert.planarSchwartzSlice