chore(data/indicator_function): a few more simp lemmas (#5293)

* drop `indicator_of_support_subset` in favor of the new `indicator_eq_self`;

* add a few more lemmas: `indicator_apply_eq_self`,
 `indicator_apply_eq_zero`, `indicator_eq_zero`, `indicator_eq_zero'`

Author: urkud

src/data/indicator_function.lean

@@ -63,20 +63,23 @@ lemma eq_on_indicator : eq_on (indicator s f) f s := λ x hx, indicator_of_mem h
 lemma support_indicator : function.support (s.indicator f) ⊆ s :=
 λ x hx, hx.imp_symm (λ h, indicator_of_not_mem h f)
 
-lemma indicator_of_support_subset (h : support f ⊆ s) : s.indicator f = f :=
-begin
-  ext x,
-  by_cases hx : f x = 0,
-  { rw hx,
-    by_contradiction H,
-    have := mem_of_indicator_ne_zero H,
-    rw [indicator_of_mem this f, hx] at H,
-    exact H rfl },
-  { exact indicator_of_mem (h hx) f }
-end
+@[simp] lemma indicator_apply_eq_self : s.indicator f a = f a ↔ (a ∉ s → f a = 0) :=
+ite_eq_left_iff.trans $ by rw [@eq_comm _ (f a)]
+
+@[simp] lemma indicator_eq_self : s.indicator f = f ↔ support f ⊆ s :=
+by simp only [funext_iff, subset_def, mem_support, indicator_apply_eq_self, not_imp_comm]
 
 @[simp] lemma indicator_support : (support f).indicator f = f :=
-indicator_of_support_subset $ subset.refl _
+indicator_eq_self.2 $ subset.refl _
+
+@[simp] lemma indicator_apply_eq_zero : indicator s f a = 0 ↔ (a ∈ s → f a = 0) :=
+ite_eq_right_iff
+
+@[simp] lemma indicator_eq_zero : indicator s f = (λ x, 0) ↔ disjoint (support f) s :=
+by simp only [funext_iff, indicator_apply_eq_zero, set.disjoint_left, mem_support, not_imp_not]
+
+@[simp] lemma indicator_eq_zero' : indicator s f = 0 ↔ disjoint (support f) s :=
+indicator_eq_zero
 
 @[simp] lemma indicator_range_comp {ι : Sort*} (f : ι → α) (g : α → β) :
   indicator (range f) g ∘ f = g ∘ f :=
@@ -86,22 +89,23 @@ lemma indicator_congr (h : ∀ a ∈ s, f a = g a) : indicator s f = indicator s
 funext $ λx, by { simp only [indicator], split_ifs, { exact h _ h_1 }, refl }
 
 @[simp] lemma indicator_univ (f : α → β) : indicator (univ : set α) f = f :=
-funext $ λx, indicator_of_mem (mem_univ _) f
+indicator_eq_self.2 $ subset_univ _
 
 @[simp] lemma indicator_empty (f : α → β) : indicator (∅ : set α) f = λa, 0 :=
-funext $ λx, indicator_of_not_mem (not_mem_empty _) f
+indicator_eq_zero.2 $ disjoint_empty _
 
 variable (β)
 
 @[simp] lemma indicator_zero (s : set α) : indicator s (λx, (0:β)) = λx, (0:β) :=
-funext $ λx, by { simp only [indicator], split_ifs, refl, refl }
+indicator_eq_zero.2 $ by simp only [support_zero, empty_disjoint]
 
 @[simp] lemma indicator_zero' {s : set α} : s.indicator (0 : α → β) = 0 :=
 indicator_zero β s
 
 variable {β}
 
-lemma indicator_indicator (s t : set α) (f : α → β) : indicator s (indicator t f) = indicator (s ∩ t) f :=
+lemma indicator_indicator (s t : set α) (f : α → β) :
+  indicator s (indicator t f) = indicator (s ∩ t) f :=
 funext $ λx, by { simp only [indicator], split_ifs, repeat {simp * at * {contextual := tt}} }
 
 lemma comp_indicator (h : β → γ) (f : α → β) {s : set α} {x : α} :

src/data/set/function.lean

@@ -580,6 +580,10 @@ by simp [piecewise, hi]
 lemma piecewise_eq_of_not_mem {i : α} (hi : i ∉ s) : s.piecewise f g i = g i :=
 by simp [piecewise, hi]
 
+lemma piecewise_singleton (x : α) [Π y, decidable (y ∈ ({x} : set α))] [decidable_eq α]
+  (f g : α → β) : piecewise {x} f g = function.update g x (f x) :=
+by { ext y, by_cases hy : y = x, { subst y, simp }, { simp [hy] } }
+
 lemma piecewise_eq_on (f g : α → β) : eq_on (s.piecewise f g) f s :=
 λ _, piecewise_eq_of_mem _ _ _
 

src/measure_theory/interval_integral.lean

@@ -461,8 +461,7 @@ lemma integral_eq_integral_of_support_subset {f : α → E} {a b} (h : function.
 begin
   by_cases hfm : measurable f,
   { cases le_total a b with hab hab,
-    { rw [integral_of_le hab, ← integral_indicator hfm is_measurable_Ioc,
-        indicator_of_support_subset h] },
+    { rw [integral_of_le hab, ← integral_indicator hfm is_measurable_Ioc, indicator_eq_self.2 h] },
     { rw [Ioc_eq_empty hab, subset_empty_iff, function.support_eq_empty_iff] at h,
       simp [h] } },
   { rw [integral_non_measurable hfm, measure_theory.integral_non_measurable hfm] },

src/measure_theory/set_integral.lean

@@ -470,7 +470,7 @@ lemma continuous.integrable_of_compact_closure_support
   (hfc : is_compact (closure $ support f)) :
   integrable f μ :=
 begin
-  rw [← indicator_of_support_subset (@subset_closure _ _ (support f)),
+  rw [← indicator_eq_self.2 (@subset_closure _ _ (support f)),
     integrable_indicator_iff hf.measurable is_closed_closure.is_measurable],
   exact hf.integrable_on_compact hfc
 end