The Wigner function on L², and its time derivative along the interacting orbit

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #167 (out of #64: the interacting Wigner equation, first brick).

The corpus's Wigner function (Wigner.lean) is defined on Schwartz functions, where the kernel y ↦ ψ(x + y/2) conj ψ(x − y/2) is itself Schwartz. The interacting Schrödinger orbit U(t)ψ of #129/#154 lives in L² (in dom H₀, operator-theoretically), not in Schwartz space, so to differentiate W_{U(t)ψ} in t the Wigner function has to exist on L² first. It does, in the momentum form: for φ, ψ ∈ L²(ℝ),

W(φ, ψ)(x, ξ) = 2 ∫ e(2xu) · ψ̂(ξ + u) · conj φ̂(ξ − u) du = 2 ⟪ L_ξ φ, R_{x,ξ} ψ ⟫_{L²},

where L_ξ φ = φ̂(ξ − ·) and R_{x,ξ} ψ = e(2x·) ψ̂(ξ + ·) are isometries of L² (Plancherel, a reflection/translation of Lebesgue measure, and a unimodular multiplier). Writing W as an inner product of two continuous linear images of the states is what makes everything else one line: the integrand is integrable, |W| ≤ 2‖φ‖‖ψ‖, and t ↦ W(ψ_t, ψ_t) is differentiable whenever t ↦ ψ_t is differentiable in L², with ∂_t W = W(ψ̇, ψ) + W(ψ, ψ̇).

• WignerFunction.reflectAt, shiftAt, phaseLinf, wignerLeft, wignerRight — the two continuous linear maps, with their almost-everywhere values;
• ★ WignerFunction.wignerL2, wignerL2_eq_integral — the Wigner function of two L² states, and its integral formula;
• ★ WignerFunction.norm_wignerL2_le — ‖W(φ, ψ)(x, ξ)‖ ≤ 2 ‖φ‖ ‖ψ‖;
• ★★ WignerFunction.wignerL2_toLp — on a Schwartz state it is the Wigner function of Wigner.lean (through wigner_fourier, Mathlib's SchwartzMap.toLp_fourier_eq, and the substitution y = 2u);
• ★★ WignerFunction.hasDerivAt_wignerL2 — the chain rule: along any L²-differentiable path, ∂_t W(ψ_t, ψ_t) = W(ψ̇_t, ψ_t) + W(ψ_t, ψ̇_t) pointwise in (x, ξ);
• ★★★ WignerFunction.hasDerivAt_wignerL2_schrodinger — along the interacting orbit ψ_t = U(t)ψ₀ (bounded real potential, ψ₀ ∈ dom H₀), for every t > 0, ∂_t W_{ψ_t}(x, ξ) = W(−i(H₀ + V)ψ_t, ψ_t) + W(ψ_t, −i(H₀ + V)ψ_t), with H₀ acting on the orbit point — the interacting Wigner equation in its first, operator form.

Honest scope

• The two halves of the right-hand side are identified downstream: W(−iH₀ψ, ψ) + W(ψ, −iH₀ψ) = −2πξ ∂_x W_ψ for ψ ∈ dom H₀ in WignerFree.lean (#168), and W(−iVψ, ψ) + W(ψ, −iVψ) = moyalPotL2 V ψ ψ (the Moyal term of MoyalBracket.lean, on L²) in WignerPotential.lean (#169), which assembles ∂_t W = −2πξ ∂_x W + moyalPotL2, the equation #64 named.
• V enters as an L^∞ class (potential VL), as in #129/#154; the orbit is the Dyson/Trotter propagator schrodinger of BoundedPerturbation.lean.
• One space dimension.

References: E. Wigner, Phys. Rev. 40 (1932) 749; Wigner.lean (wigner, wigner_fourier), PhaseGeneratorDomain.lean (#154, hasDerivAt_schrodinger_orbit), MoyalBracket.lean, WignerEvolution.lean; Mathlib Analysis/Fourier/LpSpace.lean (Lp.fourierTransformₗᵢ, SchwartzMap.toLp_fourier_eq); specs/BACKLOG.md #167, #64.

The two continuous linear maps

noncomputable def WignerFunction.reflectAt (ξ : ℝ) : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume) →ₗᵢ[ℂ] ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

u ↦ f(ξ − u), an isometry of L².

Equations

• WignerFunction.reflectAt ξ = MeasureTheory.Lp.compMeasurePreservingₗᵢ ℂ (fun (u : ℝ) => ξ - u) ⋯

noncomputable def WignerFunction.shiftAt (ξ : ℝ) : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume) →ₗᵢ[ℂ] ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

u ↦ f(ξ + u), an isometry of L².

Equations

• WignerFunction.shiftAt ξ = MeasureTheory.Lp.compMeasurePreservingₗᵢ ℂ (fun (u : ℝ) => ξ + u) ⋯

theorem WignerFunction.coeFn_reflectAt (ξ : ℝ) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ↑↑((reflectAt ξ) f) =ᵐ[MeasureTheory.volume] fun (u : ℝ) => ↑↑f (ξ - u)

theorem WignerFunction.coeFn_shiftAt (ξ : ℝ) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ↑↑((shiftAt ξ) f) =ᵐ[MeasureTheory.volume] fun (u : ℝ) => ↑↑f (ξ + u)

theorem WignerFunction.continuous_phase (x : ℝ) : Continuous fun (u : ℝ) => ↑(Real.fourierChar (2 * x * u))

theorem WignerFunction.memLp_top_phase (x : ℝ) : MeasureTheory.MemLp (fun (u : ℝ) => ↑(Real.fourierChar (2 * x * u))) ⊤ MeasureTheory.volume

noncomputable def WignerFunction.phaseLinf (x : ℝ) : ↥(MeasureTheory.Lp ℂ ⊤ MeasureTheory.volume)

The unimodular phase u ↦ e(2xu) as an L^∞ class.

Equations

• WignerFunction.phaseLinf x = MeasureTheory.MemLp.toLp (fun (u : ℝ) => ↑(Real.fourierChar (2 * x * u))) ⋯

theorem WignerFunction.coeFn_phaseLinf (x : ℝ) : ↑↑(phaseLinf x) =ᵐ[MeasureTheory.volume] fun (u : ℝ) => ↑(Real.fourierChar (2 * x * u))

theorem WignerFunction.norm_phaseLinf_le (x : ℝ) : ‖phaseLinf x‖ ≤ 1

noncomputable def WignerFunction.wignerLeft (ξ : ℝ) : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume) →L[ℂ] ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

