The potential half, and the interacting Wigner equation

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

Along the Schrödinger orbit ψ_t = U(t)ψ₀ of a bounded real potential V, started in dom H₀, for every t > 0 and every phase-space point,

∂_t W_{ψ_t}(x, ξ) = −2πξ · ∂_x W_{ψ_t}(x, ξ) + moyalPotL2 V ψ_t ψ_t (x, ξ),

the Wigner (Moyal) evolution equation for H = 2π²ξ² + V(x) on L². #167 gave ∂_t W = W(−i(H₀+V)ψ, ψ) + W(ψ, −i(H₀+V)ψ) and #168 the H₀ half; this file does the V half.

The one real step is Plancherel on L². The L² Wigner function of #167 is defined in the momentum form, W(φ, ψ)(x, ξ) = 2 ⟪ φ̂(ξ − ·), e(2x·) ψ̂(ξ + ·) ⟫, because H₀ is a multiplier there; a potential is a multiplier in the position form, W_pos(φ, ψ)(x, ξ) = 2 ⟪ φ(x − ·), e(−2ξ·) ψ(x + ·) ⟫. The two forms are the same function (★★★ wignerPos_eq_wignerL2): both are continuous sesquilinear forms on L² × L², and they agree on Schwartz states — where both are the cross Wigner function wigner₂ of MoyalBracket.lean, by the Plancherel symmetry ★★ wigner₂_fourier, the cross form of Wigner.lean's wigner_fourier — and Schwartz states are dense (SchwartzMap.denseRange_toLpCLM). No Fourier transform of a translate or a modulation is computed on L².

• WignerFunction.posRight, ★ wignerPos, wignerPos_eq_integral, integrable_wignerPos_integrand — the position form, an inner product of continuous linear images of the states, like the momentum form;
• WignerFunction.wignerL2_eq_wignerPos_fourier — the momentum form is the position form of the transforms at (ξ, −x);
• WignerFunction.wignerPos_toLp, ★★ wigner₂_fourier, wignerL2_toLp₂ — on Schwartz states both forms are wigner₂ (first slot conjugated);
• ★★★ WignerFunction.wignerPos_eq_wignerL2 — the L² Plancherel identity for the Wigner function;
• ★ WignerFunction.moyalPotL2, ★★ moyalPotL2_toLp — the potential term on L², equal to moyalPot on Schwartz states;
• ★★★ WignerFunction.wignerPos_potential_add, ★★★ wignerL2_potential_add, wignerL2_potential_add_toLp — the potential half: W(−iVφ, ψ) + W(φ, −iVψ) = moyalPotL2 V φ ψ;
• ★★★ WignerFunction.hasDerivAt_wignerL2_schrodinger_eq — the interacting Wigner equation along the orbit, assembled from #167, #168 and the potential half.

Honest scope

