The Weyl operator maps Schwartz space to Schwartz space

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate). BACKLOG #122, both halves.

#92(a1) proved the Weyl operator's output continuous on the Schwartz kernel class and said that continuity is the first of the Schwartz seminorm estimates, not the last. This file proves the rest of them and assembles the operator.

The smoothness half.

• ★★ iteratedFDeriv_comp_affine and ★★ norm_iteratedFDeriv_comp_affine_le — the iterated chain rule along an affine line, which is what the Weyl kernel needs because x enters K through ((x+y)/2, x−y) = (y/2, −y) + x·(1/2, 1): an affine path with constant velocity. Mathlib has the two halves (ContinuousLinearMap.iteratedFDeriv_comp_right for the linear part, iteratedFDeriv_comp_add_left for the translation) and not the composite;
• ★ exists_bound_snd_iteratedFDeriv — #92(a1)'s second-slot decay, now at every order;
• ★★ partialDeriv_weylIntegrand and ★★ norm_partialDeriv_weylIntegrand_le — the integrand's parameter derivatives, as an identity and in the primitive bound both halves run on;
• ★★★ contDiff_weylOpK — the output is C^∞, by #120 on each ball with the bound family the previous items supply.

The decay half, which #122 first recorded as blocked on a derivative formula. #125 supplied the formula, and this is what it buys:

• ★★ iteratedDeriv_weylOpK — #125's formula on this integrand, so that a weight has something to move onto;
• ★ abs_le_norm_weylPath — |x| ≤ (3/2)·‖A y x‖: the weight moves off the parameter and onto the kernel, which is the one inequality the whole half turns on;
• ★★ exists_bound_snd_iteratedFDeriv_weighted — the kernel's decay at orders N and N + 2 combined into a weighted bound that still has an integrable profile in the second slot;
• ★★★ exists_bound_weylOpK — every derivative decays in every weight, with the constant depending only on K and the bound linear in one seminorm of the state, which is the shape SchwartzMap.mkCLM consumes;
• ★★★ weylCLM — Op(K) : 𝓢(ℝ, ℂ) →L[ℂ] 𝓢(ℝ, ℂ), row 122's statement.

Honest scope

⚠️ One kernel class. weylCLM is the operator of a jointly Schwartz kernel. Weyl quantisation of a wider symbol class (polynomially bounded symbols, Hörmander classes) is a different theorem and is not proved here; #92's slicing caveat in WeylSymbolClass.lean still stands as written.

⚠️ The constant is not sharp. (3/2)ᴺ·C·π falls out of this route, not out of an optimisation.

⚠️ Nothing about composition. That Op(a) ∘ Op(b) is again a Weyl operator — the Moyal product — is a separate brick and is not proved here; WignerCalculus.lean carries the ℏ² statement this file does not touch.

