English
If for all non-identity group elements g the translates g·s are aedisjoint from s, and each translation is quasi-measure-preserving, then the family {g·s} is pairwise aedisjoint.
Русский
Если для всех неидентичных элементов группы g·s раздельно по AED, и каждое такое преобразование тождественно сохраняет меру до квазимера, то множество пар г·s попарно AED-несовместны.
LaTeX
$$Pairwise (AEDisjoint μ on (fun g: G => g · s))$$
Lean4
@[to_additive]
theorem pairwise_aedisjoint_of_aedisjoint_forall_ne_one {G α : Type*} [Group G] [MulAction G α] {_ : MeasurableSpace α}
{μ : Measure α} {s : Set α} (h_ae_disjoint : ∀ g ≠ (1 : G), AEDisjoint μ (g • s) s)
(h_qmp : ∀ g : G, QuasiMeasurePreserving (g • ·) μ μ) : Pairwise (AEDisjoint μ on fun g : G => g • s) :=
by
intro g₁ g₂ hg
let g := g₂⁻¹ * g₁
replace hg : g ≠ 1 := by
rw [Ne, inv_mul_eq_one]
exact hg.symm
have : (g₂⁻¹ • ·) ⁻¹' (g • s ∩ s) = g₁ • s ∩ g₂ • s := by
rw [preimage_eq_iff_eq_image (MulAction.bijective g₂⁻¹), image_smul, smul_set_inter, smul_smul, smul_smul,
inv_mul_cancel, one_smul]
change μ (g₁ • s ∩ g₂ • s) = 0
exact this ▸ (h_qmp g₂⁻¹).preimage_null (h_ae_disjoint g hg)
