The partial Fourier transform is smooth on the plane, with uniformly bounded derivatives

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

For a Schwartz kernel K on the plane, the partial Fourier transform in the second slot,

𝓕₂K(u, ξ) = ∫ e(−wξ) K(u, w) dw,

is C^∞ as a function of (u, ξ) ∈ ℝ × ℝ, and every iterated derivative is bounded uniformly on the plane by a constant times a single Finset.sup of K's seminorms:

‖∂ⁿ 𝓕₂K(u, ξ)‖ ≤ (Σᵢ C(n, i) (2π)ⁱ 2ⁱ⁺²) · π · 𝒮ₙ(K).

The integrand F p w = e(−w p.2) · K(p.1, w) has parameter p = (u, ξ) in a finite-dimensional space and is jointly smooth in (p, w), which is exactly the shape of #124's ★★★ contDiffOn_integral_of_iteratedFDeriv_bound and ★★★ norm_iteratedFDeriv_integral_le (ContDiffParametricIntegralFDeriv.lean); #126(ii)'s prodDirDeriv lemmas discharge the measurability hypotheses for any jointly smooth integrand. The content of this file is the bound family, a Leibniz expansion across the oscillating factor: ∂ᵏ_p [e(−wξ) K(u, w)] is a sum over i ≤ k of a derivative of the phase of order i — of norm exactly (2π|w|)ⁱ, the phase being exp(c · ξ) with |c| = 2π|w| — times a derivative of u ↦ K(u, w) of order k − i, and K's decay two orders apart turns (1 + |w|)ⁱ ‖∂ᵏ⁻ⁱK(u, w)‖ into 2ⁱ⁺² 𝒮(K) (1 + w²)⁻¹, integrable in w and independent of u.

• SchwartzMap.partialFourier — 𝓕₂K as a plain function on the plane, with partialFourier_eq_sliceFourier: at (u, ξ) it is the slice-wise transform of PartialFourier.lean, so the slice-wise object and this one are the same;
• SchwartzMap.iteratedDeriv_cexp_const_mul_ofReal, ★ norm_iteratedFDeriv_phase_le — the phase's derivatives in the parameter have norm (2π|w|)ⁱ;
• ★ SchwartzMap.one_add_abs_pow_mul_norm_iteratedFDeriv_le — the weight transfer onto the integration variable: (1 + |w|)ⁱ ‖∂ʲK(u, w)‖ ≤ 2ⁱ⁺² 𝒮(K) (1 + w²)⁻¹, uniformly in u;
• ★★ SchwartzMap.norm_iteratedFDeriv_partialFourierIntegrand_le — the Leibniz bound family, ‖∂ᵏ_p F(·, w)(p)‖ ≤ leibnizConst k · kSup K k · (1 + w²)⁻¹;
• ★★ SchwartzMap.contDiff_partialFourier — 𝓕₂K is C^∞ on the plane;
• ★★ SchwartzMap.norm_iteratedFDeriv_partialFourier_le, norm_partialFourier_le — every derivative is bounded uniformly on the plane, linearly in one Finset.sup of K's seminorms.

Honest scope

• No decay in (u, ξ) is proved here: that is #172 (the multiplication identities) and #173 (the joint seminorm bounds). The uniform derivative bound is what #173 combines with them.
• The constants are not sharp; leibnizConst k = Σᵢ C(k, i) (2π)ⁱ 2ⁱ⁺² and kSup K k, the sup of K's seminorms over Iic (k + 2, k), fall out of the route.
• One dimension in each slot, scalar-valued kernels.

