The free half of the interacting Wigner equation on dom H₀

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

For φ, ψ ∈ dom H₀ (the free Hamiltonian's domain in the position representation),

W(−iH₀φ, ψ) + W(φ, −iH₀ψ) = −2πξ · ∂_x W(φ, ψ).

In the momentum form of #167, W(φ, ψ)(x, ξ) = 2 ∫ e(2xu) ψ̂(ξ + u) conj φ̂(ξ − u) du, and H₀ multiplies the transform by 2π²η² (freeSymbolOp). Two facts make the identity algebra:

• the x-dependence is a phase group. e(2xu) = e^{−ix·κ(u)} with κ(u) = −4πu, so x ↦ e(2x·) ψ̂(ξ + ·) is phaseGroup κ x applied to a fixed L² function, and PhaseGenerator.lean's ★★★ hasDerivAt_phaseGroup_apply differentiates it in L² as soon as κ · ψ̂(ξ + ·) ∈ L², which is exactly what ψ ∈ dom H₀ gives (η ψ̂ ∈ L² because |η| ≤ 1 + 2π²η²). Hence ∂_x W = 2 ∫ 4πiu · e(2xu) ψ̂(ξ + u) conj φ̂(ξ − u) du;

• (ξ − u)² − (ξ + u)² = −4ξu, so the two H₀ terms combine to −2πξ times that integrand.

• WignerFunction.wignerKappa, phaseFun_wignerKappa, ★ wignerRight_eq_phaseGroup — the right slot is the phase group of κ(u) = −4πu;

• WignerFunction.memLp_id_mul_of_mem, memLp_shift_mul, memLp_kappa_shift — the domain condition η ψ̂ ∈ L² and its translates;

• ★★ WignerFunction.hasDerivAt_wignerRight, ★★ hasDerivAt_wignerL2_x, deriv_wignerL2_x_eq — the x-derivative of the L² Wigner function exists for ψ ∈ dom H₀, with its integral formula;

• WignerFunction.mem_freeSymbolOp_domain_of_mem, fourier_freePositionOp — H₀ on dom H₀ is the symbol multiplier on the transform;

• WignerFunction.integrable_wignerL2_integrand, wignerL2_add_left, wignerL2_add_right, wignerL2_smul_left, wignerL2_smul_right — the integrand is integrable; W is sesquilinear;

• ★★★ WignerFunction.wignerL2_freePositionOp_add — the free half: W(−iH₀φ, ψ) + W(φ, −iH₀ψ) = −2πξ ∂_x W(φ, ψ) on dom H₀.

Honest scope

• dom H₀ is freePositionOp.domain, the operator-theoretic domain ({ψ : (1 + ξ²) ψ̂ ∈ L²}); no identification with H²(ℝ) is used or needed.
• The potential half W(−iVψ, ψ) + W(ψ, −iVψ) = moyalPot V ψ and the assembled equation are #169, WignerPotential.lean.

References: E. Wigner, Phys. Rev. 40 (1932) 749; WignerL2.lean (#167), PhaseGenerator.lean (hasDerivAt_phaseGroup_apply), FreeHamiltonian.lean (freeSymbolOp, freePositionOp), LinearPMapConj.lean (conjIsometry_apply_of_eq); specs/BACKLOG.md #168, #64.

Sesquilinearity and integrability

theorem WignerFunction.wignerL2_add_left (φ₁ φ₂ ψ : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (x ξ : ℝ) : wignerL2 (φ₁ + φ₂) ψ x ξ = wignerL2 φ₁ ψ x ξ + wignerL2 φ₂ ψ x ξ

theorem WignerFunction.wignerL2_add_right (φ ψ₁ ψ₂ : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (x ξ : ℝ) : wignerL2 φ (ψ₁ + ψ₂) x ξ = wignerL2 φ ψ₁ x ξ + wignerL2 φ ψ₂ x ξ

theorem WignerFunction.wignerL2_smul_left (c : ℂ) (φ ψ : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (x ξ : ℝ) : wignerL2 (c • φ) ψ x ξ = (starRingEnd ℂ) c * wignerL2 φ ψ x ξ

theorem WignerFunction.wignerL2_smul_right (c : ℂ) (φ ψ : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (x ξ : ℝ) : wignerL2 φ (c • ψ) x ξ = c * wignerL2 φ ψ x ξ

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

The integrand of the momentum form is integrable (it is the integrand of an L² inner product).

The right slot is a phase group

noncomputable def WignerFunction.wignerKappa (u : ℝ) : ℝ

The multiplier κ(u) = −4πu, whose phase group e^{−ixκ} is e(2x·).

Equations

• WignerFunction.wignerKappa u = -(4 * Real.pi * u)

theorem WignerFunction.measurable_wignerKappa : Measurable wignerKappa

theorem WignerFunction.phaseFun_wignerKappa (x u : ℝ) : SchrodingerGroup.phaseFun wignerKappa x u = ↑(Real.fourierChar (2 * x * u))

theorem WignerFunction.wignerRight_eq_phaseGroup (x ξ : ℝ) (ψ : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : (wignerRight x ξ) ψ = (SchrodingerGroup.phaseGroup measurable_wignerKappa x) ((shiftAt ξ) ((MeasureTheory.Lp.fourierTransformₗᵢ ℝ ℂ) ψ))

★ The right slot is the phase group of κ applied to the shifted transform.

The domain condition η ψ̂ ∈ L²

theorem WignerFunction.memLp_id_mul_of_mem (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (hf : f ∈ SchrodingerGroup.freeSymbolOp.domain) : MeasureTheory.MemLp (fun (η : ℝ) => ↑η * ↑↑f η) 2 MeasureTheory.volume

(1 + 2π²η²) f ∈ L² gives η f ∈ L².

theorem WignerFunction.memLp_shift_mul (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (hf : f ∈ SchrodingerGroup.freeSymbolOp.domain) (ξ : ℝ) : MeasureTheory.MemLp (fun (u : ℝ) => ↑u * ↑↑f (ξ + u)) 2 MeasureTheory.volume

The translate u ↦ u · f(ξ + u) is in L² for f in the free symbol domain.

theorem WignerFunction.memLp_kappa_shift (ψ : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (hψ : (MeasureTheory.Lp.fourierTransformₗᵢ ℝ ℂ) ψ ∈ SchrodingerGroup.freeSymbolOp.domain) (ξ : ℝ) : MeasureTheory.MemLp (fun (u : ℝ) => ↑(wignerKappa u) * ↑↑((shiftAt ξ) ((MeasureTheory.Lp.fourierTransformₗᵢ ℝ ℂ) ψ)) u) 2 MeasureTheory.volume

κ · ψ̂(ξ + ·) ∈ L² for ψ̂ in the free symbol domain.

The x-derivative

noncomputable def WignerFunction.kappaShift (ψ : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (hψ : (MeasureTheory.Lp.fourierTransformₗᵢ ℝ ℂ) ψ ∈ SchrodingerGroup.freeSymbolOp.domain) (ξ : ℝ) : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

The L² class of u ↦ κ(u) ψ̂(ξ + u).

Equations

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

theorem WignerFunction.coeFn_kappaShift (ψ : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (hψ : (MeasureTheory.Lp.fourierTransformₗᵢ ℝ ℂ) ψ ∈ SchrodingerGroup.freeSymbolOp.domain) (ξ : ℝ) : ↑↑(kappaShift ψ hψ ξ) =ᵐ[MeasureTheory.volume] fun (u : ℝ) => ↑(wignerKappa u) * ↑↑((shiftAt ξ) ((MeasureTheory.Lp.fourierTransformₗᵢ ℝ ℂ) ψ)) u

theorem WignerFunction.hasDerivAt_wignerRight (ξ : ℝ) (ψ : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (hψ : (MeasureTheory.Lp.fourierTransformₗᵢ ℝ ℂ) ψ ∈ SchrodingerGroup.freeSymbolOp.domain) (x : ℝ) : HasDerivAt (fun (x : ℝ) => (wignerRight x ξ) ψ) (-Complex.I • (SchrodingerGroup.phaseGroup measurable_wignerKappa x) (kappaShift ψ hψ ξ)) x

★★ The right slot is differentiable in x for ψ̂ in the free symbol domain, with derivative −i · e(2x·) · κ ψ̂(ξ + ·).

theorem WignerFunction.hasDerivAt_wignerL2_x (φ ψ : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (hψ : (MeasureTheory.Lp.fourierTransformₗᵢ ℝ ℂ) ψ ∈ SchrodingerGroup.freeSymbolOp.domain) (x ξ : ℝ) : HasDerivAt (fun (x : ℝ) => wignerL2 φ ψ x ξ) (2 * inner ℂ ((wignerLeft ξ) φ) (-Complex.I • (SchrodingerGroup.phaseGroup measurable_wignerKappa x) (kappaShift ψ hψ ξ))) x

★★ The L² Wigner function is differentiable in x for ψ ∈ dom H₀.

theorem WignerFunction.deriv_wignerL2_x_eq (φ ψ : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (hψ : (MeasureTheory.Lp.fourierTransformₗᵢ ℝ ℂ) ψ ∈ SchrodingerGroup.freeSymbolOp.domain) (x ξ : ℝ) : deriv (fun (x : ℝ) => wignerL2 φ ψ x ξ) x = 2 * ∫ (u : ℝ), ↑(4 * Real.pi * u) * Complex.I * ↑(Real.fourierChar (2 * x * u)) * (↑↑((MeasureTheory.Lp.fourierTransformₗᵢ ℝ ℂ) ψ) (ξ + u) * (starRingEnd ℂ) (↑↑((MeasureTheory.Lp.fourierTransformₗᵢ ℝ ℂ) φ) (ξ - u)))

The integral formula for ∂_x W: 2 ∫ 4πiu · e(2xu) ψ̂(ξ + u) conj φ̂(ξ − u) du.

H₀ on the transform

theorem WignerFunction.mem_freeSymbolOp_domain_of_mem {ψ : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)} (hψ : ψ ∈ SchrodingerGroup.freePositionOp.domain) : (MeasureTheory.Lp.fourierTransformₗᵢ ℝ ℂ) ψ ∈ SchrodingerGroup.freeSymbolOp.domain

theorem WignerFunction.fourier_freePositionOp {ψ : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)} (hψ : ψ ∈ SchrodingerGroup.freePositionOp.domain) : (MeasureTheory.Lp.fourierTransformₗᵢ ℝ ℂ) (↑SchrodingerGroup.freePositionOp ⟨ψ, hψ⟩) = ↑SchrodingerGroup.freeSymbolOp ⟨(MeasureTheory.Lp.fourierTransformₗᵢ ℝ ℂ) ψ, ⋯⟩

𝓕 (H₀ ψ) = (2π²η²) ψ̂ on dom H₀.

theorem WignerFunction.coeFn_fourier_neg_I_smul_freePositionOp {ψ : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)} (hψ : ψ ∈ SchrodingerGroup.freePositionOp.domain) : ↑↑((MeasureTheory.Lp.fourierTransformₗᵢ ℝ ℂ) (-Complex.I • ↑SchrodingerGroup.freePositionOp ⟨ψ, hψ⟩)) =ᵐ[MeasureTheory.volume] fun (η : ℝ) => -Complex.I * (↑(SchrodingerGroup.freeSymbol η) * ↑↑((MeasureTheory.Lp.fourierTransformₗᵢ ℝ ℂ) ψ) η)

The transform of −iH₀ψ, almost everywhere: −i · 2π²η² · ψ̂(η).

The free half

theorem WignerFunction.wignerL2_freePositionOp_add {φ ψ : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)} (hφ : φ ∈ SchrodingerGroup.freePositionOp.domain) (hψ : ψ ∈ SchrodingerGroup.freePositionOp.domain) (x ξ : ℝ) : wignerL2 (-Complex.I • ↑SchrodingerGroup.freePositionOp ⟨φ, hφ⟩) ψ x ξ + wignerL2 φ (-Complex.I • ↑SchrodingerGroup.freePositionOp ⟨ψ, hψ⟩) x ξ = -(2 * ↑Real.pi * ↑ξ) * deriv (fun (x : ℝ) => wignerL2 φ ψ x ξ) x

★★★ The free half of the interacting Wigner equation: for φ, ψ ∈ dom H₀, W(−iH₀φ, ψ) + W(φ, −iH₀ψ) = −2πξ · ∂_x W(φ, ψ).