PlanarSliceFourierDerivative.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Vertical differentiation of a general planar Schwartz function has the Fourier multiplier 2π i η. Consequently every scaled covariant vertical jet used in the packet construction preserves spectral zeros. The proof uses one-dimensional differentiation and product Fubini, so it does not impose a tensor decomposition on the planar packet.

def OAI.LipschitzHilbert.verticalSchwartzSlice line 19
theorem OAI.LipschitzHilbert.verticalSchwartzSlice_apply line 24
theorem OAI.LipschitzHilbert.verticalSchwartzSlice_deriv line 29
theorem OAI.LipschitzHilbert.verticalSchwartzSlice_fourier_deriv line 41
theorem OAI.LipschitzHilbert.planarFourier_integrand_integrable line 53
theorem OAI.LipschitzHilbert.planarFourier_eq_vertical_integral line 65
theorem OAI.LipschitzHilbert.planarFourier_verticalDerivative line 89
Source documentation
The exact vertical-derivative multiplier for the product-Lebesgue Fourier transform, with mathlib's 2π convention.
```
theorem planarFourier_verticalDerivative (f : SchwartzMap (ℝ × ℝ) ℂ)
    (ξ η : ℝ) :
    planarFourier (planarVerticalDerivative f) (ξ, η) =
      (2 * Real.pi * Complex.I * η) * planarFourier f (ξ, η) := by
…
```
Mentions: OAI.LipschitzHilbert.planarFourier, OAI.LipschitzHilbert.planarVerticalDerivative
theorem OAI.LipschitzHilbert.planarFourier_smul line 101
theorem OAI.LipschitzHilbert.planarFourier_sub line 112
theorem OAI.LipschitzHilbert.planarFourier_covariantDerivative line 121
theorem OAI.LipschitzHilbert.planarFourier_covariantJet_eq_zero line 132
Source documentation
All three scaled covariant jets retain every spectral zero of the original general planar Schwartz packet.
```
theorem planarFourier_covariantJet_eq_zero (f : SchwartzMap (ℝ × ℝ) ℂ)
    (frequency scale : ℝ) (i : Fin 3) (ξ η : ℝ)
    (hzero : planarFourier f (ξ, η) = 0) :
    planarFourier (planarCovariantJet f frequency scale i) (ξ, η) = 0 := by
…
```
Mentions: OAI.LipschitzHilbert.planarFourier, OAI.LipschitzHilbert.planarCovariantJet
theorem OAI.LipschitzHilbert.planarAngularFourier_verticalDerivative line 147
theorem OAI.LipschitzHilbert.planarAngularFourier_covariantDerivative line 157
theorem OAI.LipschitzHilbert.planarAngularFourier_covariantJet_eq_zero line 167