English
If f is invariant under G, then aestronglyMeasurable_on_iff holds for s and t; i.e., invariance transfers measurability between restricted measures.
Русский
Если f инвариантна по G, то aestronglyMeasurable_on_iff переносит измеримость между ограниченными мерами.
LaTeX
$$$$\\text{AEStronglyMeasurable}(f, \\mu|_s) \\iff \\text{AEStronglyMeasurable}(f, \\mu|_t).$$$$
Lean4
@[to_additive]
protected theorem aestronglyMeasurable_on_iff {β : Type*} [TopologicalSpace β] [PseudoMetrizableSpace β]
(hs : IsFundamentalDomain G s μ) (ht : IsFundamentalDomain G t μ) {f : α → β}
(hf : ∀ (g : G) (x), f (g • x) = f x) :
AEStronglyMeasurable f (μ.restrict s) ↔ AEStronglyMeasurable f (μ.restrict t) :=
calc
AEStronglyMeasurable f (μ.restrict s) ↔ AEStronglyMeasurable f (Measure.sum fun g : G => μ.restrict (g • t ∩ s)) :=
by simp only [← ht.restrict_restrict, ht.sum_restrict_of_ac restrict_le_self.absolutelyContinuous]
_ ↔ ∀ g : G, AEStronglyMeasurable f (μ.restrict (g • (g⁻¹ • s ∩ t))) := by
simp only [smul_set_inter, inter_comm, smul_inv_smul, aestronglyMeasurable_sum_measure_iff]
_ ↔ ∀ g : G, AEStronglyMeasurable f (μ.restrict (g⁻¹ • (g⁻¹⁻¹ • s ∩ t))) := inv_surjective.forall
_ ↔ ∀ g : G, AEStronglyMeasurable f (μ.restrict (g⁻¹ • (g • s ∩ t))) := by simp only [inv_inv]
_ ↔ ∀ g : G, AEStronglyMeasurable f (μ.restrict (g • s ∩ t)) :=
by
refine forall_congr' fun g => ?_
have he : MeasurableEmbedding (g⁻¹ • · : α → α) := measurableEmbedding_const_smul _
rw [← image_smul, ← ((measurePreserving_smul g⁻¹ μ).restrict_image_emb he _).aestronglyMeasurable_comp_iff he]
simp only [Function.comp_def, hf]
_ ↔ AEStronglyMeasurable f (μ.restrict t) := by
simp only [← aestronglyMeasurable_sum_measure_iff, ← hs.restrict_restrict,
hs.sum_restrict_of_ac restrict_le_self.absolutelyContinuous]
