The partial Fourier transform on 𝓢(ℝ × ℝ, ℂ), and the Wigner function on the plane

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #174 (out of #121(ii), brick 5 of 5 — closes #121).

The partial Fourier transform in the second slot is a continuous linear map of Schwartz space on the plane to itself, ★★★ partialFourierCLM : 𝓢(ℝ × ℝ, ℂ) →L[ℂ] 𝓢(ℝ × ℝ, ℂ), by SchwartzMap.mkCLM with #170 (smoothness), #171 (linearity in the kernel) and #173 (the joint seminorm bounds). Its value at (u, ξ) is the corpus's weylSymbol of the sliced kernel (★★ partialFourierCLM_apply_eq_weylSymbol): the symbol of a Schwartz kernel is a Schwartz function on the plane, which is what #92(c) recorded as the missing step.

The payoff. The Wigner kernel (x, y) ↦ ψ(x + y/2) · conj ψ(x − y/2) is a Schwartz function on the plane — the tensor product ψ ⊗ conj ψ of #126(i) composed with the linear automorphism (x, y) ↦ (x + y/2, x − y/2) — and W_ψ = 𝓕₂ of it, so ★★★ wignerSchwartz ψ : 𝓢(ℝ × ℝ, ℂ) with wignerSchwartz_apply : wignerSchwartz ψ (x, ξ) = wigner ψ x ξ: the Wigner function of a Schwartz state is a Schwartz function of (x, ξ), resolving the caveat in WignerCalculus.lean.

• ★★★ SchwartzMap.partialFourierCLM, partialFourierCLM_apply, slice_partialFourierCLM — the transform as a CLM; its slices are the slice-wise transforms of PartialFourier.lean;
• ★★ SchwartzMap.partialFourierCLM_apply_eq_weylSymbol — it is weylSymbol of the slice family;
• SchwartzMap.conjS, wignerL, norm_le_wignerL, ★ wignerKernelS, wignerKernelS_apply — the Wigner kernel as a Schwartz function on the plane;
• ★★★ SchwartzMap.wignerSchwartz, wignerSchwartz_apply — the Wigner function on the plane.

Honest scope

• One dimension in each slot, scalar kernels; the transform is in the second slot only (the first slot is the parameter), which is the one a symbol calculus uses.
• wignerSchwartz is the Wigner function of one Schwartz state; the cross Wigner function wigner₂ of MoyalBracket.lean is the same construction with φ ⊗ conj ψ and is not packaged here.
• Nothing about the Moyal product of symbols, adjoints, or a wider symbol class: partialFourierCLM is the tool those would be stated with, not any of them.

