The joint Schwartz seminorm bounds of the partial Fourier transform

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

For every k, n there are a finite set s of seminorm indices and a constant C with

‖p‖ᵏ · ‖∂ⁿ 𝓕₂K(p)‖ ≤ C · (s.sup 𝓠) K for every kernel K and every p ∈ ℝ × ℝ,

which is the hypothesis SchwartzMap.mkCLM consumes (#174). The three previous bricks reduce it to one fact about continuous linear maps of Schwartz space:

• #171: ∂ⁿ 𝓕₂K(p)(v) = 𝓕₂(dopFin n v K)(p), so a derivative of 𝓕₂K is 𝓕₂ of a Schwartz function G;
• #172: ‖p‖ᵏ ‖𝓕₂G(p)‖ ≤ ‖𝓕₂(uᵏ G)(p)‖ + (2π)⁻ᵏ ‖𝓕₂(∂_wᵏ G)(p)‖, the weight moved onto G;
• #170: ‖𝓕₂H(p)‖ ≤ 4π · 𝒮(H) for one Schwartz seminorm 𝒮.

The one fact: a continuous linear map T of 𝓢(ℝ × ℝ, ℂ) to itself satisfies, for every finite sup of seminorms s.sup 𝓠, a bound (s.sup 𝓠)(T K) ≤ C · (s'.sup 𝓠) K — Mathlib's Seminorm.bound_of_continuous for the continuous seminorm (s.sup 𝓠) ∘ T on a space whose topology is given by the family 𝓠 (schwartz_withSeminorms). Applied to uᵏ ·, ∂_wᵏ and the two operators Dop is built from, with Dop h linear in h so that ∏ ‖vᵢ‖ factors out of dopFin n v, this is the whole proof.

• ★★ SchwartzMap.exists_seminorm_bound_clm — the one fact, for any continuous linear endomorphism of 𝓢(ℝ × ℝ, ℂ);
• ★ SchwartzMap.exists_seminorm_bound_Dop — (s.sup 𝓠)(Dop h K) ≤ C ‖h‖ (s'.sup 𝓠) K;
• ★★ SchwartzMap.exists_seminorm_bound_dopFin — (s.sup 𝓠)(dopFin n v K) ≤ C (∏ ‖vᵢ‖) (s'.sup 𝓠) K;
• ★★★ SchwartzMap.exists_bound_partialFourier — the joint seminorm bounds.

Honest scope

• The constants are existential: Seminorm.bound_of_continuous produces them from continuity, so nothing here names a C in terms of k, n and the Leibniz constant of #170 (which it could, at the cost of exporting the bounds mkCLM was built from). mkCLM asks for existence.
• Nothing is yet a SchwartzMap; the packaging and the weylSymbol identification are #174.

References: PartialFourierSmooth.lean (#170), PartialFourierDeriv.lean (#171), PartialFourierMul.lean (#172); Mathlib Analysis/LocallyConvex/WithSeminorms.lean (Seminorm.bound_of_continuous), Analysis/Distribution/SchwartzSpace/Basic.lean (schwartz_withSeminorms); specs/BACKLOG.md #173, #121.

The one fact: continuous linear maps of Schwartz space are seminorm-bounded

theorem SchwartzMap.continuous_finset_sup_schwartzSeminorm (s : Finset (ℕ × ℕ)) : Continuous ⇑(s.sup (schwartzSeminormFamily ℂ (ℝ × ℝ) ℂ))

A finite sup of the Schwartz seminorms is continuous (its balls are basis sets).

theorem SchwartzMap.exists_seminorm_bound_clm (T : SchwartzMap (ℝ × ℝ) ℂ →L[ℂ] SchwartzMap (ℝ × ℝ) ℂ) (s : Finset (ℕ × ℕ)) : ∃ (s' : Finset (ℕ × ℕ)) (C : ℝ), 0 ≤ C ∧ ∀ (K : SchwartzMap (ℝ × ℝ) ℂ), (s.sup (schwartzSeminormFamily ℂ (ℝ × ℝ) ℂ)) (T K) ≤ C * (s'.sup (schwartzSeminormFamily ℂ (ℝ × ℝ) ℂ)) K

★★ A continuous linear map of Schwartz space is bounded, seminorm by seminorm: for every finite sup of seminorms there are a finite sup and a constant controlling its composite with T.

The first-order operator, with the direction factored out

theorem SchwartzMap.exists_seminorm_bound_Dop (s : Finset (ℕ × ℕ)) : ∃ (s' : Finset (ℕ × ℕ)) (C : ℝ), 0 ≤ C ∧ ∀ (h : ℝ × ℝ) (K : SchwartzMap (ℝ × ℝ) ℂ), (s.sup (schwartzSeminormFamily ℂ (ℝ × ℝ) ℂ)) ((Dop h) K) ≤ C * ‖h‖ * (s'.sup (schwartzSeminormFamily ℂ (ℝ × ℝ) ℂ)) K

★ (s.sup 𝓠)(Dop h K) ≤ C · ‖h‖ · (s'.sup 𝓠) K: Dop h is linear in h.

theorem SchwartzMap.exists_seminorm_bound_dopFin (n : ℕ) (s : Finset (ℕ × ℕ)) : ∃ (s' : Finset (ℕ × ℕ)) (C : ℝ), 0 ≤ C ∧ ∀ (v : Fin n → ℝ × ℝ) (K : SchwartzMap (ℝ × ℝ) ℂ), (s.sup (schwartzSeminormFamily ℂ (ℝ × ℝ) ℂ)) ((dopFin n v) K) ≤ (C * ∏ i : Fin n, ‖v i‖) * (s'.sup (schwartzSeminormFamily ℂ (ℝ × ℝ) ℂ)) K

★★ (s.sup 𝓠)(dopFin n v K) ≤ C · (∏ ‖vᵢ‖) · (s'.sup 𝓠) K.

The joint seminorm bounds

theorem SchwartzMap.exists_bound_partialFourier (k n : ℕ) : ∃ (s : Finset (ℕ × ℕ)) (C : ℝ), 0 ≤ C ∧ ∀ (K : SchwartzMap (ℝ × ℝ) ℂ) (p : ℝ × ℝ), ‖p‖ ^ k * ‖iteratedFDeriv ℝ n K.partialFourier p‖ ≤ C * (s.sup (schwartzSeminormFamily ℂ (ℝ × ℝ) ℂ)) K

★★★ The joint Schwartz seminorm bounds of the partial Fourier transform: for every k, n there are a finite set of seminorm indices and a constant with ‖p‖ᵏ · ‖∂ⁿ 𝓕₂K(p)‖ ≤ C · (s.sup 𝓠) K for all K and p — the hypothesis SchwartzMap.mkCLM consumes.