A finite cyclic-invariance criterion

On the zero-sum hyperplane, reversal of all coordinates and reversal of the initial coordinates generate cyclic shifts.

Reference: J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter VIII (Vervaat's transformation and the uniform law of the minimum time); L. Chaumont, Excursion normalisée, méandre et pont pour les processus de Lévy stables, Bull. Sci. Math. 121 (1997), 377–403.

theorem BGW.StableTrees.map_cyclic_of_reverse_of_prefix_reverse (M : ℕ) (μ : MeasureTheory.Measure (Fin (M + 1) → ℝ)) (hsum : ∀ᵐ (x : Fin (M + 1) → ℝ) ∂μ, ∑ i : Fin (M + 1), x i = 0) (hrev : MeasureTheory.Measure.map (fun (x : Fin (M + 1) → ℝ) (i : Fin (M + 1)) => x i.rev) μ = μ) (hprefix : MeasureTheory.Measure.map (fun (x : Fin M → ℝ) (i : Fin M) => x i.rev) (MeasureTheory.Measure.map (fun (x : Fin (M + 1) → ℝ) (i : Fin M) => x i.castSucc) μ) = MeasureTheory.Measure.map (fun (x : Fin (M + 1) → ℝ) (i : Fin M) => x i.castSucc) μ) (k : Fin (M + 1)) : MeasureTheory.Measure.map (fun (x : Fin (M + 1) → ℝ) (i : Fin (M + 1)) => x (i + k)) μ = μ

Full reversal and reversal of the strict prefix imply cyclic invariance for a measure supported on zero-sum vectors.