feat(*): add more lemmas about set.piecewise (#6862)

Author: urkud

src/algebra/group/pi.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Patrick Massot
 -/
 import data.pi
+import data.set.function
 import tactic.pi_instances
 import algebra.group.defs
 import algebra.group.hom
@@ -202,3 +203,25 @@ lemma pi.single_mul [Π i, monoid_with_zero $ f i] (i : I) (x y : f i) :
 (mul_hom.single f i).map_mul x y
 
 end single
+
+section piecewise
+
+@[to_additive]
+lemma set.piecewise_mul [Π i, has_mul (f i)] (s : set I) [Π i, decidable (i ∈ s)]
+  (f₁ f₂ g₁ g₂ : Π i, f i) :
+  s.piecewise (f₁ * f₂) (g₁ * g₂) = s.piecewise f₁ g₁ * s.piecewise f₂ g₂ :=
+s.piecewise_op₂ _ _ _ _ (λ _, (*))
+
+@[to_additive]
+lemma pi.piecewise_inv [Π i, has_inv (f i)] (s : set I) [Π i, decidable (i ∈ s)]
+  (f₁ g₁ : Π i, f i) :
+  s.piecewise (f₁⁻¹) (g₁⁻¹) = (s.piecewise f₁ g₁)⁻¹ :=
+s.piecewise_op f₁ g₁ (λ _ x, x⁻¹)
+
+@[to_additive]
+lemma pi.piecewise_div [Π i, has_div (f i)] (s : set I) [Π i, decidable (i ∈ s)]
+  (f₁ f₂ g₁ g₂ : Π i, f i) :
+  s.piecewise (f₁ / f₂) (g₁ / g₂) = s.piecewise f₁ g₁ / s.piecewise f₂ g₂ :=
+s.piecewise_op₂ _ _ _ _ (λ _, (/))
+
+end piecewise

src/data/indicator_function.lean

@@ -138,7 +138,7 @@ by rw [← mul_indicator_mul_indicator, mul_indicator_mul_support]
 
 @[to_additive] lemma comp_mul_indicator (h : M → β) (f : α → M) {s : set α} {x : α} :
   h (s.mul_indicator f x) = s.piecewise (h ∘ f) (const α (h 1)) x :=
-s.comp_piecewise h
+s.apply_piecewise _ _ (λ _, h)
 
 @[to_additive] lemma mul_indicator_comp_right {s : set α} (f : β → α) {g : α → M} {x : β} :
   mul_indicator (f ⁻¹' s) (g ∘ f) x = mul_indicator s g (f x) :=

src/data/set/function.lean

@@ -666,6 +666,22 @@ lemma piecewise_eq_on (f g : α → β) : eq_on (s.piecewise f g) f s :=
 lemma piecewise_eq_on_compl (f g : α → β) : eq_on (s.piecewise f g) g sᶜ :=
 λ _, piecewise_eq_of_not_mem _ _ _
 
+lemma piecewise_le {δ : α → Type*} [Π i, preorder (δ i)] {s : set α} [Π j, decidable (j ∈ s)]
+  {f₁ f₂ g : Π i, δ i} (h₁ : ∀ i ∈ s, f₁ i ≤ g i) (h₂ : ∀ i ∉ s, f₂ i ≤ g i) :
+  s.piecewise f₁ f₂ ≤ g :=
+λ i, if h : i ∈ s then by simp * else by simp *
+
+lemma le_piecewise {δ : α → Type*} [Π i, preorder (δ i)] {s : set α} [Π j, decidable (j ∈ s)]
+  {f₁ f₂ g : Π i, δ i} (h₁ : ∀ i ∈ s, g i ≤ f₁ i) (h₂ : ∀ i ∉ s, g i ≤ f₂ i) :
+  g ≤ s.piecewise f₁ f₂ :=
+@piecewise_le α (λ i, order_dual (δ i)) _ s _ _ _ _ h₁ h₂
+
+lemma piecewise_le_piecewise {δ : α → Type*} [Π i, preorder (δ i)] {s : set α}
+  [Π j, decidable (j ∈ s)] {f₁ f₂ g₁ g₂ : Π i, δ i} (h₁ : ∀ i ∈ s, f₁ i ≤ g₁ i)
+  (h₂ : ∀ i ∉ s, f₂ i ≤ g₂ i) :
+  s.piecewise f₁ f₂ ≤ s.piecewise g₁ g₂ :=
+by apply piecewise_le; intros; simp *
+
 @[simp, priority 990]
 lemma piecewise_insert_of_ne {i j : α} (h : i ≠ j) [∀i, decidable (i ∈ insert j s)] :
   (insert j s).piecewise f g i = s.piecewise f g i :=
@@ -710,10 +726,25 @@ lemma piecewise_preimage (f g : α → β) (t) :
   s.piecewise f g ⁻¹' t = s.ite (f ⁻¹' t) (g ⁻¹' t) :=
 ext $ λ x, by by_cases x ∈ s; simp [*, set.ite]
 
-lemma comp_piecewise (h : β → γ) {f g : α → β} {x : α} :
-  h (s.piecewise f g x) = s.piecewise (h ∘ f) (h ∘ g) x :=
+lemma apply_piecewise {δ' : α → Sort*} (h : Π i, δ i → δ' i) {x : α} :
+  h x (s.piecewise f g x) = s.piecewise (λ x, h x (f x)) (λ x, h x (g x)) x :=
+by by_cases hx : x ∈ s; simp [hx]
+
+lemma apply_piecewise₂ {δ' δ'' : α → Sort*} (f' g' : Π i, δ' i) (h : Π i, δ i → δ' i → δ'' i)
+  {x : α} :
+  h x (s.piecewise f g x) (s.piecewise f' g' x) =
+    s.piecewise (λ x, h x (f x) (f' x)) (λ x, h x (g x) (g' x)) x :=
 by by_cases hx : x ∈ s; simp [hx]
 
+lemma piecewise_op {δ' : α → Sort*} (h : Π i, δ i → δ' i) :
+  s.piecewise (λ x, h x (f x)) (λ x, h x (g x)) = λ x, h x (s.piecewise f g x) :=
+funext $ λ x, (apply_piecewise _ _ _ _).symm
+
+lemma piecewise_op₂ {δ' δ'' : α → Sort*} (f' g' : Π i, δ' i) (h : Π i, δ i → δ' i → δ'' i) :
+  s.piecewise (λ x, h x (f x) (f' x)) (λ x, h x (g x) (g' x)) =
+    λ x, h x (s.piecewise f g x) (s.piecewise f' g' x) :=
+funext $ λ x, (apply_piecewise₂ _ _ _ _ _ _).symm
+
 @[simp] lemma piecewise_same : s.piecewise f f = f :=
 by { ext x, by_cases hx : x ∈ s; simp [hx] }
 

src/data/set/intervals/pi.lean

@@ -31,6 +31,17 @@ ext $ λ y, by simp [pi.le_def]
 @[simp] lemma pi_univ_Icc : pi univ (λ i, Icc (x i) (y i)) = Icc x y :=
 ext $ λ y, by simp [pi.le_def, forall_and_distrib]
 
+lemma piecewise_mem_Icc {s : set ι} [Π j, decidable (j ∈ s)] {f₁ f₂ g₁ g₂ : Π i, α i}
+  (h₁ : ∀ i ∈ s, f₁ i ∈ Icc (g₁ i) (g₂ i)) (h₂ : ∀ i ∉ s, f₂ i ∈ Icc (g₁ i) (g₂ i)) :
+  s.piecewise f₁ f₂ ∈ Icc g₁ g₂ :=
+⟨le_piecewise (λ i hi, (h₁ i hi).1) (λ i hi, (h₂ i hi).1),
+  piecewise_le (λ i hi, (h₁ i hi).2) (λ i hi, (h₂ i hi).2)⟩
+
+lemma piecewise_mem_Icc' {s : set ι} [Π j, decidable (j ∈ s)] {f₁ f₂ g₁ g₂ : Π i, α i}
+  (h₁ : f₁ ∈ Icc g₁ g₂) (h₂ : f₂ ∈ Icc g₁ g₂) :
+  s.piecewise f₁ f₂ ∈ Icc g₁ g₂ :=
+piecewise_mem_Icc (λ i hi, ⟨h₁.1 _, h₁.2 _⟩) (λ i hi, ⟨h₂.1 _, h₂.2 _⟩)
+
 section nonempty
 
 variable [nonempty ι]