References: PartialFourierSmooth.lean (#170), PartialFourierDeriv.lean (#171), PartialFourierMul.lean (#172), PartialFourierBound.lean (#173), PartialFourier.lean (sliceFourierCLM, weylSymbol_slice_apply), SchwartzTensor.lean (#126(i), tensorProd), Wigner.lean (wigner), WignerCalculus.lean (#92(c)); specs/BACKLOG.md #174, #121, #92.

The partial Fourier transform as a continuous linear map

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

★★★ The partial Fourier transform on Schwartz space of the plane, 𝓕₂ : 𝓢(ℝ × ℝ, ℂ) →L[ℂ] 𝓢(ℝ × ℝ, ℂ), 𝓕₂K(u, ξ) = ∫ e(−wξ) K(u, w) dw.

Equations

• SchwartzMap.partialFourierCLM = SchwartzMap.mkCLM (fun (K : SchwartzMap (ℝ × ℝ) ℂ) (p : ℝ × ℝ) => K.partialFourier p) ⋯ ⋯ ⋯ SchwartzMap.partialFourierCLM._proof_6

@[simp]

theorem SchwartzMap.partialFourierCLM_apply (K : SchwartzMap (ℝ × ℝ) ℂ) (p : ℝ × ℝ) : (partialFourierCLM K) p = K.partialFourier p

theorem SchwartzMap.slice_partialFourierCLM (K : SchwartzMap (ℝ × ℝ) ℂ) (u : ℝ) : (partialFourierCLM K).slice u = (sliceFourierCLM u) K

The slices of 𝓕₂K are the slice-wise transforms of PartialFourier.lean.

theorem SchwartzMap.partialFourierCLM_apply_eq_weylSymbol (K : SchwartzMap (ℝ × ℝ) ℂ) (u ξ : ℝ) : (partialFourierCLM K) (u, ξ) = WignerFunction.weylSymbol K.slice u ξ

★★ The symbol of a Schwartz kernel is a Schwartz function on the plane: 𝓕₂K is the corpus's weylSymbol of the slice family of K.

The Wigner kernel as a Schwartz function on the plane

noncomputable def SchwartzMap.conjS (ψ : SchwartzMap ℝ ℂ) : SchwartzMap ℝ ℂ

The complex conjugate of a Schwartz function, as a Schwartz function.

Equations

• ψ.conjS = (SchwartzMap.bilinLeftCLM (ContinuousLinearMap.mul ℝ ℂ ∘SL ↑Complex.conjCLE) SchwartzMap.conjS._proof_1) ψ

@[simp]

theorem SchwartzMap.conjS_apply (ψ : SchwartzMap ℝ ℂ) (x : ℝ) : ψ.conjS x = (starRingEnd ℂ) (ψ x)

noncomputable def SchwartzMap.wignerL : ℝ × ℝ →L[ℝ] ℝ × ℝ

The linear automorphism (x, y) ↦ (x + y/2, x − y/2) of the plane.

Equations

• SchwartzMap.wignerL = (ContinuousLinearMap.fst ℝ ℝ ℝ + 2⁻¹ • ContinuousLinearMap.snd ℝ ℝ ℝ).prod (ContinuousLinearMap.fst ℝ ℝ ℝ - 2⁻¹ • ContinuousLinearMap.snd ℝ ℝ ℝ)

theorem SchwartzMap.wignerL_apply (q : ℝ × ℝ) : wignerL q = (q.1 + q.2 / 2, q.1 - q.2 / 2)

theorem SchwartzMap.norm_le_wignerL (q : ℝ × ℝ) : ‖q‖ ≤ 2 * (1 + ‖wignerL q‖) ^ 1

wignerL does not shrink the norm by more than a factor 2, which is what compCLM needs.

noncomputable def SchwartzMap.wignerKernelS (ψ : SchwartzMap ℝ ℂ) : SchwartzMap (ℝ × ℝ) ℂ

★ The Wigner kernel is a Schwartz function on the plane: ψ ⊗ conj ψ composed with wignerL.

Equations

• ψ.wignerKernelS = (SchwartzMap.compCLM ℂ SchwartzMap.wignerKernelS._proof_2 SchwartzMap.wignerKernelS._proof_3) (ψ.tensorProd ψ.conjS)

theorem SchwartzMap.wignerKernelS_apply (ψ : SchwartzMap ℝ ℂ) (x y : ℝ) : ψ.wignerKernelS (x, y) = ψ (x + y / 2) * (starRingEnd ℂ) (ψ (x - y / 2))

The Wigner function on the plane

noncomputable def SchwartzMap.wignerSchwartz (ψ : SchwartzMap ℝ ℂ) : SchwartzMap (ℝ × ℝ) ℂ

★★★ The Wigner function of a Schwartz state, as a Schwartz function on the plane.

Equations

• ψ.wignerSchwartz = SchwartzMap.partialFourierCLM ψ.wignerKernelS

theorem SchwartzMap.wignerSchwartz_apply (ψ : SchwartzMap ℝ ℂ) (x ξ : ℝ) : ψ.wignerSchwartz (x, ξ) = WignerFunction.wigner ψ x ξ

It is Wigner.lean's wigner at every point.