L_ξ φ = φ̂(ξ − ·).

Equations

• WignerFunction.wignerLeft ξ = (WignerFunction.reflectAt ξ).toContinuousLinearMap ∘SL ↑↑(MeasureTheory.Lp.fourierTransformₗᵢ ℝ ℂ)

noncomputable def WignerFunction.wignerRight (x ξ : ℝ) : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume) →L[ℂ] ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

R_{x,ξ} ψ = e(2x·) ψ̂(ξ + ·).

Equations

• WignerFunction.wignerRight x ξ = HeatSemigroup.potential (WignerFunction.phaseLinf x) ∘SL (WignerFunction.shiftAt ξ).toContinuousLinearMap ∘SL ↑↑(MeasureTheory.Lp.fourierTransformₗᵢ ℝ ℂ)

theorem WignerFunction.coeFn_wignerLeft (ξ : ℝ) (φ : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ↑↑((wignerLeft ξ) φ) =ᵐ[MeasureTheory.volume] fun (u : ℝ) => ↑↑((MeasureTheory.Lp.fourierTransformₗᵢ ℝ ℂ) φ) (ξ - u)

theorem WignerFunction.coeFn_wignerRight (x ξ : ℝ) (ψ : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ↑↑((wignerRight x ξ) ψ) =ᵐ[MeasureTheory.volume] fun (u : ℝ) => ↑(Real.fourierChar (2 * x * u)) * ↑↑((MeasureTheory.Lp.fourierTransformₗᵢ ℝ ℂ) ψ) (ξ + u)

theorem WignerFunction.norm_wignerLeft_apply (ξ : ℝ) (φ : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ‖(wignerLeft ξ) φ‖ = ‖φ‖

theorem WignerFunction.norm_wignerRight_apply_le (x ξ : ℝ) (ψ : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ‖(wignerRight x ξ) ψ‖ ≤ ‖ψ‖

The Wigner function of two L² states

noncomputable def WignerFunction.wignerL2 (φ ψ : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (x ξ : ℝ) : ℂ

★ The Wigner function of two L² states, in the momentum form W(φ, ψ)(x, ξ) = 2 ⟪ φ̂(ξ − ·), e(2x·) ψ̂(ξ + ·) ⟫_{L²}.

Equations

• WignerFunction.wignerL2 φ ψ x ξ = 2 * inner ℂ ((WignerFunction.wignerLeft ξ) φ) ((WignerFunction.wignerRight x ξ) ψ)

theorem WignerFunction.wignerL2_eq_integral (φ ψ : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (x ξ : ℝ) : wignerL2 φ ψ x ξ = 2 * ∫ (u : ℝ), ↑(Real.fourierChar (2 * x * u)) * (↑↑((MeasureTheory.Lp.fourierTransformₗᵢ ℝ ℂ) ψ) (ξ + u) * (starRingEnd ℂ) (↑↑((MeasureTheory.Lp.fourierTransformₗᵢ ℝ ℂ) φ) (ξ - u)))

The integral formula: W(φ, ψ)(x, ξ) = 2 ∫ e(2xu) ψ̂(ξ + u) conj φ̂(ξ − u) du.

theorem WignerFunction.norm_wignerL2_le (φ ψ : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (x ξ : ℝ) : ‖wignerL2 φ ψ x ξ‖ ≤ 2 * ‖φ‖ * ‖ψ‖

★ ‖W(φ, ψ)(x, ξ)‖ ≤ 2 ‖φ‖ ‖ψ‖.

On Schwartz states it is the Wigner function

theorem WignerFunction.wignerL2_toLp (ψ : SchwartzMap ℝ ℂ) (x ξ : ℝ) : wignerL2 (ψ.toLp 2 MeasureTheory.volume) (ψ.toLp 2 MeasureTheory.volume) x ξ = wigner ψ x ξ

★★ On a Schwartz state the L² Wigner function is the Wigner function of Wigner.lean.

The chain rule

theorem WignerFunction.hasDerivAt_wignerL2 {ψ : ℝ → ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)} {ψ' : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)} {t : ℝ} (hψ : HasDerivAt ψ ψ' t) (x ξ : ℝ) : HasDerivAt (fun (s : ℝ) => wignerL2 (ψ s) (ψ s) x ξ) (wignerL2 ψ' (ψ t) x ξ + wignerL2 (ψ t) ψ' x ξ) t

★★ The chain rule for the Wigner function: along an L²-differentiable path, ∂_t W(ψ_t, ψ_t)(x, ξ) = W(ψ̇_t, ψ_t)(x, ξ) + W(ψ_t, ψ̇_t)(x, ξ).

Along the interacting orbit

theorem WignerFunction.hasDerivAt_wignerL2_schrodinger (VL : ↥(MeasureTheory.Lp ℂ ⊤ MeasureTheory.volume)) (f : ↥SchrodingerGroup.freeSymbolOp.domain) (h : SchrodingerGroup.fourierL2.symm ↑f ∈ SchrodingerGroup.freePositionOp.domain) {t : ℝ} (ht : 0 < t) (x ξ : ℝ) : HasDerivAt (fun (s : ℝ) => wignerL2 ((SchrodingerGroup.schrodinger ⋯ VL s) (SchrodingerGroup.fourierL2.symm ↑f)) ((SchrodingerGroup.schrodinger ⋯ VL s) (SchrodingerGroup.fourierL2.symm ↑f)) x ξ) (wignerL2 (-Complex.I • ↑(SchrodingerGroup.freePositionOp.addCLM (HeatSemigroup.potential VL)) ⟨(SchrodingerGroup.schrodinger ⋯ VL t) (SchrodingerGroup.fourierL2.symm ↑f), ⋯⟩) ((SchrodingerGroup.schrodinger ⋯ VL t) (SchrodingerGroup.fourierL2.symm ↑f)) x ξ + wignerL2 ((SchrodingerGroup.schrodinger ⋯ VL t) (SchrodingerGroup.fourierL2.symm ↑f)) (-Complex.I • ↑(SchrodingerGroup.freePositionOp.addCLM (HeatSemigroup.potential VL)) ⟨(SchrodingerGroup.schrodinger ⋯ VL t) (SchrodingerGroup.fourierL2.symm ↑f), ⋯⟩) x ξ) t

★★★ The interacting Wigner equation, operator form. Along the Schrödinger orbit ψ_t = U(t)ψ₀ of a bounded real potential, started in dom H₀, for every t > 0 and every phase-space point,

∂_t W_{ψ_t}(x, ξ) = W(−i(H₀ + V)ψ_t, ψ_t)(x, ξ) + W(ψ_t, −i(H₀ + V)ψ_t)(x, ξ),

with H₀ = freePositionOp acting on the orbit point.