The composition of two Weyl operators is a Weyl operator

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate). BACKLOG #126(iii)(iv), the close of #126.

★★★ weylCLM_comp — Op(K₁) ∘ Op(K₂) = Op(K₁ ⋆ K₂) on the jointly Schwartz kernel class, with ★★★ weylCompKernel the composite kernel and ★★ weylCompKernel_apply its formula ∫ w, k₁(x, w)·k₂(w, z). #122 made Op(K) an operator on 𝓢(ℝ, ℂ); this is the first thing a calculus needs, and the first statement in which the operators compose rather than the integrals.

The reframing that makes it short

A Weyl operator is an integral operator with a Schwartz kernel: x and y enter K through the linear isomorphism (x, y) ↦ ((x+y)/2, x − y), so ★ weylKernelCLM (composition with it, which SchwartzMap.compCLMOfContinuousLinearEquiv makes a continuous linear map) turns the symbol-kernel into the integral kernel and back. In those coordinates composition is the classical kernel product, and the content is that the product is again Schwartz:

• ★ compAffineCLM — composition with an injective affine map on the right, as a CLM on Schwartz space. SchwartzMap.compCLMOfAntilipschitz wants an antilipschitz constant; ★ antilipschitzWith_affine_of_leftInverse supplies it from an explicit linear left inverse, which is what a concrete coordinate map always has;
• compPair — ((x, z), w) ↦ ((x, w), (w, z)), injective, so #126(i)'s tensor product composed with it is Schwartz on (ℝ × ℝ) × ℝ, and #126(ii)'s integralLastCLM integrates w out;
• ★★ weylCompKernel_apply — the formula, and ★★★ weylCLM_comp the operator identity, by integral_integral_swap with the integrability supplied by the same tensor construction at a fixed first argument.

Honest scope

⚠️ The symbol-level statement is not here. That the composite's symbol is the Moyal star product a ♯ b needs the joint partial Fourier transform of #121(ii), and the ℏ² expansion of the bracket is #64. This row is the operator identity with the kernel named, which is what is reachable without them.

⚠️ One kernel class, as in #122: jointly Schwartz kernels. Composition for a wider symbol class is a different theorem and is not proved here.

⚠️ No algebra structure is claimed. That ⋆ is associative, or that the Weyl operators of Schwartz kernels form an algebra, follows from this identity and the injectivity of weylKernelCLM — but neither is stated, and nothing needs them.

