The Weyl operator's symbol class

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate). BACKLOG #92(a), brick (a1).

#92's measurement of its own part (a) was that Op(a) as a continuous operator on 𝓢(ℝ, ℂ) is not a gap in the proofs but a statement needing a different symbol class: with weylOp's datum — a family b : ℝ → 𝓢(ℝ, ℂ) with no regularity in its first slot — weylOp b ψ need not even be continuous. WignerWeyl.lean works around this by assuming what it needs: integrable_weylPair takes joint continuity (hbc) and a uniform bound integrable in the first slot (hM, hbM) as hypotheses.

This file fixes the class and discharges those hypotheses as theorems.

• ★ exists_bound_fst, ★ exists_bound_snd — a Schwartz function on the plane decays like (1 + t²)⁻¹ in each slot separately, uniformly in the other. Two orders of SchwartzMap.decay (k = 2 and k = 0) and ‖p‖² ≥ pᵢ²;
• weylOpK — the Weyl operator of a jointly Schwartz kernel, and ★ weylOpK_eq_weylOp: it agrees with weylOp of any slice family, so everything already proved about weylOp transfers whenever a slice family is available;
• ★ continuous_weylKernel and ★★ exists_integrable_bound — WignerWeyl.lean's three assumed hypotheses, now theorems on this class;
• ★ integrable_weylOpK_integrand and ★★ continuous_weylOpK — the defect #92 recorded, fixed: on the Schwartz kernel class the Weyl operator's output is continuous, by dominated continuity against 4C·(1 + (y − x₀)²)⁻¹, the majorant the second-slot decay supplies uniformly on a unit ball of parameters.

Honest scope

⚠️ This is the symbol class, not the calculus. Op(a) : 𝓢(ℝ, ℂ) →L 𝓢(ℝ, ℂ) is not proved — continuity of the output function is the first of the Schwartz seminorm estimates, not the last. The remaining obstruction is the one #92 measured and it is unchanged: smoothness of the output to all orders needs differentiation under the integral sign to all orders with bounds, which the pin has in no form for integrals over ℝ (the corpus's ContDiffParametricIntervalIntegral.lean, from #60, is interval integrals on a compact interval, where the bounds come free from continuity).

⚠️ No slicing here. weylOpK_eq_weylOp takes a slice family as a hypothesis. That a Schwartz function on the plane slices into a Schwartz-valued family is the two-variable Schwartz API #92 named as absent when this file was written; it is now SchwartzSlice.lean (#121(i), SchwartzMap.slice), and the symbol of a sliced kernel is a Schwartz function on the plane by PartialFourierCLM.lean (#121(ii), partialFourierCLM_apply_eq_weylSymbol). The properties above are still proved for weylOpK directly, as written.

References: WignerWeyl.lean (weylOp, integrable_weylPair, integral_conj_mul_weylOp), WignerCalculus.lean (#92(b)(c)), Mathlib/Analysis/Calculus/ContDiffParametricIntervalIntegral.lean (#60, the interval case); specs/BACKLOG.md #92, #63, #60.

A Schwartz function on the plane decays in each slot separately

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

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

The Weyl operator of a jointly Schwartz kernel

noncomputable def WignerFunction.weylOpK (K : SchwartzMap (ℝ × ℝ) ℂ) (ψ : SchwartzMap ℝ ℂ) (x : ℝ) : ℂ

The Weyl operator of a jointly Schwartz kernel. Same integral as weylOp, with the kernel given as one Schwartz function on the plane instead of a family with no regularity in its first slot.

Equations

• WignerFunction.weylOpK K ψ x = ∫ (y : ℝ), K ((x + y) / 2, x - y) * ψ y

theorem WignerFunction.weylOpK_eq_weylOp (K : SchwartzMap (ℝ × ℝ) ℂ) (b : ℝ → SchwartzMap ℝ ℂ) (hb : ∀ (u w : ℝ), (b u) w = K (u, w)) (ψ : SchwartzMap ℝ ℂ) (x : ℝ) : weylOpK K ψ x = weylOp b ψ x

★ The bridge. Whenever a slice family is available, this is weylOp of it — so every statement already proved about weylOp transfers. The hypothesis is what the absent two-variable Schwartz API would supply.

theorem WignerFunction.continuous_weylKernel (K : SchwartzMap (ℝ × ℝ) ℂ) : Continuous fun (p : ℝ × ℝ) => K (p.1, p.2)

★ WignerWeyl.lean's joint-continuity hypothesis, now a theorem.

theorem WignerFunction.exists_integrable_bound (K : SchwartzMap (ℝ × ℝ) ℂ) : ∃ (M : ℝ → ℝ), MeasureTheory.Integrable M MeasureTheory.volume ∧ ∀ (u w : ℝ), ‖K (u, w)‖ ≤ M u

★★ WignerWeyl.lean's two bound hypotheses, now a theorem: on the Schwartz kernel class there is a bound integrable in the first slot and uniform in the second.

theorem WignerFunction.norm_weylKernel_le {K : SchwartzMap (ℝ × ℝ) ℂ} {C : ℝ} (hC0 : 0 ≤ C) (hC : ∀ (p : ℝ × ℝ), ‖K p‖ ≤ C * (1 + p.2 ^ 2)⁻¹) {x₀ x : ℝ} (hx : |x - x₀| ≤ 1) (y : ℝ) : ‖K ((x + y) / 2, x - y)‖ ≤ 4 * C * (1 + (y - x₀) ^ 2)⁻¹

The majorant the second-slot decay supplies, uniformly for parameters in a unit ball.

theorem WignerFunction.integrable_weylOpK_integrand (K : SchwartzMap (ℝ × ℝ) ℂ) (ψ : SchwartzMap ℝ ℂ) (x : ℝ) : MeasureTheory.Integrable (fun (y : ℝ) => K ((x + y) / 2, x - y) * ψ y) MeasureTheory.volume

★ The defining integral converges, with no hypotheses.

theorem WignerFunction.continuous_weylOpK (K : SchwartzMap (ℝ × ℝ) ℂ) (ψ : SchwartzMap ℝ ℂ) : Continuous (weylOpK K ψ)

★★ The defect #92 recorded, fixed: on the Schwartz kernel class the Weyl operator's output is continuous. Dominated continuity against the second-slot majorant, which is uniform for parameters within 1 of the point.