The Weyl operators of Schwartz kernels form a non-unital algebra

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate). BACKLOG #127, out of #126.

#126 proved Op(K₁) ∘ Op(K₂) = Op(K₁ ⋆ K₂) and claimed nothing about the structure. This is the structure, and the keystone is a theorem the row did not have:

• ★★★ weylOpK_injective — the kernel is determined by the operator. Op is faithful on the Schwartz kernel class, so a statement about operators can be pulled back to a statement about kernels;
• ★★★ weylCompKernel_assoc — ⋆ is associative, and ★★ weylCompKernel_add_left/_right, _smul_left/_right — it is bilinear. All four are corollaries of faithfulness and the corresponding fact about operators, which is where the work went;
• ★★★ not_weylOpK_eq_id and ★★★ weylCLM_ne_one — there is no unit. No Schwartz kernel represents the identity operator, so this is a genuinely non-unital algebra.

The correction this row records

#127's own entry said associativity would follow from "associativity of operator composition and the injectivity of weylKernelCLM". That route does not close. weylKernelCLM is the change of coordinates (x, y) ↦ ((x+y)/2, x − y), and its injectivity says nothing about whether two different kernels can give the same operator — which is exactly what is needed to turn an identity between operators into an identity between kernels. The ingredient is faithfulness of Op, and that is a theorem rather than bookkeeping: ★★★ weylOpK_injective is proved by feeding the operator the conjugate of its own kernel slice (SchwartzMap.conjCLM of #121(i)'s slice), which turns the pairing into ∫ ‖k(x, y)‖² dy; that vanishes only if the slice vanishes almost everywhere, and a continuous function vanishing almost everywhere for Lebesgue measure vanishes.

Honest scope

⚠️ No Mul instance, deliberately. Declaring ⋆ as the Mul of 𝓢(ℝ × ℝ, ℂ) would commit the type globally to the Weyl product, when the pointwise product is at least as natural a choice and a NonUnitalAlgebra instance would then fix which one every downstream file means. The facts are stated as theorems; a bundled NonUnitalAlgHom is one letI away for a consumer who wants it, and nothing in the corpus does.

⚠️ Nothing about the symbol product. Faithfulness here is of K ↦ Op(K) on kernels; that the symbol composes by the Moyal star product still needs #121(ii), and the ℏ² expansion is #64.