References: ContDiffParametricIntegralFDeriv.lean (#124), SchwartzPartialIntegral.lean (#126(ii), the measurability lemmas and the weight transfer this file mirrors), SchwartzTensor.lean (norm_iteratedFDeriv_comp_clm_le), PartialFourier.lean (sliceFourierCLM); Mathlib Analysis/Calculus/ContDiff/Bounds.lean (norm_iteratedFDeriv_mul_le); specs/BACKLOG.md #170, #121.

The partial Fourier transform as a function

noncomputable def SchwartzMap.partialFourier (K : SchwartzMap (ℝ × ℝ) ℂ) (p : ℝ × ℝ) : ℂ

The partial Fourier transform of a Schwartz kernel on the plane, in the second slot: 𝓕₂K(u, ξ) = ∫ e(−wξ) K(u, w) dw.

Equations

• K.partialFourier p = ∫ (w : ℝ), ↑(Real.fourierChar (-(w * p.2))) * K (p.1, w)

theorem SchwartzMap.partialFourier_eq_sliceFourier (K : SchwartzMap (ℝ × ℝ) ℂ) (u ξ : ℝ) : K.partialFourier (u, ξ) = ((sliceFourierCLM u) K) ξ

At (u, ξ) the partial Fourier transform is the slice-wise transform of PartialFourier.lean.

noncomputable def SchwartzMap.partialFourierIntegrand (K : SchwartzMap (ℝ × ℝ) ℂ) (q : (ℝ × ℝ) × ℝ) : ℂ

The integrand, as a jointly smooth function of (p, w).

Equations

• K.partialFourierIntegrand q = ↑(Real.fourierChar (-(q.2 * q.1.2))) * K (q.1.1, q.2)

theorem SchwartzMap.partialFourierIntegrand_apply (K : SchwartzMap (ℝ × ℝ) ℂ) (p : ℝ × ℝ) (w : ℝ) : K.partialFourierIntegrand (p, w) = ↑(Real.fourierChar (-(w * p.2))) * K (p.1, w)

theorem SchwartzMap.partialFourier_eq_integral_integrand (K : SchwartzMap (ℝ × ℝ) ℂ) : K.partialFourier = fun (p : ℝ × ℝ) => ∫ (w : ℝ), K.partialFourierIntegrand (p, w)

theorem SchwartzMap.contDiff_partialFourierIntegrand (K : SchwartzMap (ℝ × ℝ) ℂ) : ContDiff ℝ (↑⊤) K.partialFourierIntegrand

The integrand is jointly smooth.

theorem SchwartzMap.contDiff_partialFourierIntegrand_left (K : SchwartzMap (ℝ × ℝ) ℂ) (w : ℝ) : ContDiff ℝ ↑⊤ fun (p : ℝ × ℝ) => K.partialFourierIntegrand (p, w)

The phase

theorem SchwartzMap.iteratedDeriv_cexp_const_mul_ofReal (n : ℕ) (c : ℂ) : (iteratedDeriv n fun (x : ℝ) => Complex.exp (c * ↑x)) = fun (x : ℝ) => c ^ n * Complex.exp (c * ↑x)

The iterated derivative of x ↦ exp(c x) on the real line.

theorem SchwartzMap.contDiff_cexp_const_mul_ofReal (c : ℂ) : ContDiff ℝ ↑⊤ fun (x : ℝ) => Complex.exp (c * ↑x)

theorem SchwartzMap.phase_eq (w : ℝ) : (fun (p : ℝ × ℝ) => ↑(Real.fourierChar (-(w * p.2)))) = fun (p : ℝ × ℝ) => Complex.exp (↑(-(2 * Real.pi * w)) * Complex.I * ↑((ContinuousLinearMap.snd ℝ ℝ ℝ) p))

The phase in the parameter is exp(c · ξ) with c = −2πw · i, read through the second projection.

theorem SchwartzMap.norm_iteratedFDeriv_phase_le (w : ℝ) (i : ℕ) (p : ℝ × ℝ) : ‖iteratedFDeriv ℝ i (fun (p : ℝ × ℝ) => ↑(Real.fourierChar (-(w * p.2)))) p‖ ≤ (2 * Real.pi * |w|) ^ i

★ The phase's derivatives in the parameter have norm (2π|w|)ⁱ.

The kernel factor

theorem SchwartzMap.norm_iteratedFDeriv_slice_fst_le (K : SchwartzMap (ℝ × ℝ) ℂ) (w : ℝ) (j : ℕ) (p : ℝ × ℝ) : ‖iteratedFDeriv ℝ j (fun (p : ℝ × ℝ) => K (p.1, w)) p‖ ≤ ‖iteratedFDeriv ℝ j ⇑K (p.1, w)‖

A derivative in u of u ↦ K(u, w) is no bigger than the full derivative of K.

theorem SchwartzMap.one_add_abs_pow_mul_norm_iteratedFDeriv_le (K : SchwartzMap (ℝ × ℝ) ℂ) (i j : ℕ) (u w : ℝ) : (1 + |w|) ^ i * ‖iteratedFDeriv ℝ j ⇑K (u, w)‖ ≤ 2 ^ (i + 2) * ((Finset.Iic (i + 2, j)).sup (schwartzSeminormFamily ℂ (ℝ × ℝ) ℂ)) K * (1 + w ^ 2)⁻¹

★ The weight transfer onto the integration variable: two orders of K's decay give (1 + |w|)ⁱ ‖∂ʲK(u, w)‖ ≤ 2ⁱ⁺² 𝒮(K) (1 + w²)⁻¹, uniformly in u. The mirror of #126(ii)'s one_add_norm_pow_mul_norm_iteratedFDeriv_le, with the weight on the other slot.

The bound family

noncomputable def SchwartzMap.kSup (K : SchwartzMap (ℝ × ℝ) ℂ) (k : ℕ) : ℝ

The sup of K's seminorms over the square Iic (k + 2, k), which dominates every Iic (i + 2, k − i) with i ≤ k.

Equations

• K.kSup k = ((Finset.Iic (k + 2, k)).sup (schwartzSeminormFamily ℂ (ℝ × ℝ) ℂ)) K

theorem SchwartzMap.kSup_nonneg (K : SchwartzMap (ℝ × ℝ) ℂ) (k : ℕ) : 0 ≤ K.kSup k

theorem SchwartzMap.sup_le_kSup (K : SchwartzMap (ℝ × ℝ) ℂ) (k i : ℕ) (hi : i ≤ k) : ((Finset.Iic (i + 2, k - i)).sup (schwartzSeminormFamily ℂ (ℝ × ℝ) ℂ)) K ≤ K.kSup k

noncomputable def SchwartzMap.leibnizConst (k : ℕ) : ℝ

The Leibniz constant Σᵢ C(k, i) (2π)ⁱ 2ⁱ⁺².

Equations

• SchwartzMap.leibnizConst k = ∑ i ∈ Finset.range (k + 1), ↑(k.choose i) * (2 * Real.pi) ^ i * 2 ^ (i + 2)

theorem SchwartzMap.leibnizConst_nonneg (k : ℕ) : 0 ≤ leibnizConst k

theorem SchwartzMap.leibnizConst_zero : leibnizConst 0 = 4

theorem SchwartzMap.norm_iteratedFDeriv_partialFourierIntegrand_le (K : SchwartzMap (ℝ × ℝ) ℂ) (k : ℕ) (p : ℝ × ℝ) (w : ℝ) : ‖iteratedFDeriv ℝ k (fun (p : ℝ × ℝ) => K.partialFourierIntegrand (p, w)) p‖ ≤ leibnizConst k * K.kSup k * (1 + w ^ 2)⁻¹

★★ The Leibniz bound family: every p-derivative of the integrand is bounded, uniformly in p, by leibnizConst k · kSup K k · (1 + w²)⁻¹, which is integrable in w.

Smoothness and the uniform derivative bound

theorem SchwartzMap.norm_dirDeriv_partialFourierIntegrand_le (K : SchwartzMap (ℝ × ℝ) ℂ) (hs : List (ℝ × ℝ)) (p : ℝ × ℝ) (w : ℝ) : ‖dirDeriv (fun (p : ℝ × ℝ) (w : ℝ) => K.partialFourierIntegrand (p, w)) hs p w‖ ≤ dirWeight hs * (leibnizConst hs.length * K.kSup hs.length * (1 + w ^ 2)⁻¹)

The bound family in the form #124's theorems take it.

theorem SchwartzMap.contDiff_partialFourier (K : SchwartzMap (ℝ × ℝ) ℂ) : ContDiff ℝ (↑⊤) K.partialFourier

★★ The partial Fourier transform is C^∞ on the plane.

theorem SchwartzMap.norm_iteratedFDeriv_partialFourier_le (K : SchwartzMap (ℝ × ℝ) ℂ) (n : ℕ) (p : ℝ × ℝ) : ‖iteratedFDeriv ℝ n K.partialFourier p‖ ≤ leibnizConst n * K.kSup n * Real.pi

★★ Every derivative of the partial Fourier transform is bounded uniformly on the plane, linearly in one Finset.sup of K's seminorms: ‖∂ⁿ 𝓕₂K(p)‖ ≤ leibnizConst n · kSup K n · π.

theorem SchwartzMap.norm_partialFourier_le (K : SchwartzMap (ℝ × ℝ) ℂ) (p : ℝ × ℝ) : ‖K.partialFourier p‖ ≤ 4 * Real.pi * K.kSup 0

The zero-order case: ‖𝓕₂K(p)‖ ≤ 4π · kSup K 0.