The symbol of a Schwartz kernel, at each midpoint

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate). BACKLOG #121(ii), partially — see the scope note, which is the point of this file.

#121(ii) asked for the partial Fourier transform on 𝓢(ℝ × ℝ, ℂ): the transform in the second slot alone, landing in Schwartz functions on the plane. That is what turns a kernel into a symbol and what #92(c) recorded as the reason W could not be shown Schwartz on the plane.

What is delivered here is the slice-wise transform, which is the object weylSymbol actually is:

• SchwartzMap.sliceFourierCLM — the composite of #121(i)'s sliceCLM with Mathlib's fourierTransformCLM, so the symbol at a fixed midpoint is a Schwartz function of the frequency, continuously and linearly in the kernel;
• ★ WignerFunction.weylSymbol_slice_apply — it is weylSymbol of the kernel's slice family;
• ★ WignerFunction.integrable_weylSymbol_slice and ★ WignerFunction.exists_bound_weylSymbol_slice — the two consequences a consumer wants, both free once the symbol slice is Schwartz.

Honest scope — and a dependency the row did not know about

⚠️ This does not close #121(ii) by itself, and the joint statement is not a corollary of it. The joint statement is now proved (2026-10-21, #170–#174): ★★★ SchwartzMap.partialFourierCLM in PartialFourierCLM.lean is the transform as a continuous linear map 𝓢(ℝ × ℝ, ℂ) →L[ℂ] 𝓢(ℝ × ℝ, ℂ), with slice_partialFourierCLM identifying its slices with this file's sliceFourierCLM. The paragraphs below record why that was not a corollary, as they stood when this file was written. That (u, ξ) ↦ weylSymbol (slice K) u ξ is Schwartz on the plane needs decay and smoothness jointly, and slice-wise Schwartzness gives neither: every constant here may depend on the midpoint u.

⚠️ The reason is structural, and it is new information. The natural proof of the joint statement factors through the curry 𝓢(E × F, G) ≃ 𝓢(E, 𝓢(F, G)), after which a partial transform is just Mathlib's fourierTransformCLM applied in the inner factor. Mathlib has no such curry, and its first half is #123. The alternative is bespoke: differentiate under the integral in both variables to all orders, which needs the finite-dimensional-parameter version of #120 (that row's own scope note records the one-dimensional restriction), and then the seminorm estimates (2πiξ)^c 𝓕₂K = 𝓕₂[∂_w^c K] and ∂_ξ^b 𝓕₂K = 𝓕₂[(−2πiw)^b K] assembled against K's decay. Either way it is not a one-sitting build, which the row's L did not reflect.

References: SchwartzSlice.lean (#121(i)), WignerWeyl.lean (weylSymbol), Mathlib/Analysis/Distribution/SchwartzSpace/Fourier.lean; specs/BACKLOG.md #121, #123, #120, #92.

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

The slice-wise Fourier transform: slice the kernel at a midpoint, then transform. A continuous linear map in the kernel, being a composite of two.

Equations

• SchwartzMap.sliceFourierCLM u = SchwartzMap.fourierTransformCLM ℂ ∘SL SchwartzMap.sliceCLM ℂ u

@[simp]

theorem SchwartzMap.sliceFourierCLM_apply (u : ℝ) (K : SchwartzMap (ℝ × ℝ) ℂ) : ⇑((sliceFourierCLM u) K) = ⇑(FourierTransform.fourier (K.slice u))

theorem WignerFunction.weylSymbol_slice_apply (K : SchwartzMap (ℝ × ℝ) ℂ) (u ξ : ℝ) : weylSymbol K.slice u ξ = ((SchwartzMap.sliceFourierCLM u) K) ξ

★ The symbol at a midpoint is a Schwartz function of the frequency. The left side is the corpus's weylSymbol; the right is a term of 𝓢(ℝ, ℂ).

theorem WignerFunction.integrable_weylSymbol_slice (K : SchwartzMap (ℝ × ℝ) ℂ) (u : ℝ) : MeasureTheory.Integrable (weylSymbol K.slice u) MeasureTheory.volume

★ The symbol slice is integrable, which is what the Weyl expectation formula's inner integral needs.

theorem WignerFunction.exists_bound_weylSymbol_slice (K : SchwartzMap (ℝ × ℝ) ℂ) (u : ℝ) : ∃ (C : ℝ), ∀ (ξ : ℝ), ‖weylSymbol K.slice u ξ‖ ≤ C

★ And bounded, uniformly in the frequency.