CorollaryStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A Hamiltonian local flow on a phase domain preserves Lebesgue measure on its flow domain

Statement

Assume the Axiom of Countable Choice where the cited change-of-variables theorem requires it (The Axiom of Countable Choice ( ${A C}_{ω}$ ), A C^1 diffeomorphism satisfies the change-of-variables formula for L^1 functions). Let $n \geq 1$ , let $U$ be a phase domain (A phase domain, its canonical one-form and its standard symplectic two-form), let $H \in C^{2} (U)$ , and let $Φ$ be the local flow of $X_{H} = J \nabla H$ (The Hamiltonian field of a $C^{2}$ function on a phase domain is $J \nabla H$ , and the Poisson bracket is $\sum_{i} (\partial_{q^{i}} f \partial_{p_{i}} g - \partial_{p_{i}} f \partial_{q^{i}} g)$ ). Let $t \in R$ , let $D_{t} : = {z \in U : (t, z) lies in the flow domain}$ be the open domain of $Φ_{t}$ (The flow domain of a C¹ autonomous field is open and the flow is C¹ on it), and let $A \subseteq D_{t}$ be a bounded Borel set with $\overline{A} \subseteq D_{t}$ . Then $A$ and $Φ_{t} (A)$ are Lebesgue measurable with

$λ_{2 n} (Φ_{t} (A)) = λ_{2 n} (A) .$

For a $C^{2}$ time-dependent Hamiltonian $H : T \times U \to R$ and the evolution $E$ of The derivative of the Hamiltonian flow satisfies $Y^{T} J Y = J$ and $\det Y = 1$ , fix $t_{0}, t \in T$ . Its initial-state domain $D_{t, t_{0}} = {z : E (t, t_{0}, z) is defined}$ is open. For every bounded Borel $A \subseteq D_{t, t_{0}}$ with $\overline{A} \subseteq D_{t, t_{0}}$ , $λ_{2 n} (E (t, t_{0}, A)) = λ_{2 n} (A) .$ No completeness or time independence is needed.

Facts & Assumptions

Given: The phase domain $U$ , $H \in C^{2} (U)$ , the local flow $Φ$ of $X_{H}$ , a time $t \in R$ , the open set $D_{t}$ and a bounded Borel set $A$ with $\overline{A} \subseteq D_{t}$ .

[F1]

Flow regularity and time maps as diffeomorphisms (The flow domain of a C¹ autonomous field is open and the flow is C¹ on it, The local flow is a partial one-parameter group: identity, composition and inverse-time laws, The local flow of an autonomous first-order system): the flow domain $Ω$ is open in $R \times U$ and $Φ$ is $C^{1}$ with $\partial_{t} Φ = F (Φ)$ for $F = X_{H}$ ; the partial flow satisfies $Φ (0, a) = a$ , $Φ (s + t, a) = Φ (t, Φ (s, a))$ and $Φ (- t, Φ (t, a)) = a$ wherever the displayed points lie in $Ω$ , so for each $t$ the time- $t$ map $Φ_{t} : D_{t} \to Φ_{t} (D_{t})$ is a bijection with inverse $Φ_{- t}$ , of class $C^{1}$ in both directions: a $C^{1}$ diffeomorphism onto its image.

[F2]

Unit Jacobian determinant (The derivative of the Hamiltonian flow satisfies $Y^{T} J Y = J$ and $\det Y = 1$ ): for $z \in D_{t}$ , $\det D Φ_{t} (z) = 1$ .

[F3]

Change of variables for $L^{1}$ functions under a $C^{1}$ diffeomorphism (A C^1 diffeomorphism satisfies the change-of-variables formula for L^1 functions): for open $V, W \subseteq R^{m}$ and a $C^{1}$ diffeomorphism $T : V \to W$ , $\int_{W} f d λ_{m} = \int_{V} (f \circ T) ∣ \det D T ∣ d λ_{m}$ for $f \in L^{1} (W)$ ; the Lebesgue measure and $σ$ -algebra are those of Lebesgue measurable sets, the family $L (R^{n})$ , and the restricted set function $λ_{n}$ , and Borel sets are those of The Borel sigma-algebra of a topological space.

[F4]

