feat(measure_theory/group): add measurable_set.const_smul (#10025)

Partially based on lemmas from #2819.

Co-authored-by: Alex J. Best <alex.j.best@gmail.com>

src/algebra/pointwise.lean

@@ -621,6 +621,14 @@ lemma zero_smul_set [has_zero α] [has_zero β] [smul_with_zero α β] {s : set
   (0 : α) • s = (0 : set β) :=
 by simp only [← image_smul, image_eta, zero_smul, h.image_const, singleton_zero]
 
+lemma zero_smul_subset [has_zero α] [has_zero β] [smul_with_zero α β] (s : set β) :
+  (0 : α) • s ⊆ 0 :=
+image_subset_iff.2 $ λ x _, zero_smul α x
+
+lemma subsingleton_zero_smul_set [has_zero α] [has_zero β] [smul_with_zero α β] (s : set β) :
+  ((0 : α) • s).subsingleton :=
+subsingleton_singleton.mono (zero_smul_subset s)
+
 section group
 variables [group α] [mul_action α β]
 

src/measure_theory/group/pointwise.lean

@@ -0,0 +1,44 @@
+/-
+Copyright (c) 2021 Yury G. Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury G. Kudryashov, Alex J. Best
+-/
+import measure_theory.group.arithmetic
+
+/-!
+# Pointwise set operations on `measurable_set`s
+
+In this file we prove several versions of the following fact: if `s` is a measurable set, then so is
+`a • s`. Note that the pointwise product of two measurable sets need not be measurable, so there is
+no `measurable_set.mul` etc.
+-/
+
+open_locale pointwise
+open set
+
+@[to_additive]
+lemma measurable_set.const_smul {G α : Type*} [group G] [mul_action G α] [measurable_space G]
+  [measurable_space α] [has_measurable_smul G α] {s : set α} (hs : measurable_set s) (a : G) :
+  measurable_set (a • s) :=
+begin
+  rw ← preimage_smul_inv,
+  exact measurable_const_smul _ hs
+end
+
+lemma measurable_set.const_smul_of_ne_zero {G₀ α : Type*} [group_with_zero G₀] [mul_action G₀ α]
+  [measurable_space G₀] [measurable_space α] [has_measurable_smul G₀ α] {s : set α}
+  (hs : measurable_set s) {a : G₀} (ha : a ≠ 0) :
+  measurable_set (a • s) :=
+begin
+  rw ← preimage_smul_inv₀ ha,
+  exact measurable_const_smul _ hs
+end
+
+lemma measurable_set.const_smul₀ {G₀ α : Type*} [group_with_zero G₀] [has_zero α]
+  [mul_action_with_zero G₀ α] [measurable_space G₀] [measurable_space α] [has_measurable_smul G₀ α]
+  [measurable_singleton_class α] {s : set α} (hs : measurable_set s) (a : G₀) :
+  measurable_set (a • s) :=
+begin
+  rcases eq_or_ne a 0 with (rfl|ha),
+  exacts [(subsingleton_zero_smul_set s).measurable_set, hs.const_smul_of_ne_zero ha]
+end

src/measure_theory/measurable_space_def.lean

@@ -252,6 +252,9 @@ lemma measurable_set.insert {s : set α} (hs : measurable_set s) (a : α) :
   else insert_diff_self_of_not_mem ha ▸ h.diff (measurable_set_singleton _),
   λ h, h.insert a⟩
 
+lemma set.subsingleton.measurable_set {s : set α} (hs : s.subsingleton) : measurable_set s :=
+hs.induction_on measurable_set.empty measurable_set_singleton
+
 lemma set.finite.measurable_set {s : set α} (hs : finite s) : measurable_set s :=
 finite.induction_on hs measurable_set.empty $ λ a s ha hsf hsm, hsm.insert _