References: WeylSmooth.lean (#122, weylCLM), SchwartzTensor.lean (#126(i)), SchwartzPartialIntegral.lean (#126(ii)); specs/BACKLOG.md #126, #122, #121, #64.

Composition with an injective affine map

theorem WignerFunction.antilipschitzWith_affine_of_leftInverse {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (L : D →L[ℝ] E) (S : E →L[ℝ] D) (hS : ∀ (x : D), S (L x) = x) (c : E) : AntilipschitzWith ‖S‖₊ fun (x : D) => c + L x

★ An injective affine map is antilipschitz, with the constant read off an explicit linear left inverse. This is what SchwartzMap.compCLMOfAntilipschitz asks for, in the form a concrete coordinate map can supply.

noncomputable def WignerFunction.compAffineCLM {D : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace ℂ F] [SMulCommClass ℝ ℂ F] (L : D →L[ℝ] E) (S : E →L[ℝ] D) (hS : ∀ (x : D), S (L x) = x) (c : E) : SchwartzMap E F →L[ℂ] SchwartzMap D F

★ Composition with an injective affine map, as a continuous linear map on Schwartz space.

Equations

• WignerFunction.compAffineCLM L S hS c = SchwartzMap.compCLMOfAntilipschitz ℂ ⋯ ⋯

@[simp]

theorem WignerFunction.compAffineCLM_apply {D : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace ℂ F] [SMulCommClass ℝ ℂ F] (L : D →L[ℝ] E) (S : E →L[ℝ] D) (hS : ∀ (x : D), S (L x) = x) (c : E) (f : SchwartzMap E F) (x : D) : ((compAffineCLM L S hS c) f) x = f (c + L x)

A Weyl operator is the integral operator of a Schwartz kernel

noncomputable def WignerFunction.weylCoordsEquiv : (ℝ × ℝ) ≃ₗ[ℝ] ℝ × ℝ

The Weyl change of variables (x, y) ↦ ((x+y)/2, x − y), as a linear equivalence.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def WignerFunction.weylCoords : (ℝ × ℝ) ≃L[ℝ] ℝ × ℝ

The same, as a continuous linear equivalence.

Equations

• WignerFunction.weylCoords = WignerFunction.weylCoordsEquiv.toContinuousLinearEquiv

@[simp]

theorem WignerFunction.weylCoords_apply (p : ℝ × ℝ) : weylCoords p = ((p.1 + p.2) / 2, p.1 - p.2)

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

★ The integral kernel of a Weyl operator, as a continuous linear map of the symbol-kernel — and an invertible one, so every Schwartz kernel is the Weyl kernel of exactly one symbol-kernel.

Equations

• WignerFunction.weylKernelCLM = SchwartzMap.compCLMOfContinuousLinearEquiv ℂ WignerFunction.weylCoords

@[simp]

theorem WignerFunction.weylKernelCLM_apply (K : SchwartzMap (ℝ × ℝ) ℂ) (p : ℝ × ℝ) : (weylKernelCLM K) p = K ((p.1 + p.2) / 2, p.1 - p.2)

theorem WignerFunction.weylOpK_eq_integral_kernel (K : SchwartzMap (ℝ × ℝ) ℂ) (ψ : SchwartzMap ℝ ℂ) (x : ℝ) : weylOpK K ψ x = ∫ (y : ℝ), (weylKernelCLM K) (x, y) * ψ y

★ A Weyl operator is the integral operator of its kernel.

The composite kernel

def WignerFunction.compPairMap : (ℝ × ℝ) × ℝ →ₗ[ℝ] (ℝ × ℝ) × ℝ × ℝ

((x, z), w) ↦ ((x, w), (w, z)): the map that turns a pair of kernels into the integrand of their composition. It is injective, which is the only property needed.

Equations

• WignerFunction.compPairMap = { toFun := fun (r : (ℝ × ℝ) × ℝ) => ((r.1.1, r.2), r.2, r.1.2), map_add' := WignerFunction.compPairMap._proof_1, map_smul' := WignerFunction.compPairMap._proof_2 }

def WignerFunction.compPairInvMap : (ℝ × ℝ) × ℝ × ℝ →ₗ[ℝ] (ℝ × ℝ) × ℝ

Its linear left inverse, which is what makes it antilipschitz.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def WignerFunction.compPair : (ℝ × ℝ) × ℝ →L[ℝ] (ℝ × ℝ) × ℝ × ℝ

compPairMap as a continuous linear map.

Equations

• WignerFunction.compPair = LinearMap.toContinuousLinearMap WignerFunction.compPairMap

noncomputable def WignerFunction.compPairInv : (ℝ × ℝ) × ℝ × ℝ →L[ℝ] (ℝ × ℝ) × ℝ

compPairInvMap as a continuous linear map.

Equations

• WignerFunction.compPairInv = LinearMap.toContinuousLinearMap WignerFunction.compPairInvMap

@[simp]

theorem WignerFunction.compPair_apply (r : (ℝ × ℝ) × ℝ) : compPair r = ((r.1.1, r.2), r.2, r.1.2)

theorem WignerFunction.compPairInv_compPair (r : (ℝ × ℝ) × ℝ) : compPairInv (compPair r) = r

noncomputable def WignerFunction.weylCompIntegrand (K₁ K₂ : SchwartzMap (ℝ × ℝ) ℂ) : SchwartzMap ((ℝ × ℝ) × ℝ) ℂ

The integrand of the composition, as a Schwartz function of ((x, z), w): the tensor product of the two kernels, composed with the injective compPair.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem WignerFunction.weylCompIntegrand_apply (K₁ K₂ : SchwartzMap (ℝ × ℝ) ℂ) (x z w : ℝ) : (weylCompIntegrand K₁ K₂) ((x, z), w) = (weylKernelCLM K₁) (x, w) * (weylKernelCLM K₂) (w, z)

noncomputable def WignerFunction.weylCompKernel (K₁ K₂ : SchwartzMap (ℝ × ℝ) ℂ) : SchwartzMap (ℝ × ℝ) ℂ

★★★ The composite kernel. Jointly Schwartz, which is the whole content of #126: the integrand above is Schwartz on (ℝ × ℝ) × ℝ by #126(i) and the injectivity of compPair, #126(ii) integrates w out, and the Weyl change of variables carries the result back to a symbol-kernel.

Equations

• WignerFunction.weylCompKernel K₁ K₂ = (SchwartzMap.compCLMOfContinuousLinearEquiv ℂ WignerFunction.weylCoords.symm) (SchwartzMap.integralLastCLM (WignerFunction.weylCompIntegrand K₁ K₂))

theorem WignerFunction.weylCompKernel_apply (K₁ K₂ : SchwartzMap (ℝ × ℝ) ℂ) (x z : ℝ) : (weylKernelCLM (weylCompKernel K₁ K₂)) (x, z) = ∫ (w : ℝ), (weylKernelCLM K₁) (x, w) * (weylKernelCLM K₂) (w, z)

★★ The composite kernel is the classical kernel product.

The operator identity

def WignerFunction.slicePairMap : ℝ × ℝ →ₗ[ℝ] (ℝ × ℝ) × ℝ × ℝ

(w, z) ↦ ((0, w), (w, z)): the integration-variable part of the composition's integrand, at a fixed output point.

Equations

• WignerFunction.slicePairMap = { toFun := fun (r : ℝ × ℝ) => ((0, r.1), r.1, r.2), map_add' := ⋯, map_smul' := ⋯ }

def WignerFunction.slicePairInvMap : (ℝ × ℝ) × ℝ × ℝ →ₗ[ℝ] ℝ × ℝ

Its linear left inverse.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def WignerFunction.slicePair : ℝ × ℝ →L[ℝ] (ℝ × ℝ) × ℝ × ℝ

slicePairMap as a continuous linear map.

Equations

• WignerFunction.slicePair = LinearMap.toContinuousLinearMap WignerFunction.slicePairMap

noncomputable def WignerFunction.slicePairInv : (ℝ × ℝ) × ℝ × ℝ →L[ℝ] ℝ × ℝ

slicePairInvMap as a continuous linear map.

Equations

• WignerFunction.slicePairInv = LinearMap.toContinuousLinearMap WignerFunction.slicePairInvMap

theorem WignerFunction.slicePairInv_slicePair (r : ℝ × ℝ) : slicePairInv (slicePair r) = r

noncomputable def WignerFunction.weylCompSlice (K₁ K₂ : SchwartzMap (ℝ × ℝ) ℂ) (x : ℝ) : SchwartzMap (ℝ × ℝ) ℂ

The composition's integrand at a fixed output point, as a Schwartz function of the two integration variables. This is what supplies Fubini's integrability hypothesis.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem WignerFunction.weylCompSlice_apply (K₁ K₂ : SchwartzMap (ℝ × ℝ) ℂ) (x w z : ℝ) : (weylCompSlice K₁ K₂ x) (w, z) = (weylKernelCLM K₁) (x, w) * (weylKernelCLM K₂) (w, z)

theorem WignerFunction.integrable_weylCompIntegrand (K₁ K₂ : SchwartzMap (ℝ × ℝ) ℂ) (ψ : SchwartzMap ℝ ℂ) (x : ℝ) : MeasureTheory.Integrable (Function.uncurry fun (w z : ℝ) => (weylKernelCLM K₁) (x, w) * ((weylKernelCLM K₂) (w, z) * ψ z)) (MeasureTheory.volume.prod MeasureTheory.volume)

The composition's integrand is integrable on the two integration variables jointly, which is what integral_integral_swap needs.

theorem WignerFunction.weylOpK_comp (K₁ K₂ : SchwartzMap (ℝ × ℝ) ℂ) (ψ : SchwartzMap ℝ ℂ) (x : ℝ) : weylOpK K₁ ((weylCLM K₂) ψ) x = weylOpK (weylCompKernel K₁ K₂) ψ x

★★★ The composition of two Weyl operators is the Weyl operator of the composite kernel. In integral-kernel coordinates this is the classical kernel product, and the content is that the product is again a Schwartz kernel, which is what weylCompKernel is.

theorem WignerFunction.weylCLM_comp (K₁ K₂ : SchwartzMap (ℝ × ℝ) ℂ) : weylCLM K₁ ∘SL weylCLM K₂ = weylCLM (weylCompKernel K₁ K₂)

★★★ Op(K₁) ∘ Op(K₂) = Op(K₁ ⋆ K₂), as continuous linear maps of Schwartz space — row 126's statement.