Borel and integrability bookkeeping (A continuous map has Borel preimages of Borel sets, Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line, The image of a compact metric space under a continuous map is compact, and so is the image of any compact subset, The Borel sigma-algebra of a topological space, Assuming countable choice, every Borel subset of $R^{n}$ is Lebesgue measurable, A box in $R^{n}$ with parameters $a_{i} \leq b_{i}$ is Lebesgue measurable of measure $\prod_{i < n} (b_{i} - a_{i})$ , whichever of its faces are included, The integral of a nonnegative simple function, The nonnegative integral agrees with the simple integral on simple functions, Integrable real and complex functions, and their integrals): the continuous inverse gives $Φ_{t} (A) = (Φ_{- t})^{- 1} (A)$ Borel relative to the open image domain, hence Borel in $R^{2 n}$ . Under the assumed Countable Choice, every Borel subset of $R^{2 n}$ is Lebesgue measurable. Boundedness and $\overline{A} \subseteq D_{t}$ make $\overline{A}$ compact; its continuous image $Φ_{t} (\overline{A})$ is compact and bounded. Thus $A$ and $Φ_{t} (A)$ each lie in a finite closed box $[- R, R]^{2 n}$ , whose measure is $(2 R)^{2 n} < \infty$ . Monotonicity of Lebesgue outer measure, restricted to measurable sets, bounds their measures by this value. For either measurable set $E$ , its indicator is simple and $\int ∣ 1_{E} ∣ d λ_{2 n} = λ_{2 n} (E) < \infty$ , by the simple-integral definition and its agreement with the nonnegative integral. Consequently both indicators are in $L^{1}$ .

Proof

technique · direct; write the measures as integrals of indicator functions and apply the change-of-variables theorem with unit Jacobian

1.1F1F2F4

By [F1] the map $Φ_{t} : D_{t} \to Φ_{t} (D_{t})$ is a $C^{1}$ diffeomorphism between open subsets of $R^{2 n}$ , and by [F4] the set $Φ_{t} (A)$ is a bounded Borel set whose indicator is integrable; moreover $∣ \det D Φ_{t} ∣ = 1$ on $D_{t}$ by [F2].

2.1F3step 1.1algebra

Apply [F3] with $T = Φ_{t}$ , $V = D_{t}$ and $f = 1_{Φ_{t} (A)} \in L^{1}$ : since $f \circ T = 1_{A}$ and $∣ \det D T ∣ = 1$ , the identity $\int f d λ_{2 n} = \int (f \circ T) ∣ \det D T ∣ d λ_{2 n}$ reads $λ_{2 n} (Φ_{t} (A)) = \int 1_{A} d λ_{2 n} = λ_{2 n} (A)$ , which is the claim.

3.1F2F3F4step 2.1∎

For the time-dependent case the preceding proposition gives the open domain $D_{t, t_{0}}$ , the $C^{1}$ inverse $E (t_{0}, t, \cdot)$ , and unit determinant for $E (t, t_{0}, \cdot)$ . Thus its image of a Borel $A$ is Borel by the continuous inverse, and the compact closure of $A$ has compact image, so the image indicator is integrable by the same argument as [F4]. Apply [F3] to this fixed-endpoint diffeomorphism and the image indicator as in step 2.1; its pullback is $1_{A}$ and its Jacobian has absolute value $1$ . This proves the stated nonautonomous equality as well as the original autonomous one.

Remarks

The published Liouville volume preservation states the same conclusion for the Liouville form $ω^{n} / n!$ on a symplectic manifold; the present corollary is the chart-level Lebesgue form with an explicit choice-free determinant computation apart from the change-of-variables theorem it cites.
The same equality holds for every Lebesgue-measurable $A \subseteq D_{t}$ , with infinite measures permitted. To justify this extension, let $T = Φ_{t} : D_{t} \to W$ and use the proof of A C^1 diffeomorphism satisfies the change-of-variables formula for L^1 functions, steps 4.1-5.1: a $C^{1}$ diffeomorphism has measurable preimages of Lebesgue-measurable sets, and for any such $E \subseteq W$ it gives $λ_{2 n} (E) = \int_{D_{t}} 1_{E} (T (z)) ∣ \det D T (z) ∣ d z$ , without a finiteness restriction. Apply the preimage measurability assertion first to $T^{- 1} : W \to D_{t}$ and $A$ ; thus $E = T (A)$ is measurable. Apply the displayed identity to this $E$ and use $∣ \det D T ∣ = 1$ to obtain $λ_{2 n} (T (A)) = \int_{D_{t}} 1_{A} = λ_{2 n} (A)$ . The same argument applies to each fixed-endpoint evolution. Countable Choice is retained throughout; exhaustion by Borel sets alone does not establish this completion step.

A Hamiltonian local flow on a phase domain preserves Lebesgue measure on its flow domain

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources