Moments scale under the pure stretching map

Proved

HighEntropyLimit.pure_stretch_moments

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

mathematical-physicsquantum-mechanics

Let $\lambda > 1$ , let $\rho$ be a function on phase space $\mathbb R^2$ , and let $T\rho(z) = \lambda^{-1}\rho(z/\sqrt\lambda)$ . For all $n,m\in\mathbb N$ ,

\int x^n p^m\,(T\rho)(x,p)\,dx\,dp = (\sqrt\lambda)^{n+m}\int x^n p^m\,\rho(x,p)\,dx\,dp.

Formalization Note No integrability is assumed. If one side does not converge, neither does the other, and Lean assigns both the value $0$ .

Preamble

import Mathlib
import Definitions.Def_HighEntropyLimit_phase_space_stretch
open MeasureTheory

Formal statement

namespace HighEntropyLimit
theorem pure_stretch_moments (lam : ℝ) (hlam : 1 < lam) (ρ : ℝ × ℝ → ℝ) (n m : ℕ) :
    ∫ z, z.1 ^ n * z.2 ^ m * pureStretch lam ρ z =
      Real.sqrt lam ^ (n + m) * ∫ z, z.1 ^ n * z.2 ^ m * ρ z := 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. 8, Eq. (18)

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