feat(algebra/pointwise): pointwise scalar-multiplication lemmas (#1925)

* feat(algebra/pointwise): more lemmas about scaling sets

- rename `smul_set` to `scale_set` for disambiguation
- define `scale_set_action`, which subsumes `one_smul_set`
- additional lemmas lemmas

* fix(analysis/convex): refactor proofs for `scale_set`

* feat(algebra/pointwise): re-organise file

- subsume `pointwise_mul_action`

* feat(algebra/pointwise): remove `pointwise_mul_action`

- subsumed by `smul_set_action` with left-regular action.

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

Author: jlpaca

src/algebra/pointwise.lean

@@ -189,6 +189,48 @@ def pointwise_add_fintype [has_add α] [decidable_eq α] (s t : set α) [hs : fi
 
 attribute [to_additive] set.pointwise_mul_fintype
 
+/-- Pointwise scalar multiplication by a set of scalars. -/
+def pointwise_smul [has_scalar α β] : has_scalar (set α) (set β) :=
+  ⟨λ s t, { x | ∃ a ∈ s, ∃ y ∈ t, x  = a • y }⟩
+
+/-- Scaling a set: multiplying every element by a scalar. -/
+def smul_set [has_scalar α β] : has_scalar α (set β) :=
+  ⟨λ a s, { x | ∃ y ∈ s, x = a • y }⟩
+
+local attribute [instance] pointwise_smul smul_set
+
+lemma mem_smul_set [has_scalar α β] (a : α) (s : set β) (x : β) :
+  x ∈ a • s ↔ ∃ y ∈ s, x = a • y := iff.rfl
+
+lemma smul_set_eq_image [has_scalar α β] (a : α) (s : set β) :
+  a • s = (λ x, a • x) '' s :=
+set.ext $ λ x, iff.intro
+  (λ ⟨_, hy₁, hy₂⟩, ⟨_, hy₁, hy₂.symm⟩)
+  (λ ⟨_, hy₁, hy₂⟩, ⟨_, hy₁, hy₂.symm⟩)
+
+lemma smul_set_eq_pointwise_smul_singleton [has_scalar α β]
+  (a : α) (s : set β) : a • s = ({a} : set α) • s :=
+set.ext $ λ x, iff.intro
+  (λ ⟨_, h⟩, ⟨a, mem_singleton _, _, h⟩)
+  (λ ⟨_, h, y, hy, hx⟩, ⟨_, hy, by {
+    rw mem_singleton_iff at h; rwa h at hx }⟩)
+
+lemma smul_mem_smul_set [has_scalar α β]
+  (a : α) {s : set β} {y : β} (hy : y ∈ s) : a • y ∈ a • s :=
+by rw mem_smul_set; use [y, hy]
+
+lemma smul_set_union [has_scalar α β] (a : α) (s t : set β) :
+  a • (s ∪ t) = a • s ∪ a • t :=
+by simp only [smul_set_eq_image, image_union]
+
+@[simp] lemma smul_set_empty [has_scalar α β] (a : α) :
+  a • (∅ : set β) = ∅ :=
+by rw [smul_set_eq_image, image_empty]
+
+lemma smul_set_mono [has_scalar α β]
+  (a : α) {s t : set β} (h : s ⊆ t) : a • s ⊆ a • t :=
+by { rw [smul_set_eq_image, smul_set_eq_image], exact image_subset _ h }
+
 section monoid
 
 def pointwise_mul_semiring [monoid α] : semiring (set α) :=
@@ -220,6 +262,19 @@ from @additive.add_comm_monoid _ set.comm_monoid
 
 attribute [to_additive set.add_comm_monoid] set.comm_monoid
 
+/-- A multiplicative action of a monoid on a type β gives also a
+ multiplicative action on the subsets of β. -/
+def smul_set_action [monoid α] [mul_action α β] :
+  mul_action α (set β) :=
+{ smul     := λ a s, a • s,
+  mul_smul := λ a b s, set.ext $ λ x, iff.intro
+    (λ ⟨_, hy, _⟩, ⟨b • _, smul_mem_smul_set _ hy, by rwa ←mul_smul⟩)
+    (λ ⟨_, hy, _⟩, let ⟨_, hz, h⟩ := (mem_smul_set _ _ _).2 hy in
+      ⟨_, hz, by rwa [mul_smul, ←h]⟩),
+  one_smul := λ b, set.ext $ λ x, iff.intro
+    (λ ⟨_, _, h⟩, by { rw [one_smul] at h; rwa h })
+    (λ h, ⟨_, h, by rw one_smul⟩) }
+
 section is_mul_hom
 open is_mul_hom
 
@@ -253,56 +308,8 @@ lemma pointwise_mul_image_is_semiring_hom : is_semiring_hom (image f) :=
   map_add := image_union _,
   map_mul := image_pointwise_mul _ }
 
-local attribute [instance] singleton.is_monoid_hom
-
-def pointwise_mul_action : mul_action α (set α) :=
-{ smul := λ a s, ({a} : set α) * s,
-  one_smul := one_mul,
-  mul_smul := λ _ _ _, show {_} * _ = _,
-    by { erw is_monoid_hom.map_mul (singleton : α → set α), apply mul_assoc } }
-
-local attribute [instance] pointwise_mul_action
-
-lemma mem_smul_set {a : α} {s : set α} {x : α} :
-  x ∈ a • s ↔ ∃ y ∈ s, x = a * y :=
-by { erw mem_pointwise_mul, simp }
-
-lemma smul_set_eq_image {a : α} {s : set α} :
-  a • s = (λ b, a * b) '' s :=
-set.ext $ λ x,
-begin
-  simp only [mem_smul_set, exists_prop, mem_image],
-  apply exists_congr,
-  intro y,
-  apply and_congr iff.rfl,
-  split; exact eq.symm
-end
-
 end monoid
 
-/-- Pointwise scalar multiplication by a set of scalars. -/
-def pointwise_smul [has_scalar α β] : has_scalar (set α) (set β) :=
-  ⟨λ s t, { x | ∃ a ∈ s, ∃ y ∈ t, x  = a • y }⟩
-
-/-- Scaling a set: multiplying every element by a scalar. -/
-def smul_set [has_scalar α β] : has_scalar α (set β) :=
-  ⟨λ a s, (λ y, a • y) '' s⟩
-
-local attribute [instance] pointwise_smul smul_set
-
-lemma smul_set_eq_pointwise_smul_singleton [has_scalar α β]
-  (a : α) (s : set β) : a • s = ({a} : set α) • s :=
-set.ext $ λ x, iff.intro
-  (λ ⟨_, ht, hx⟩, ⟨a, mem_singleton _, _, ht, hx.symm⟩)
-  (λ ⟨a', ha', y, hy, hx⟩, ⟨_, hy, by {
-    rw mem_singleton_iff at ha'; rw ha' at hx; exact hx.symm }⟩)
-
-/-- A set scaled by 1 is itself. -/
-lemma one_smul_set [monoid α] [mul_action α β] (s : set β) : (1 : α) • s = s :=
-set.ext $ λ x, iff.intro
-  (λ ⟨y, hy, hx⟩, by { rw ←hx, show (1 : α) • y ∈ s, by rwa one_smul })
-  (λ hx, ⟨x, hx, show (1 : α) • x = x, by rwa one_smul⟩)
-
 end set
 
 section
@@ -318,8 +325,19 @@ containing 0 in the semimodule. -/
 lemma zero_smul_set [semiring α] [add_comm_monoid β] [semimodule α β]
   {s : set β} (h : s ≠ ∅) : (0 : α) • s = {(0 : β)} :=
 set.ext $ λ x, iff.intro
-(λ ⟨y, hy, hx⟩, mem_singleton_iff.mpr (by { rw ←hx; exact zero_smul α y}))
+(λ ⟨_, _, hx⟩, mem_singleton_iff.mpr (by { rwa [hx, zero_smul] }))
 (λ hx, let ⟨_, hs⟩ := set.ne_empty_iff_exists_mem.mp h in
-  ⟨_, hs, show (0 : α) • _ = x, by { rw mem_singleton_iff at hx; rw [hx, zero_smul] }⟩)
+  ⟨_, hs, by { rw mem_singleton_iff at hx; rw [hx, zero_smul] }⟩)
+
+lemma mem_inv_smul_set_iff [field α] [mul_action α β]
+  {a : α} (ha : a ≠ 0) (A : set β) (x : β) : x ∈ a⁻¹ • A ↔ a • x ∈ A :=
+iff.intro
+  (λ ⟨y, hy, h⟩, by rwa [h, ←mul_smul, mul_inv_cancel ha, one_smul])
+  (λ h, ⟨_, h, by rw [←mul_smul, inv_mul_cancel ha, one_smul]⟩)
+
+lemma mem_smul_set_iff_inv_smul_mem [field α] [mul_action α β]
+  {a : α} (ha : a ≠ 0) (A : set β) (x : β) : x ∈ a • A ↔ a⁻¹ • x ∈ A :=
+by conv_lhs { rw ←(division_ring.inv_inv ha) };
+   exact (mem_inv_smul_set_iff (inv_ne_zero ha) _ _)
 
 end

src/analysis/convex/basic.lean

@@ -223,7 +223,10 @@ lemma convex.neg_preimage (hs : convex s) : convex ((λ z, -z) ⁻¹' s) :=
 hs.is_linear_preimage is_linear_map.is_linear_map_neg
 
 lemma convex.smul (c : ℝ) (hs : convex s) : convex (c • s) :=
-hs.is_linear_image (is_linear_map.is_linear_map_smul c)
+begin
+  rw smul_set_eq_image,
+  exact hs.is_linear_image (is_linear_map.is_linear_map_smul c)
+end
 
 lemma convex.smul_preimage (c : ℝ) (hs : convex s) : convex ((λ z, c • z) ⁻¹' s) :=
 hs.is_linear_preimage (is_linear_map.is_linear_map_smul c)
@@ -245,7 +248,7 @@ end
 lemma convex.affinity (hs : convex s) (z : E) (c : ℝ) : convex ((λx, z + c • x) '' s) :=
 begin
   convert (hs.smul c).translate z using 1,
-  erw [← image_comp]
+  erw [smul_set_eq_image, ←image_comp]
 end
 
 lemma convex_real_iff {s : set ℝ} :

src/analysis/convex/topology.lean

@@ -79,11 +79,17 @@ convex_iff_pointwise_add_subset.mpr $ λ a b ha hb hab,
   or.elim (classical.em (a = 0))
   (λ heq,
     have hne : b ≠ 0, by { rw [heq, zero_add] at hab, rw hab, exact one_ne_zero },
-    is_open_pointwise_add_left ((is_open_map_smul_of_ne_zero hne _) is_open_interior))
+    (smul_set_eq_image b (interior s)).symm ▸
+    (is_open_pointwise_add_left ((is_open_map_smul_of_ne_zero hne _) is_open_interior)))
   (λ hne,
-    is_open_pointwise_add_right ((is_open_map_smul_of_ne_zero hne _) is_open_interior)),
+    (smul_set_eq_image a (interior s)).symm ▸
+    (is_open_pointwise_add_right ((is_open_map_smul_of_ne_zero hne _) is_open_interior))),
   (subset_interior_iff_subset_of_open h).mpr $ subset.trans
-    (by { apply pointwise_add_subset_add; exact image_subset _ interior_subset })
+    begin
+      apply pointwise_add_subset_add;
+      rw [smul_set_eq_image, smul_set_eq_image];
+      exact image_subset _ interior_subset
+    end
     (convex_iff_pointwise_add_subset.mp hs ha hb hab)
 
 /-- In a topological vector space, the closure of a convex set is convex. -/