English
If f is measure-preserving with respect to μ and equivariant with respect to M, then the image measure map f μ is SMulInvariant under M.
Русский
Если отображение f сохраняет меру μ и совместимо с действием M, то образующая мера map f μ инвариантна относительно M.
LaTeX
$$$(\\forall m,a, f(m\\cdot a) = m\\cdot f(a)) \\land \\text{Measurable}(f) \\Rightarrow \\text{SMulInvariantMeasure } M (\\operatorname{map} f \\mu)$$$
Lean4
@[to_additive]
theorem smulInvariantMeasure_map [SMul M α] [SMul M β] [MeasurableSMul M β] (μ : Measure α) [SMulInvariantMeasure M α μ]
(f : α → β) (hsmul : ∀ (m : M) a, f (m • a) = m • f a) (hf : Measurable f) : SMulInvariantMeasure M β (map f μ)
where
measure_preimage_smul m S
hS :=
calc
map f μ ((m • ·) ⁻¹' S)
_ = μ (f ⁻¹' ((m • ·) ⁻¹' S)) := (map_apply hf <| hS.preimage (measurable_const_smul _))
_ = μ ((m • f ·) ⁻¹' S) := by rw [preimage_preimage]
_ = μ ((f <| m • ·) ⁻¹' S) := by simp_rw [hsmul]
_ = μ ((m • ·) ⁻¹' (f ⁻¹' S)) := by rw [← preimage_preimage]
_ = μ (f ⁻¹' S) := by rw [SMulInvariantMeasure.measure_preimage_smul m (hS.preimage hf)]
_ = map f μ S := (map_apply hf hS).symm