• V enters as a bounded class VL ∈ L^∞ almost everywhere equal to the real function V (the hypothesis form of SchrodingerGroup.norm_schrodinger_apply); moyalPotL2 is stated with the real V, as moyalPot is. No regularity of V beyond boundedness is used — the classical limit of moyalPot (MoyalBracket.lean) is where V''' enters, and it is unchanged.
• The equation is for W_{ψ_t} = wignerL2 ψ_t ψ_t with ψ_t ∈ L² (the orbit leaves Schwartz space); for a Schwartz initial state the t = 0 value is wigner ψ₀ (wignerL2_toLp, #167).
• ∂_x W is the derivative of #168, which exists because ψ_t ∈ dom H₀ (schrodinger_mem_freePositionOp_domain).
• One dimension, as the whole Wigner line.

References: E. Wigner, Phys. Rev. 40 (1932) 749; J. E. Moyal, Proc. Cambridge Philos. Soc. 45 (1949) 99 §7; WignerL2.lean (#167), WignerFree.lean (#168), MoyalBracket.lean (moyalPot, wigner₂), Wigner.lean (wigner_fourier), PhaseGeneratorDomain.lean (hasDerivAt_schrodinger_orbit); specs/BACKLOG.md #169, #64.

The position form

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

P_{x,ξ} ψ = e(−2ξ·) ψ(x + ·).

Equations

• WignerFunction.posRight x ξ = HeatSemigroup.potential (WignerFunction.phaseLinf (-ξ)) ∘SL (WignerFunction.shiftAt x).toContinuousLinearMap

theorem WignerFunction.coeFn_posRight (x ξ : ℝ) (ψ : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ↑↑((posRight x ξ) ψ) =ᵐ[MeasureTheory.volume] fun (v : ℝ) => ↑(Real.fourierChar (-(2 * v * ξ))) * ↑↑ψ (x + v)

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

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

Equations

• WignerFunction.wignerPos φ ψ x ξ = 2 * inner ℂ ((WignerFunction.reflectAt x) φ) ((WignerFunction.posRight x ξ) ψ)

theorem WignerFunction.wignerPos_eq_integral (φ ψ : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (x ξ : ℝ) : wignerPos φ ψ x ξ = 2 * ∫ (v : ℝ), ↑(Real.fourierChar (-(2 * v * ξ))) * (↑↑ψ (x + v) * (starRingEnd ℂ) (↑↑φ (x - v)))

The integral formula: W_pos(φ, ψ)(x, ξ) = 2 ∫ e(−2vξ) ψ(x + v) conj φ(x − v) dv.

theorem WignerFunction.integrable_wignerPos_integrand (φ ψ : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (x ξ : ℝ) : MeasureTheory.Integrable (fun (v : ℝ) => ↑(Real.fourierChar (-(2 * v * ξ))) * (↑↑ψ (x + v) * (starRingEnd ℂ) (↑↑φ (x - v)))) MeasureTheory.volume

theorem WignerFunction.wignerL2_eq_wignerPos_fourier (φ ψ : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (x ξ : ℝ) : wignerL2 φ ψ x ξ = wignerPos ((MeasureTheory.Lp.fourierTransformₗᵢ ℝ ℂ) φ) ((MeasureTheory.Lp.fourierTransformₗᵢ ℝ ℂ) ψ) ξ (-x)

The momentum form is the position form of the transforms, with (x, ξ) ↦ (ξ, −x): W(φ, ψ)(x, ξ) = W_pos(φ̂, ψ̂)(ξ, −x).

On Schwartz states both forms are the cross Wigner function

theorem WignerFunction.wignerPos_toLp (φ ψ : SchwartzMap ℝ ℂ) (x ξ : ℝ) : wignerPos (φ.toLp 2 MeasureTheory.volume) (ψ.toLp 2 MeasureTheory.volume) x ξ = wigner₂ ψ φ x ξ

On Schwartz states the position form is the cross Wigner function of MoyalBracket.lean, with the slots in inner-product order (the first slot conjugated).

theorem WignerFunction.wigner₂_fourier (φ ψ : SchwartzMap ℝ ℂ) (x ξ : ℝ) : wigner₂ (FourierTransform.fourier φ) (FourierTransform.fourier ψ) ξ (-x) = wigner₂ φ ψ x ξ

★★ The Plancherel symmetry of the cross Wigner function: W(𝓕φ, 𝓕ψ)(ξ, −x) = W(φ, ψ)(x, ξ) on Schwartz states — the cross form of wigner_fourier.

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

On Schwartz states the momentum form is the cross Wigner function too (first slot conjugated).

The L² Plancherel identity

theorem WignerFunction.continuous_wignerPos (x ξ : ℝ) : Continuous fun (q : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume) × ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) => wignerPos q.1 q.2 x ξ

theorem WignerFunction.continuous_wignerL2 (x ξ : ℝ) : Continuous fun (q : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume) × ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) => wignerL2 q.1 q.2 x ξ

theorem WignerFunction.wignerPos_eq_wignerL2 (φ ψ : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (x ξ : ℝ) : wignerPos φ ψ x ξ = wignerL2 φ ψ x ξ

★★★ The L² Plancherel identity for the Wigner function: the position form and the momentum form agree on all of L² × L². Both are continuous sesquilinear forms; they agree on Schwartz states (wignerPos_toLp, wignerL2_toLp₂), which are dense.

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

The integral formula of the momentum form, in position variables.

The potential term on L²

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

★ The potential term of the Wigner equation on L², for a real potential V: the position integral against the symmetric difference V(x + v) − V(x − v). It is MoyalBracket.lean's moyalPot in the variable y = 2v (moyalPotL2_toLp), extended to L² states and to two slots (the first conjugated).

Equations

• WignerFunction.moyalPotL2 V φ ψ x ξ = 2 * ∫ (v : ℝ), ↑(Real.fourierChar (-(2 * v * ξ))) * (-Complex.I * ↑(V (x + v) - V (x - v)) * (↑↑ψ (x + v) * (starRingEnd ℂ) (↑↑φ (x - v))))

theorem WignerFunction.moyalPotL2_toLp (V : ℝ → ℝ) (ψ : SchwartzMap ℝ ℂ) (x ξ : ℝ) : moyalPotL2 V (ψ.toLp 2 MeasureTheory.volume) (ψ.toLp 2 MeasureTheory.volume) x ξ = moyalPot V ψ x ξ

★★ On a Schwartz state, moyalPotL2 is moyalPot.

theorem WignerFunction.coeFn_neg_I_smul_potential {VL : ↥(MeasureTheory.Lp ℂ ⊤ MeasureTheory.volume)} {V : ℝ → ℝ} (hVL : ↑↑VL =ᵐ[MeasureTheory.volume] fun (y : ℝ) => ↑(V y)) (φ : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ↑↑(-Complex.I • (HeatSemigroup.potential VL) φ) =ᵐ[MeasureTheory.volume] fun (y : ℝ) => -Complex.I * (↑(V y) * ↑↑φ y)

(−i V φ)(y) = −i V(y) φ(y) almost everywhere, for VL almost everywhere the real V.

The potential half

theorem WignerFunction.wignerPos_potential_add {VL : ↥(MeasureTheory.Lp ℂ ⊤ MeasureTheory.volume)} {V : ℝ → ℝ} (hVL : ↑↑VL =ᵐ[MeasureTheory.volume] fun (y : ℝ) => ↑(V y)) (φ ψ : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (x ξ : ℝ) : wignerPos (-Complex.I • (HeatSemigroup.potential VL) φ) ψ x ξ + wignerPos φ (-Complex.I • (HeatSemigroup.potential VL) ψ) x ξ = moyalPotL2 V φ ψ x ξ

★★★ The potential half of the interacting Wigner equation, position form: for a bounded potential VL almost everywhere equal to the real V, W_pos(−iVφ, ψ) + W_pos(φ, −iVψ) = moyalPotL2 V φ ψ. Pointwise under the position integral: conj(−i V(x−v)) + (−i V(x+v)) = −i (V(x+v) − V(x−v)) because V is real.

theorem WignerFunction.wignerL2_potential_add {VL : ↥(MeasureTheory.Lp ℂ ⊤ MeasureTheory.volume)} {V : ℝ → ℝ} (hVL : ↑↑VL =ᵐ[MeasureTheory.volume] fun (y : ℝ) => ↑(V y)) (φ ψ : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (x ξ : ℝ) : wignerL2 (-Complex.I • (HeatSemigroup.potential VL) φ) ψ x ξ + wignerL2 φ (-Complex.I • (HeatSemigroup.potential VL) ψ) x ξ = moyalPotL2 V φ ψ x ξ

★★★ The potential half, momentum form — the form the orbit theorem of #167 produces — via the L² Plancherel identity: W(−iVφ, ψ) + W(φ, −iVψ) = moyalPotL2 V φ ψ.

theorem WignerFunction.wignerL2_potential_add_toLp {VL : ↥(MeasureTheory.Lp ℂ ⊤ MeasureTheory.volume)} {V : ℝ → ℝ} (hVL : ↑↑VL =ᵐ[MeasureTheory.volume] fun (y : ℝ) => ↑(V y)) (ψ : SchwartzMap ℝ ℂ) (x ξ : ℝ) : wignerL2 (-Complex.I • (HeatSemigroup.potential VL) (ψ.toLp 2 MeasureTheory.volume)) (ψ.toLp 2 MeasureTheory.volume) x ξ + wignerL2 (ψ.toLp 2 MeasureTheory.volume) (-Complex.I • (HeatSemigroup.potential VL) (ψ.toLp 2 MeasureTheory.volume)) x ξ = moyalPot V ψ x ξ

The potential half on a Schwartz state, with MoyalBracket.lean's moyalPot on the right: W(−iVψ, ψ) + W(ψ, −iVψ) = moyalPot V ψ.

The interacting Wigner equation

theorem WignerFunction.hasDerivAt_wignerL2_schrodinger_eq (VL : ↥(MeasureTheory.Lp ℂ ⊤ MeasureTheory.volume)) {V : ℝ → ℝ} (hVL : ↑↑VL =ᵐ[MeasureTheory.volume] fun (y : ℝ) => ↑(V y)) (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 ξ) (-(2 * ↑Real.pi * ↑ξ) * deriv (fun (x : ℝ) => wignerL2 ((SchrodingerGroup.schrodinger ⋯ VL t) (SchrodingerGroup.fourierL2.symm ↑f)) ((SchrodingerGroup.schrodinger ⋯ VL t) (SchrodingerGroup.fourierL2.symm ↑f)) x ξ) x + moyalPotL2 V ((SchrodingerGroup.schrodinger ⋯ VL t) (SchrodingerGroup.fourierL2.symm ↑f)) ((SchrodingerGroup.schrodinger ⋯ VL t) (SchrodingerGroup.fourierL2.symm ↑f)) x ξ) t

★★★ The interacting Wigner equation. Along the Schrödinger orbit ψ_t = U(t)ψ₀ of a bounded potential VL almost everywhere equal to the real V, started in dom H₀, for every t > 0 and every phase-space point (x, ξ),

∂_t W_{ψ_t}(x, ξ) = −2πξ · ∂_x W_{ψ_t}(x, ξ) + moyalPotL2 V ψ_t ψ_t (x, ξ).

The free transport is #168's half, the potential term is wignerL2_potential_add, and the left-hand side is #167's ∂_t W = W(−i(H₀+V)ψ, ψ) + W(ψ, −i(H₀+V)ψ) split by sesquilinearity.