⚠️ The non-unitality is stated for this class only. That no Schwartz kernel gives the identity is proved; a wider class (distributional kernels, where the identity's kernel is a delta) is a different setting and is not formalised.

References: WeylComposition.lean (#126, weylCompKernel, weylCLM_comp), SchwartzSlice.lean (#121(i), slice), WeylSmooth.lean (#122, weylCLM); specs/BACKLOG.md #127, #126, #122, #64.

Conjugation on Schwartz space

Needed to feed the operator the conjugate of its own kernel slice. Conjugation is ℝ-linear and not ℂ-linear, which is why this is a map over ℝ; only its values matter below.

noncomputable def SchwartzMap.conjCLM {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] : SchwartzMap E ℂ →L[ℝ] SchwartzMap E ℂ

Complex conjugation on Schwartz space, as a continuous ℝ-linear map.

Equations

• SchwartzMap.conjCLM = SchwartzMap.postcompCLM Complex.conjLIE.toLinearIsometry.toContinuousLinearMap

@[simp]

theorem SchwartzMap.conjCLM_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : SchwartzMap E ℂ) (x : E) : (conjCLM f) x = (starRingEnd ℂ) (f x)

The Weyl operator is linear in its kernel

theorem WignerFunction.weylOpK_add_kernel (K₁ K₂ : SchwartzMap (ℝ × ℝ) ℂ) (ψ : SchwartzMap ℝ ℂ) (x : ℝ) : weylOpK (K₁ + K₂) ψ x = weylOpK K₁ ψ x + weylOpK K₂ ψ x

theorem WignerFunction.weylOpK_sub_kernel (K₁ K₂ : SchwartzMap (ℝ × ℝ) ℂ) (ψ : SchwartzMap ℝ ℂ) (x : ℝ) : weylOpK (K₁ - K₂) ψ x = weylOpK K₁ ψ x - weylOpK K₂ ψ x

theorem WignerFunction.weylOpK_smul_kernel (c : ℂ) (K : SchwartzMap (ℝ × ℝ) ℂ) (ψ : SchwartzMap ℝ ℂ) (x : ℝ) : weylOpK (c • K) ψ x = c * weylOpK K ψ x

Faithfulness: the kernel is determined by the operator

theorem WignerFunction.weylKernelCLM_apply' (K : SchwartzMap (ℝ × ℝ) ℂ) (p : ℝ × ℝ) : (weylKernelCLM K) p = K (weylCoords p)

The change of coordinates, in the form the injectivity argument uses.

theorem WignerFunction.weylKernelCLM_injective : Function.Injective ⇑weylKernelCLM

The change of coordinates is injective, because it is composition with a surjection.

theorem WignerFunction.integrable_norm_sq (f : SchwartzMap ℝ ℂ) : MeasureTheory.Integrable (fun (y : ℝ) => ‖f y‖ ^ 2) MeasureTheory.volume

The squared modulus of a Schwartz function is integrable, which is what the pairing below produces.

theorem WignerFunction.eq_zero_of_weylOpK_eq_zero {K : SchwartzMap (ℝ × ℝ) ℂ} (h : ∀ (ψ : SchwartzMap ℝ ℂ) (x : ℝ), weylOpK K ψ x = 0) : K = 0

★★★ The kernel is determined by the operator. A kernel whose operator annihilates every state is zero — fed the conjugate of its own slice, the operator returns ∫ ‖k(x, y)‖² dy, which vanishes only if the slice does. This is what #127's entry was missing, and it is a theorem rather than bookkeeping.

theorem WignerFunction.weylOpK_injective {K₁ K₂ : SchwartzMap (ℝ × ℝ) ℂ} (h : ∀ (ψ : SchwartzMap ℝ ℂ) (x : ℝ), weylOpK K₁ ψ x = weylOpK K₂ ψ x) : K₁ = K₂

★★★ Op is faithful on the Schwartz kernel class.

theorem WignerFunction.weylCLM_injective : Function.Injective weylCLM

★★ The same, for the packaged operators of #122.

The algebra laws

theorem WignerFunction.weylCompKernel_assoc (K₁ K₂ K₃ : SchwartzMap (ℝ × ℝ) ℂ) : weylCompKernel (weylCompKernel K₁ K₂) K₃ = weylCompKernel K₁ (weylCompKernel K₂ K₃)

★★★ ⋆ is associative. Operator composition is associative and Op is faithful, so the identity descends to the kernels.

theorem WignerFunction.weylCompKernel_add_left (K₁ K₂ K₃ : SchwartzMap (ℝ × ℝ) ℂ) : weylCompKernel (K₁ + K₂) K₃ = weylCompKernel K₁ K₃ + weylCompKernel K₂ K₃

★★ ⋆ is additive in its left argument.

theorem WignerFunction.weylCompKernel_add_right (K₁ K₂ K₃ : SchwartzMap (ℝ × ℝ) ℂ) : weylCompKernel K₁ (K₂ + K₃) = weylCompKernel K₁ K₂ + weylCompKernel K₁ K₃

★★ ⋆ is additive in its right argument. The right slot is the inner operator, so this one goes through the operators' action rather than through linearity in the kernel alone.

theorem WignerFunction.weylCompKernel_smul_left (c : ℂ) (K₁ K₂ : SchwartzMap (ℝ × ℝ) ℂ) : weylCompKernel (c • K₁) K₂ = c • weylCompKernel K₁ K₂

★★ ⋆ is homogeneous in its left argument.

theorem WignerFunction.weylCompKernel_smul_right (c : ℂ) (K₁ K₂ : SchwartzMap (ℝ × ℝ) ℂ) : weylCompKernel K₁ (c • K₂) = c • weylCompKernel K₁ K₂

★★ ⋆ is homogeneous in its right argument.

There is no unit

The identity operator is not the Weyl operator of any Schwartz kernel. A unit would have to reproduce every state's value at every point from an integral against a bounded kernel, and a shrinking bump has value 1 at the centre while its integral against anything integrable tends to 0.

noncomputable def WignerFunction.shrinkBump (n : ℕ) : SchwartzMap ℝ ℂ

A bump at 0 of outer radius 2/(n+1), as a complex Schwartz function: value 1 at 0 for every n, supported in a ball that shrinks to nothing.

Equations

• WignerFunction.shrinkBump n = ⋯.toSchwartzMap ⋯

theorem WignerFunction.shrinkBump_apply (n : ℕ) (y : ℝ) : (shrinkBump n) y = ↑(↑{ rIn := 1 / (↑n + 1), rOut := 2 / (↑n + 1), rIn_pos := ⋯, rIn_lt_rOut := ⋯ } y)

theorem WignerFunction.shrinkBump_zero (n : ℕ) : (shrinkBump n) 0 = 1

theorem WignerFunction.norm_shrinkBump_le_one (n : ℕ) (y : ℝ) : ‖(shrinkBump n) y‖ ≤ 1

theorem WignerFunction.shrinkBump_eq_zero_of_ne (n : ℕ) {y : ℝ} (hy : 2 / (↑n + 1) ≤ |y|) : (shrinkBump n) y = 0

theorem WignerFunction.tendsto_shrinkBump (y : ℝ) (hy : y ≠ 0) : Filter.Tendsto (fun (n : ℕ) => (shrinkBump n) y) Filter.atTop (nhds 0)

theorem WignerFunction.not_weylOpK_eq_id (K : SchwartzMap (ℝ × ℝ) ℂ) : ¬∀ (ψ : SchwartzMap ℝ ℂ) (x : ℝ), weylOpK K ψ x = ψ x

★★★ No Schwartz kernel represents the identity, so the algebra of #126 is genuinely non-unital. The witness is the shrinking bump: it keeps the value 1 at the origin while its pairing with the kernel's slice tends to 0.

theorem WignerFunction.weylCLM_ne_one (K : SchwartzMap (ℝ × ℝ) ℂ) : weylCLM K ≠ ContinuousLinearMap.id ℂ (SchwartzMap ℝ ℂ)

★★★ The same, for the packaged operator: no K has weylCLM K = 1.