References: WeylSymbolClass.lean (#92(a1), weylOpK, exists_bound_snd), ContDiffParametricIntegral.lean (#120 and #125, partialDeriv, contDiffOn_integral_of_bound, iteratedDeriv_integral_of_bound_le), SchwartzSlice.lean (#121(i)); specs/BACKLOG.md #122, #92, #120, #125.

The iterated chain rule along an affine line

theorem WignerFunction.iteratedFDeriv_comp_affine {H : Type u_1} {E : Type u_2} [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup E] [NormedSpace ℝ E] {K : H → E} (hK : ContDiff ℝ (↑⊤) K) (c v : H) (k : ℕ) (t : ℝ) : iteratedFDeriv ℝ k (fun (s : ℝ) => K (c + s • v)) t = (iteratedFDeriv ℝ k K (c + t • v)).compContinuousLinearMap fun (x : Fin k) => ContinuousLinearMap.smulRight 1 v

★★ The iterated derivative along an affine line, as an identity: the linear part contributes its velocity in every slot.

theorem WignerFunction.norm_iteratedFDeriv_comp_affine_le {H : Type u_1} {E : Type u_2} [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup E] [NormedSpace ℝ E] {K : H → E} (hK : ContDiff ℝ (↑⊤) K) (c v : H) (k : ℕ) (t : ℝ) : ‖iteratedFDeriv ℝ k (fun (s : ℝ) => K (c + s • v)) t‖ ≤ ‖iteratedFDeriv ℝ k K (c + t • v)‖ * ‖v‖ ^ k

★★ And the bound it gives: the velocity's norm to the order.

Second-slot decay at every order

theorem WignerFunction.exists_bound_snd_iteratedFDeriv (K : SchwartzMap (ℝ × ℝ) ℂ) (k : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (p : ℝ × ℝ), ‖iteratedFDeriv ℝ k (⇑K) p‖ ≤ C * (1 + p.2 ^ 2)⁻¹

★ #92(a1)'s second-slot decay, at every order of derivative.

The Weyl kernel as an affine path

theorem WignerFunction.weylKernel_eq_affine (y x : ℝ) : ((x + y) / 2, x - y) = (y / 2, -y) + x • (1 / 2, 1)

The affine path the Weyl kernel's argument travels as x varies.

theorem WignerFunction.norm_weylVelocity : ‖(1 / 2, 1)‖ = 1

The path's velocity is a unit vector, which is why no power of it appears in any bound.

theorem WignerFunction.snd_weylPath (x y : ℝ) : ((y / 2, -y) + x • (1 / 2, 1)).2 = x - y

The second slot of the path is x - y, which is what carries the decay.

theorem WignerFunction.abs_le_norm_weylPath (x y : ℝ) : |x| ≤ 3 / 2 * ‖(y / 2, -y) + x • (1 / 2, 1)‖

★ The weight transfers to the path. |x| ≤ (3/2)‖path‖, so a polynomial weight in x can be moved onto the kernel — which is what the decay estimate runs on.

theorem WignerFunction.contDiff_weylPath (K : SchwartzMap (ℝ × ℝ) ℂ) (y : ℝ) : ContDiff ℝ ↑⊤ fun (x : ℝ) => K ((y / 2, -y) + x • (1 / 2, 1))

The path is smooth in the parameter.

The integrand, its parameter derivatives, and the bound they obey

noncomputable def WignerFunction.weylIntegrand (K : SchwartzMap (ℝ × ℝ) ℂ) (ψ : SchwartzMap ℝ ℂ) : ℝ → ℝ → ℂ

The Weyl operator's integrand.

Equations

• WignerFunction.weylIntegrand K ψ x y = K ((x + y) / 2, x - y) * ψ y

theorem WignerFunction.weylOpK_eq_integral (K : SchwartzMap (ℝ × ℝ) ℂ) (ψ : SchwartzMap ℝ ℂ) : weylOpK K ψ = fun (x : ℝ) => ∫ (y : ℝ), weylIntegrand K ψ x y

theorem WignerFunction.weylIntegrand_slice (K : SchwartzMap (ℝ × ℝ) ℂ) (ψ : SchwartzMap ℝ ℂ) (y : ℝ) : (fun (x : ℝ) => weylIntegrand K ψ x y) = ψ y • fun (x : ℝ) => K ((y / 2, -y) + x • (1 / 2, 1))

theorem WignerFunction.contDiff_weylIntegrand (K : SchwartzMap (ℝ × ℝ) ℂ) (ψ : SchwartzMap ℝ ℂ) (m : ℕ) (y : ℝ) : ContDiff ℝ ↑m fun (x : ℝ) => weylIntegrand K ψ x y

theorem WignerFunction.partialDeriv_weylIntegrand (K : SchwartzMap (ℝ × ℝ) ℂ) (ψ : SchwartzMap ℝ ℂ) (k : ℕ) (x y : ℝ) : partialDeriv (weylIntegrand K ψ) k x y = ψ y • (iteratedFDeriv ℝ k (fun (s : ℝ) => K ((y / 2, -y) + s • (1 / 2, 1))) x) fun (x : Fin k) => 1

★★ The parameter derivatives of the integrand, as an identity. ψ does not depend on the parameter, so no product rule enters: the whole x-dependence is the affine path.

theorem WignerFunction.norm_partialDeriv_weylIntegrand_le (K : SchwartzMap (ℝ × ℝ) ℂ) (ψ : SchwartzMap ℝ ℂ) (k : ℕ) (x y : ℝ) : ‖partialDeriv (weylIntegrand K ψ) k x y‖ ≤ ‖ψ y‖ * ‖iteratedFDeriv ℝ k (⇑K) ((y / 2, -y) + x • (1 / 2, 1))‖

★★ The bound they obey, in the primitive form both halves of #122 use: the state's value times the kernel's k-th derivative at the path point. The velocity contributes nothing because it is a unit vector.

theorem WignerFunction.aestronglyMeasurable_partialDeriv_weylIntegrand (K : SchwartzMap (ℝ × ℝ) ℂ) (ψ : SchwartzMap ℝ ℂ) (k : ℕ) (x : ℝ) : MeasureTheory.AEStronglyMeasurable (partialDeriv (weylIntegrand K ψ) k x) MeasureTheory.volume

theorem WignerFunction.inv_one_add_sq_le_of_abs_sub_le {x₀ x y : ℝ} (hx : |x - x₀| ≤ 1) : (1 + (x - y) ^ 2)⁻¹ ≤ 4 * (1 + (y - x₀) ^ 2)⁻¹

The majorant the second-slot decay supplies, uniformly on a unit ball of parameters.

theorem WignerFunction.exists_weylIntegrand_ball_bound (K : SchwartzMap (ℝ × ℝ) ℂ) (ψ : SchwartzMap ℝ ℂ) (x₀ : ℝ) : ∃ (bound : ℕ → ℝ → ℝ), (∀ (k : ℕ), MeasureTheory.Integrable (bound k) MeasureTheory.volume) ∧ ∀ (k : ℕ), ∀ x ∈ Metric.ball x₀ 1, ∀ (y : ℝ), ‖partialDeriv (weylIntegrand K ψ) k x y‖ ≤ bound k y

The dominating bound both #120 statements consume, assembled once: on a unit ball of parameters every parameter derivative is dominated by an integrable profile in the integration variable.

theorem WignerFunction.contDiff_weylOpK (K : SchwartzMap (ℝ × ℝ) ℂ) (ψ : SchwartzMap ℝ ℂ) (m : ℕ) : ContDiff ℝ (↑m) (weylOpK K ψ)

★★★ The Weyl operator's output is C^∞. #92(a1) gave continuity; this gives every order, by #120 on each ball with the bound supplied by the affine chain rule and the kernel's second-slot decay.

theorem WignerFunction.iteratedDeriv_weylOpK (K : SchwartzMap (ℝ × ℝ) ℂ) (ψ : SchwartzMap ℝ ℂ) (k : ℕ) (x : ℝ) : iteratedDeriv k (weylOpK K ψ) x = ∫ (y : ℝ), partialDeriv (weylIntegrand K ψ) k x y

★★ #125's formula on this integrand: every derivative of the output is the integral of the corresponding parameter derivative. The decay estimate is stated on the right-hand side, which is why the smoothness statement above is not enough on its own.

The output's decay

Smoothness alone does not make Op(K) ψ a Schwartz function: every derivative must decay in every polynomial weight too. The weight moves off the parameter and onto the kernel through abs_le_norm_weylPath, the kernel's own decay at two orders apart supplies a majorant that is still integrable in the integration variable, and ∫ (1 + y²)⁻¹ = π finishes it. The constant comes out depending only on the kernel, and the bound linear in a single seminorm of the state — which is exactly the hypothesis SchwartzMap.mkCLM consumes.

theorem WignerFunction.exists_bound_snd_iteratedFDeriv_weighted (K : SchwartzMap (ℝ × ℝ) ℂ) (N k : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (p : ℝ × ℝ), ‖p‖ ^ N * ‖iteratedFDeriv ℝ k (⇑K) p‖ ≤ C * (1 + p.2 ^ 2)⁻¹

★★ Weighted second-slot decay. exists_bound_snd_iteratedFDeriv is the case N = 0: the kernel's decay at orders N and N + 2 combine into a bound that already carries the weight ‖p‖ ^ N and still decays in the second slot.

theorem WignerFunction.norm_real_smul_eq {t : ℝ} (z : ℂ) (ht : 0 ≤ t) : t * ‖z‖ = ‖t • z‖

A real scalar can be moved under a norm, which is how the weight gets inside the integral.

theorem WignerFunction.exists_bound_weylOpK (K : SchwartzMap (ℝ × ℝ) ℂ) (N k : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (ψ : SchwartzMap ℝ ℂ) (x : ℝ), ‖x‖ ^ N * ‖iteratedFDeriv ℝ k (weylOpK K ψ) x‖ ≤ C * (SchwartzMap.seminorm ℂ 0 0) ψ

★★★ Every derivative of the output decays, in every weight. The constant depends only on the kernel and the bound is linear in one seminorm of the state: this is the Schwartz seminorm estimate #92(a1) called continuity the first of, now at every order and weight.

The operator on Schwartz space

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

★★★ Op(K) is a continuous linear map 𝓢(ℝ, ℂ) →L[ℂ] 𝓢(ℝ, ℂ) — row 122's statement, and the form every further Weyl-calculus statement (composition, the Moyal product, adjoints) needs. The two halves are exactly the two hypotheses: smoothness from contDiff_weylOpK, decay from exists_bound_weylOpK, with the single seminorm on the right.

Equations

• WignerFunction.weylCLM K = SchwartzMap.mkCLM (fun (ψ : SchwartzMap ℝ ℂ) => WignerFunction.weylOpK K ψ) ⋯ ⋯ ⋯ ⋯

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

★ The row reads on weylOp, not only on weylOpK. #121(i)'s slice family is what discharges the gating this row recorded: the continuous linear map above is the Weyl operator of the slice family, so Op(a) : 𝓢(ℝ, ℂ) →L 𝓢(ℝ, ℂ) holds in the vocabulary #92 stated it in.

@[simp]

theorem WignerFunction.weylCLM_apply (K : SchwartzMap (ℝ × ℝ) ℂ) (ψ : SchwartzMap ℝ ℂ) (x : ℝ) : ((weylCLM K) ψ) x = weylOpK K ψ x