Slicing a Schwartz function on a product

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate). BACKLOG #121(i), out of #92's split.

A Schwartz function on a product restricts to a Schwartz function on each slice. Mathlib has the machinery — SchwartzMap.compCLM composes on the right with any map of temperate growth that does not shrink the norm too much — but not the instance, because the slice map w ↦ (e, w) is affine rather than linear and fun_prop has no Prod.mk rule for HasTemperateGrowth.

• ★ Function.hasTemperateGrowth_prodMk_left — the slice map has temperate growth, through HasTemperateGrowth.of_fderiv: its derivative is the constant inr, and ‖(e, w)‖ grows linearly;
• SchwartzMap.sliceCLM and SchwartzMap.slice — the slice, as a continuous linear map in the kernel, with ★ SchwartzMap.slice_apply its defining equation slice K e w = K (e, w);
• ★★★ WignerFunction.integral_conj_mul_weylOpK — the payoff: the Weyl expectation formula holds on the Schwartz kernel class with no hypotheses. WignerWeyl.lean states it for a slice family under three assumptions (joint continuity, and a bound integrable in the first slot); #92(a1) discharged the last two for a jointly Schwartz kernel, and the slice supplies the family itself, so nothing is left to assume.

Honest scope

⚠️ Continuity in the slice parameter is not proved, and that is the other half of #121(i). What is continuous here is slicing in the kernel (sliceCLM is a continuous linear map 𝓢(E × F, G) →L 𝓢(F, G) for each fixed e), which is what transfers theorems. That e ↦ slice K e is continuous into 𝓢(F, G) for the Schwartz topology is a different statement, it needs one more order of decay and a mean-value estimate in the sliced variable, and Mathlib has no curry 𝓢(E × F, G) ≃ 𝓢(E, 𝓢(F, G)) to get it from. It is #123, and nothing in the corpus needs it.

⚠️ No partial Fourier transform, which is #121(ii) and the half a pseudodifferential calculus would need. Done 2026-10-21: PartialFourierCLM.lean (#170–#174), ★★★ SchwartzMap.partialFourierCLM : 𝓢(ℝ × ℝ, ℂ) →L[ℂ] 𝓢(ℝ × ℝ, ℂ).

References: WeylSymbolClass.lean (#92(a1), weylOpK, weylOpK_eq_weylOp, exists_integrable_bound), WignerWeyl.lean (weylOp, weylSymbol, integral_conj_mul_weylOp); specs/BACKLOG.md #121, #92, #123.

The slice map has temperate growth

theorem Function.hasTemperateGrowth_prodMk_left {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (e : E) : HasTemperateGrowth fun (w : F) => (e, w)

★ The slice map w ↦ (e, w) has temperate growth. It is affine, so fun_prop cannot see it: the derivative is the constant inr and the value grows linearly.

theorem exists_norm_le_prodMk_left {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] (e : E) : ∃ (k : ℕ) (C : ℝ), ∀ (w : F), ‖w‖ ≤ C * (1 + ‖(e, w)‖) ^ k

The slice map does not shrink the norm, which is compCLM's other hypothesis.

The slice

noncomputable def SchwartzMap.sliceCLM {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (𝕜 : Type u_4) [RCLike 𝕜] [NormedSpace 𝕜 G] (e : E) : SchwartzMap (E × F) G →L[𝕜] SchwartzMap F G

Slicing a Schwartz function on a product, as a continuous linear map in the kernel.

Equations

• SchwartzMap.sliceCLM 𝕜 e = SchwartzMap.compCLM 𝕜 ⋯ ⋯

noncomputable def SchwartzMap.slice {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (K : SchwartzMap (E × F) G) (e : E) : SchwartzMap F G

The slice of a Schwartz function on a product: a Schwartz function on the second factor.

Equations

• K.slice e = (SchwartzMap.sliceCLM ℝ e) K

@[simp]

theorem SchwartzMap.slice_apply {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (K : SchwartzMap (E × F) G) (e : E) (w : F) : (K.slice e) w = K (e, w)

★ The defining equation of the slice.

The payoff: the Weyl expectation formula, hypothesis-free

theorem WignerFunction.weylOpK_eq_weylOp_slice (K : SchwartzMap (ℝ × ℝ) ℂ) (ψ : SchwartzMap ℝ ℂ) (x : ℝ) : weylOpK K ψ x = weylOp K.slice ψ x

★ The kernel-class Weyl operator is weylOp of the kernel's slice family — no longer a hypothesis, since SchwartzMap.slice supplies the family.

theorem WignerFunction.integral_conj_mul_weylOpK (K : SchwartzMap (ℝ × ℝ) ℂ) (ψ : SchwartzMap ℝ ℂ) : ∫ (x : ℝ), (starRingEnd ℂ) (ψ x) * weylOpK K ψ x = ∫ (u : ℝ) (ξ : ℝ), weylSymbol K.slice u ξ * wigner ψ u ξ

★★★ The Weyl expectation formula on the Schwartz kernel class, with no hypotheses. The expectation of the Weyl operator in a state is the phase-space average of the symbol against the state's Wigner function.

WignerWeyl.lean proves this for a slice family under three assumptions, because its datum could not supply them: joint continuity of the kernel, and a bound integrable in the first slot. #92(a1) discharged the latter two for a jointly Schwartz kernel (continuous_weylKernel, exists_integrable_bound) and SchwartzMap.slice supplies the family, so on this class the formula is unconditional.