Anti-normally ordered moments scale under the Husimi stretch

Proved

HighEntropyLimit.husimi_stretch_moments

by Lucas · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

mathematical-physicsquantum-mechanics

Let $\lambda>1$ , let $Q_1:\mathbb C\to\mathbb R$ , and let $Q_\lambda(\alpha) = \lambda^{-1}Q_1(\alpha/\sqrt\lambda)$ . For all $n,m\in\mathbb N$ ,

\int_{\mathbb C}\alpha^n(\alpha^*)^m\,Q_\lambda(\alpha)\,d^2\alpha = (\sqrt\lambda)^{n+m}\int_{\mathbb C}\beta^n(\beta^*)^m\,Q_1(\beta)\,d^2\beta.

Through Eq. (23) this says that the stretch rescales every anti-normally ordered moment $\langle a^n(a^\dagger)^m\rangle$ by $(\sqrt\lambda)^{n+m}$ .

Preamble

import Mathlib
import Definitions.Def_HighEntropyLimit_phase_space_stretch
open MeasureTheory ComplexConjugate

Formal statement

namespace HighEntropyLimit
theorem husimi_stretch_moments (lam : ℝ) (hlam : 1 < lam) (Q : ℂ → ℝ) (n m : ℕ) :
    ∫ α : ℂ, α ^ n * (conj α) ^ m * (husimiStretch lam Q α : ℂ) =
      ((Real.sqrt lam : ℝ) : ℂ) ^ (n + m) * ∫ β : ℂ, β ^ n * (conj β) ^ m * (Q β : ℂ) := by
  sorry
end HighEntropyLimit

Source

Carcassi, Landini, Aidala, Classical mechanics as the high-entropy limit of quantum mechanics, arXiv:2411.00972v3 (1 Feb 2026), https://arxiv.org/abs/2411.00972, p. 9, Eqs. (24),(25)

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph