Invariant twists of an invariant measure are measure-preserving

Category: 1-Mathlib (CSD-free upstream candidate).

Let a group G with a left-invariant probability measure λ act measurably on X, let μ be a measure on X preserved by every act g, and let φ : X → G be a measurable invariant parameter: φ (act g y) = φ y. Then the twist

y ↦ act (φ y) y

— "rotate each point by a group element that depends only on its orbit" — preserves μ.

This is the measure-theoretic content of "a fibrewise rotation by a fibre-constant angle preserves a fibrewise-invariant measure" without ever disintegrating μ along the orbits. The proof is four lines of Tonelli: insert ∫ dλ(g) (a probability), use μ-invariance to replace y by act g y inside, use the invariance of φ and the action law to turn the integrand into f (act (φ y * g) y), absorb φ y by the left-invariance of λ, swap the integrals back and use μ-invariance once more.

Typical instance (the reason the lemma exists here): a torus acting on a Kähler manifold by its Hamiltonian T-action, μ the Liouville measure, φ any measurable function of the moment map. The time-1 map of a Hamiltonian whose flow moves each point only along its torus orbit — by an angle depending on the conserved quantities — is such a twist.

Provenance

Staged as upstream Mathlib material; no CsdLean4-namespace content. Not found in Mathlib (2026-09-01): MeasurePreserving.skew_product covers product spaces with a fibre map that depends on the base point, which is the special case X = B × F, act trivial on B.

theorem MeasureTheory.MeasurePreserving.twist_of_invariant {G : Type u_1} {X : Type u_2} [MeasurableSpace G] [MeasurableSpace X] [Group G] [MeasurableMul₂ G] (haar : Measure G) [IsProbabilityMeasure haar] [haar.IsMulLeftInvariant] {μ : Measure X} [SFinite μ] {act : G → X → X} (hact : Measurable (Function.uncurry act)) (hcomp : ∀ (a b : G) (y : X), act a (act b y) = act (a * b) y) (hinv : ∀ (g : G), MeasurePreserving (act g) μ μ) {φ : X → G} (hφ : Measurable φ) (hφinv : ∀ (g : G) (y : X), φ (act g y) = φ y) : MeasurePreserving (fun (y : X) => act (φ y) y) μ μ

Invariant twists preserve an invariant measure. If every act g preserves μ, λ is a left-invariant probability measure on G, and φ : X → G is measurable and constant on orbits, then y ↦ act (φ y) y preserves μ. The action is only asked to be a measurable map G × X → X satisfying the composition law act a (act b y) = act (a * b) y; no MulAction instance is needed.

theorem MeasureTheory.MeasurePreserving.vadd_twist_of_invariant {G : Type u_1} {X : Type u_2} [MeasurableSpace G] [MeasurableSpace X] [AddGroup G] [MeasurableAdd₂ G] (addHaar : Measure G) [IsProbabilityMeasure addHaar] [addHaar.IsAddLeftInvariant] {μ : Measure X} [SFinite μ] {act : G → X → X} (hact : Measurable (Function.uncurry act)) (hcomp : ∀ (a b : G) (y : X), act a (act b y) = act (a + b) y) (hneg : ∀ (g : G), MeasurePreserving (act g) μ μ) {φ : X → G} (hφ : Measurable φ) (hφinv : ∀ (g : G) (y : X), φ (act g y) = φ y) : MeasurePreserving (fun (y : X) => act (φ y) y) μ μ

Invariant twists preserve an invariant measure (additive group). If every act g preserves μ, λ is a left-invariant probability measure on G, and φ : X → G is measurable and constant on orbits, then y ↦ act (φ y) y preserves μ.