Polynomial weights on the partial Fourier transform are partial Fourier transforms

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #172 (out of #121(ii), brick 3 of 5: the partial Fourier transform on 𝓢(ℝ × ℝ, ℂ)).

For a Schwartz kernel K on the plane,

u · 𝓕₂K(u, ξ) = 𝓕₂(u · K)(u, ξ), 2πi ξ · 𝓕₂K(u, ξ) = 𝓕₂(∂_w K)(u, ξ),

so every polynomial weight on 𝓕₂K is 𝓕₂ of a continuous linear image of K: ‖(u, ξ)‖ᵏ ‖𝓕₂K(u, ξ)‖ ≤ ‖𝓕₂(uᵏ K)(u, ξ)‖ + (2π)⁻ᵏ ‖𝓕₂(∂_wᵏ K)(u, ξ)‖. With #171 (derivatives are 𝓕₂'s) and #170 (𝓕₂ of a Schwartz function is bounded by one of its seminorms), this is what makes 𝓕₂K decay on the plane, which is #173.

The ξ identity is slice-wise and Mathlib's: 𝓕₂K(u, ·) = 𝓕 (slice K u) (PartialFourier.lean) and SchwartzMap.fourier_lineDerivOp_eq is 𝓕(∂f) = 2πi ξ · 𝓕f on 𝓢(ℝ, ℂ); what needs saying is that the w-derivative of a slice is the slice of the w-derivative (slice_derivW, the chain rule through w ↦ (u, w)). The u identity is that u is a parameter of the integral.

• SchwartzMap.uMul, mulU, mulU_apply — multiplication by u, a continuous linear map of Schwartz space; derivW, derivW_apply — the w-derivative;
• SchwartzMap.slice_derivW — the slice of ∂_w K is the derivative of the slice;
• ★ SchwartzMap.partialFourier_mulU — 𝓕₂(u K) = u · 𝓕₂K;
• ★★ SchwartzMap.partialFourier_derivW — 𝓕₂(∂_w K) = 2πi ξ · 𝓕₂K;
• SchwartzMap.mulUPow, derivWPow, partialFourier_mulUPow, partialFourier_derivWPow — the iterates, 𝓕₂(uᵏ K) = uᵏ 𝓕₂K and 𝓕₂(∂_wᵏ K) = (2πi ξ)ᵏ 𝓕₂K;
• ★★ SchwartzMap.norm_pow_mul_norm_partialFourier_le — the weight moves inside: ‖p‖ᵏ ‖𝓕₂K(p)‖ ≤ ‖𝓕₂(mulUPow k K)(p)‖ + (2π)⁻ᵏ ‖𝓕₂(derivWPow k K)(p)‖ for every p.

Honest scope

• Identities and one inequality, no estimate on K's seminorms: the seminorm bound on mulUPow k K and derivWPow k K, and its combination with #171's derivative operators, is #173.
• The iterates are written as explicit recursions mulUPow, derivWPow rather than powers in the endomorphism monoid of 𝓢(ℝ × ℝ, ℂ), so that their _apply lemmas are rfl.

References: PartialFourierSmooth.lean (#170, partialFourier_eq_sliceFourier), PartialFourierDeriv.lean (#171), PartialFourier.lean (sliceFourierCLM), SchwartzSlice.lean (#121(i), slice); Mathlib Analysis/Distribution/SchwartzSpace/Fourier.lean (fourier_lineDerivOp_eq); specs/BACKLOG.md #172, #121.

The two operators

noncomputable def SchwartzMap.uMul (q : ℝ × ℝ) : ℂ

The multiplier (u, w) ↦ u.

Equations

• SchwartzMap.uMul q = ↑q.1

theorem SchwartzMap.uMul_eq_clm : uMul = ⇑(Complex.ofRealCLM ∘SL ContinuousLinearMap.fst ℝ ℝ ℝ)

theorem SchwartzMap.hasTemperateGrowth_uMul : Function.HasTemperateGrowth uMul

noncomputable def SchwartzMap.mulU : SchwartzMap (ℝ × ℝ) ℂ →L[ℂ] SchwartzMap (ℝ × ℝ) ℂ

Multiplication by u on Schwartz kernels.

Equations

• SchwartzMap.mulU = SchwartzMap.smulLeftCLM ℂ SchwartzMap.uMul

theorem SchwartzMap.mulU_apply (K : SchwartzMap (ℝ × ℝ) ℂ) (q : ℝ × ℝ) : (mulU K) q = ↑q.1 * K q

noncomputable def SchwartzMap.derivW : SchwartzMap (ℝ × ℝ) ℂ →L[ℂ] SchwartzMap (ℝ × ℝ) ℂ

The w-derivative on Schwartz kernels.

Equations

• SchwartzMap.derivW = LineDeriv.lineDerivOpCLM ℂ (SchwartzMap (ℝ × ℝ) ℂ) (0, 1)

theorem SchwartzMap.derivW_apply (K : SchwartzMap (ℝ × ℝ) ℂ) (q : ℝ × ℝ) : (derivW K) q = (fderiv ℝ (⇑K) q) (0, 1)

The u identity

theorem SchwartzMap.partialFourier_mulU (K : SchwartzMap (ℝ × ℝ) ℂ) (u ξ : ℝ) : (mulU K).partialFourier (u, ξ) = ↑u * K.partialFourier (u, ξ)

★ 𝓕₂(u K) = u · 𝓕₂K: u is a parameter of the integral.

The ξ identity

theorem SchwartzMap.slice_derivW (K : SchwartzMap (ℝ × ℝ) ℂ) (u : ℝ) : (derivW K).slice u = LineDeriv.lineDerivOp 1 (K.slice u)

The slice of the w-derivative is the derivative of the slice.

theorem SchwartzMap.partialFourier_derivW (K : SchwartzMap (ℝ × ℝ) ℂ) (u ξ : ℝ) : (derivW K).partialFourier (u, ξ) = 2 * ↑Real.pi * Complex.I * (↑ξ * K.partialFourier (u, ξ))

★★ 𝓕₂(∂_w K) = 2πi ξ · 𝓕₂K: Mathlib's Fourier–derivative rule on the slice.

The iterates

noncomputable def SchwartzMap.mulUPow : ℕ → SchwartzMap (ℝ × ℝ) ℂ →L[ℂ] SchwartzMap (ℝ × ℝ) ℂ

uᵏ ·, as an explicit recursion.

Equations

• SchwartzMap.mulUPow 0 = ContinuousLinearMap.id ℂ (SchwartzMap (ℝ × ℝ) ℂ)
• SchwartzMap.mulUPow k.succ = SchwartzMap.mulU ∘SL SchwartzMap.mulUPow k

noncomputable def SchwartzMap.derivWPow : ℕ → SchwartzMap (ℝ × ℝ) ℂ →L[ℂ] SchwartzMap (ℝ × ℝ) ℂ

∂_wᵏ, as an explicit recursion.

Equations

• SchwartzMap.derivWPow 0 = ContinuousLinearMap.id ℂ (SchwartzMap (ℝ × ℝ) ℂ)
• SchwartzMap.derivWPow k.succ = SchwartzMap.derivW ∘SL SchwartzMap.derivWPow k

@[simp]

theorem SchwartzMap.mulUPow_zero (K : SchwartzMap (ℝ × ℝ) ℂ) : (mulUPow 0) K = K

theorem SchwartzMap.mulUPow_succ (k : ℕ) (K : SchwartzMap (ℝ × ℝ) ℂ) : (mulUPow (k + 1)) K = mulU ((mulUPow k) K)

@[simp]

theorem SchwartzMap.derivWPow_zero (K : SchwartzMap (ℝ × ℝ) ℂ) : (derivWPow 0) K = K

theorem SchwartzMap.derivWPow_succ (k : ℕ) (K : SchwartzMap (ℝ × ℝ) ℂ) : (derivWPow (k + 1)) K = derivW ((derivWPow k) K)

theorem SchwartzMap.partialFourier_mulUPow (k : ℕ) (K : SchwartzMap (ℝ × ℝ) ℂ) (u ξ : ℝ) : ((mulUPow k) K).partialFourier (u, ξ) = ↑u ^ k * K.partialFourier (u, ξ)

𝓕₂(uᵏ K) = uᵏ · 𝓕₂K.

theorem SchwartzMap.partialFourier_derivWPow (k : ℕ) (K : SchwartzMap (ℝ × ℝ) ℂ) (u ξ : ℝ) : ((derivWPow k) K).partialFourier (u, ξ) = (2 * ↑Real.pi * Complex.I * ↑ξ) ^ k * K.partialFourier (u, ξ)

𝓕₂(∂_wᵏ K) = (2πi ξ)ᵏ · 𝓕₂K.

The weight moves inside

theorem SchwartzMap.norm_two_pi_I : ‖2 * ↑Real.pi * Complex.I‖ = 2 * Real.pi

theorem SchwartzMap.max_pow_le_add_pow {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (k : ℕ) : max a b ^ k ≤ a ^ k + b ^ k

max(a, b)ᵏ ≤ aᵏ + bᵏ for nonnegative a, b.

theorem SchwartzMap.norm_pow_mul_norm_partialFourier_le (K : SchwartzMap (ℝ × ℝ) ℂ) (k : ℕ) (p : ℝ × ℝ) : ‖p‖ ^ k * ‖K.partialFourier p‖ ≤ ‖((mulUPow k) K).partialFourier p‖ + (2 * Real.pi)⁻¹ ^ k * ‖((derivWPow k) K).partialFourier p‖

★★ The weight moves inside: a polynomial weight on 𝓕₂K is bounded by 𝓕₂ of two continuous linear images of K, with no p left outside.