feat(data/equiv/local_equiv): define piecewise and disjoint_union (#6700)

Also change some lemmas to use `set.ite`.

Author: urkud

src/data/equiv/local_equiv.lean

@@ -156,6 +156,11 @@ protected def symm : local_equiv β α :=
 
 instance : has_coe_to_fun (local_equiv α β) := ⟨_, local_equiv.to_fun⟩
 
+/-- See Note [custom simps projection] -/
+def simps.inv_fun (e : local_equiv α β) : β → α := e.symm
+
+initialize_simps_projections local_equiv (to_fun → apply, inv_fun → symm_apply)
+
 @[simp, mfld_simps] theorem coe_mk (f : α → β) (g s t ml mr il ir) :
   (local_equiv.mk f g s t ml mr il ir : α → β) = f := rfl
 
@@ -200,6 +205,97 @@ protected def to_equiv : equiv (e.source) (e.target) :=
 
 lemma image_source_eq_target : e '' e.source = e.target := e.bij_on.image_eq
 
+/-- We say that `t : set β` is an image of `s : set α` under a local equivalence if
+any of the following equivalent conditions hold:
+
+* `e '' (e.source ∩ s) = e.target ∩ t`;
+* `e.source ∩ e ⁻¹ t = e.source ∩ s`;
+* `∀ x ∈ e.source, e x ∈ t ↔ x ∈ s` (this one is used in the definition).
+-/
+def is_image (s : set α) (t : set β) : Prop := ∀ ⦃x⦄, x ∈ e.source → (e x ∈ t ↔ x ∈ s)
+
+namespace is_image
+
+variables {e} {s : set α} {t : set β} {x : α} {y : β}
+
+lemma apply_mem_iff (h : e.is_image s t) (hx : x ∈ e.source) : e x ∈ t ↔ x ∈ s := h hx
+
+lemma symm_apply_mem_iff (h : e.is_image s t) : ∀ ⦃y⦄, y ∈ e.target → (e.symm y ∈ s ↔ y ∈ t) :=
+by { rw [← e.image_source_eq_target, ball_image_iff], intros x hx, rw [e.left_inv hx, h hx] }
+
+protected lemma symm (h : e.is_image s t) : e.symm.is_image t s := h.symm_apply_mem_iff
+
+@[simp] lemma symm_iff : e.symm.is_image t s ↔ e.is_image s t := ⟨λ h, h.symm, λ h, h.symm⟩
+
+protected lemma maps_to (h : e.is_image s t) : maps_to e (e.source ∩ s) (e.target ∩ t) :=
+λ x hx, ⟨e.maps_to hx.1, (h hx.1).2 hx.2⟩
+
+lemma symm_maps_to (h : e.is_image s t) : maps_to e.symm (e.target ∩ t) (e.source ∩ s) :=
+h.symm.maps_to
+
+/-- Restrict a `local_equiv` to a pair of corresponding sets. -/
+@[simps] def restr (h : e.is_image s t) : local_equiv α β :=
+{ to_fun := e,
+  inv_fun := e.symm,
+  source := e.source ∩ s,
+  target := e.target ∩ t,
+  map_source' := h.maps_to,
+  map_target' := h.symm_maps_to,
+  left_inv' := e.left_inv_on.mono (inter_subset_left _ _),
+  right_inv' := e.right_inv_on.mono (inter_subset_left _ _) }
+
+lemma image_eq (h : e.is_image s t) : e '' (e.source ∩ s) = e.target ∩ t :=
+h.restr.image_source_eq_target
+
+lemma symm_image_eq (h : e.is_image s t) : e.symm '' (e.target ∩ t) = e.source ∩ s :=
+h.symm.image_eq
+
+lemma iff_preimage_eq : e.is_image s t ↔ e.source ∩ e ⁻¹' t = e.source ∩ s :=
+by simp only [is_image, set.ext_iff, mem_inter_eq, and.congr_right_iff, mem_preimage]
+
+alias iff_preimage_eq ↔ local_equiv.is_image.preimage_eq local_equiv.is_image.of_preimage_eq
+
+lemma iff_symm_preimage_eq : e.is_image s t ↔ e.target ∩ e.symm ⁻¹' s = e.target ∩ t :=
+symm_iff.symm.trans iff_preimage_eq
+
+alias iff_symm_preimage_eq ↔ local_equiv.is_image.symm_preimage_eq
+  local_equiv.is_image.of_symm_preimage_eq
+
+lemma of_image_eq (h : e '' (e.source ∩ s) = e.target ∩ t) : e.is_image s t :=
+of_symm_preimage_eq $ eq.trans (of_symm_preimage_eq rfl).image_eq.symm h
+
+lemma of_symm_image_eq (h : e.symm '' (e.target ∩ t) = e.source ∩ s) : e.is_image s t :=
+of_preimage_eq $ eq.trans (of_preimage_eq rfl).symm_image_eq.symm h
+
+protected lemma compl (h : e.is_image s t) : e.is_image sᶜ tᶜ :=
+λ x hx, not_congr (h hx)
+
+protected lemma inter {s' t'} (h : e.is_image s t) (h' : e.is_image s' t') :
+  e.is_image (s ∩ s') (t ∩ t') :=
+λ x hx, and_congr (h hx) (h' hx)
+
+protected lemma union {s' t'} (h : e.is_image s t) (h' : e.is_image s' t') :
+  e.is_image (s ∪ s') (t ∪ t') :=
+λ x hx, or_congr (h hx) (h' hx)
+
+protected lemma diff {s' t'} (h : e.is_image s t) (h' : e.is_image s' t') :
+  e.is_image (s \ s') (t \ t') :=
+h.inter h'.compl
+
+lemma left_inv_on_piecewise {e' : local_equiv α β} [∀ i, decidable (i ∈ s)] [∀ i, decidable (i ∈ t)]
+  (h : e.is_image s t) (h' : e'.is_image s t) :
+  left_inv_on (t.piecewise e.symm e'.symm) (s.piecewise e e') (s.ite e.source e'.source) :=
+begin
+  rintro x (⟨he, hs⟩|⟨he, hs : x ∉ s⟩),
+  { rw [piecewise_eq_of_mem _ _ _ hs, piecewise_eq_of_mem _ _ _ ((h he).2 hs), e.left_inv he], },
+  { rw [piecewise_eq_of_not_mem _ _ _ hs, piecewise_eq_of_not_mem _ _ _ ((h'.compl he).2 hs),
+      e'.left_inv he] }
+end
+
+end is_image
+
+lemma is_image_source_target : e.is_image e.source e.target := λ x hx, by simp [hx]
+
 lemma image_source_inter_eq' (s : set α) :
   e '' (e.source ∩ s) = e.target ∩ e.symm ⁻¹' s :=
 by rw [inter_comm, e.left_inv_on.image_inter', image_source_eq_target, inter_comm]
@@ -257,20 +353,7 @@ end
 
 /-- Restricting a local equivalence to e.source ∩ s -/
 protected def restr (s : set α) : local_equiv α β :=
-{ to_fun  := e,
-  inv_fun := e.symm,
-  source  := e.source ∩ s,
-  target  := e.target ∩ e.symm⁻¹' s,
-  map_source'  := λx hx, begin
-    simp only with mfld_simps at hx,
-    simp only [hx] with mfld_simps,
-  end,
-  map_target' := λy hy, begin
-    simp only with mfld_simps at hy,
-    simp only [hy] with mfld_simps,
-  end,
-  left_inv'  := λx hx, e.left_inv hx.1,
-  right_inv' := λy hy, e.right_inv hy.1 }
+(@is_image.of_symm_preimage_eq α β e s _ rfl).restr
 
 @[simp, mfld_simps] lemma restr_coe (s : set α) : (e.restr s : α → β) = e := rfl
 @[simp, mfld_simps] lemma restr_coe_symm (s : set α) : ((e.restr s).symm : β → α) = e.symm := rfl
@@ -520,6 +603,62 @@ by ext x; simp [ext_iff]; tauto
 
 end prod
 
+/-- Combine two `local_equiv`s using `set.piecewise`. The source of the new `local_equiv` is
+`s.ite e.source e'.source = e.source ∩ s ∪ e'.source \ s`, and similarly for target.  The function
+sends `e.source ∩ s` to `e.target ∩ t` using `e` and `e'.source \ s` to `e'.target \ t` using `e'`,
+and similarly for the inverse function. The definition assumes `e.is_image s t` and
+`e'.is_image s t`. -/
+@[simps] def piecewise (e e' : local_equiv α β) (s : set α) (t : set β)
+  [∀ x, decidable (x ∈ s)] [∀ y, decidable (y ∈ t)] (H : e.is_image s t) (H' : e'.is_image s t) :
+  local_equiv α β :=
+{ to_fun := s.piecewise e e',
+  inv_fun := t.piecewise e.symm e'.symm,
+  source := s.ite e.source e'.source,
+  target := t.ite e.target e'.target,
+  map_source' := H.maps_to.piecewise_ite H'.compl.maps_to,
+  map_target' := H.symm.maps_to.piecewise_ite H'.symm.compl.maps_to,
+  left_inv' := H.left_inv_on_piecewise H',
+  right_inv' := H.symm.left_inv_on_piecewise H'.symm }
+
+lemma symm_piecewise (e e' : local_equiv α β) {s : set α} {t : set β}
+  [∀ x, decidable (x ∈ s)] [∀ y, decidable (y ∈ t)]
+  (H : e.is_image s t) (H' : e'.is_image s t) :
+  (e.piecewise e' s t H H').symm = e.symm.piecewise e'.symm t s H.symm H'.symm :=
+rfl
+
+/-- Combine two `local_equiv`s with disjoint sources and disjoint targets. We do not reuse
+`local_equiv.piecewise` here to provide better formulas for `source` and `target`. -/
+@[simps] def disjoint_union (e e' : local_equiv α β) (hs : disjoint e.source e'.source)
+  (ht : disjoint e.target e'.target) [∀ x, decidable (x ∈ e.source)]
+  [∀ y, decidable (y ∈ e.target)] :
+  local_equiv α β :=
+{ to_fun := e.source.piecewise e e',
+  inv_fun := e.target.piecewise e.symm e'.symm,
+  source := e.source ∪ e'.source,
+  target := e.target ∪ e'.target,
+  map_source' := λ x,
+    have x ∈ e'.source → x ∉ e.source, from λ h' h, hs ⟨h, h'⟩,
+    by rintro (he|he'); simp *,
+  map_target' := λ y,
+    have y ∈ e'.target → y ∉ e.target, from λ h' h, ht ⟨h, h'⟩,
+    by rintro (he|he'); simp *,
+  left_inv' := λ x,
+    begin
+      rintro (he|he'),
+      { simp * },
+      { have : x ∉ e.source ∧ e' x ∉ e.target,
+          from ⟨λ h, hs ⟨h, he'⟩, λ h, ht ⟨h, e'.map_source he'⟩⟩,
+        simp * }
+    end,
+  right_inv' := λ y,
+    begin
+      rintro (he|he'),
+      { simp * },
+      { have : y ∉ e.target ∧ e'.symm y ∉ e.source,
+          from ⟨λ h, ht ⟨h, he'⟩, λ h, hs ⟨h, e'.map_target he'⟩⟩,
+        simp * }
+    end }
+
 section pi
 
 variables {ι : Type*} {αi βi : ι → Type*} (ei : Π i, local_equiv (αi i) (βi i))

src/data/indicator_function.lean

@@ -129,12 +129,12 @@ begin
 end
 
 lemma indicator_preimage (s : set α) (f : α → β) (B : set β) :
-  (indicator s f)⁻¹' B = s ∩ f ⁻¹' B ∪ sᶜ ∩ (λa:α, (0:β)) ⁻¹' B :=
+  (indicator s f)⁻¹' B = s.ite (f ⁻¹' B) (0 ⁻¹' B) :=
 piecewise_preimage s f 0 B
 
 lemma indicator_preimage_of_not_mem (s : set α) (f : α → β) {t : set β} (ht : (0:β) ∉ t) :
-  (indicator s f)⁻¹' t = s ∩ f ⁻¹' t :=
-by simp [indicator_preimage, set.preimage_const_of_not_mem ht]
+  (indicator s f)⁻¹' t = f ⁻¹' t ∩ s :=
+by simp [indicator_preimage, pi.zero_def, set.preimage_const_of_not_mem ht]
 
 lemma mem_range_indicator {r : β} {s : set α} {f : α → β} :
   r ∈ range (indicator s f) ↔ (r = 0 ∧ s ≠ univ) ∨ (r ∈ f '' s) :=

src/data/set/basic.lean

@@ -1046,6 +1046,12 @@ by simp [set.ite]
 @[simp] lemma ite_univ (s s' : set α) : set.ite univ s s' = s :=
 by simp [set.ite]
 
+@[simp] lemma ite_empty_left (t s : set α) : t.ite ∅ s = s \ t :=
+by simp [set.ite]
+
+@[simp] lemma ite_empty_right (t s : set α) : t.ite s ∅ = s ∩ t :=
+by simp [set.ite]
+
 lemma ite_mono (t : set α) {s₁ s₁' s₂ s₂' : set α} (h : s₁ ⊆ s₂) (h' : s₁' ⊆ s₂') :
   t.ite s₁ s₁' ⊆ t.ite s₂ s₂' :=
 union_subset_union (inter_subset_inter_left _ h) (inter_subset_inter_left _ h')

src/data/set/function.lean

@@ -679,9 +679,36 @@ funext $ λ x, if hx : x ∈ s then by simp [hx] else by simp [hx]
   (range f).piecewise g₁ g₂ ∘ f = g₁ ∘ f :=
 comp_eq_of_eq_on_range $ piecewise_eq_on _ _ _
 
+theorem maps_to.piecewise_ite {s s₁ s₂ : set α} {t t₁ t₂ : set β} {f₁ f₂ : α → β}
+  [∀ i, decidable (i ∈ s)]
+  (h₁ : maps_to f₁ (s₁ ∩ s) (t₁ ∩ t)) (h₂ : maps_to f₂ (s₂ ∩ sᶜ) (t₂ ∩ tᶜ)) :
+  maps_to (s.piecewise f₁ f₂) (s.ite s₁ s₂) (t.ite t₁ t₂) :=
+begin
+  refine (h₁.congr _).union_union (h₂.congr _),
+  exacts [(piecewise_eq_on s f₁ f₂).symm.mono (inter_subset_right _ _),
+    (piecewise_eq_on_compl s f₁ f₂).symm.mono (inter_subset_right _ _)]
+end
+
+theorem eq_on_piecewise {f f' g : α → β} {t} :
+  eq_on (s.piecewise f f') g t ↔ eq_on f g (t ∩ s) ∧ eq_on f' g (t ∩ sᶜ) :=
+begin
+  simp only [eq_on, ← forall_and_distrib],
+  refine forall_congr (λ a, _), by_cases a ∈ s; simp *
+end
+
+theorem eq_on.piecewise_ite' {f f' g : α → β} {t t'} (h : eq_on f g (t ∩ s))
+  (h' : eq_on f' g (t' ∩ sᶜ)) :
+  eq_on (s.piecewise f f') g (s.ite t t') :=
+by simp [eq_on_piecewise, *]
+
+theorem eq_on.piecewise_ite {f f' g : α → β} {t t'} (h : eq_on f g t)
+  (h' : eq_on f' g t') :
+  eq_on (s.piecewise f f') g (s.ite t t') :=
+(h.mono (inter_subset_left _ _)).piecewise_ite' s (h'.mono (inter_subset_left _ _))
+
 lemma piecewise_preimage (f g : α → β) (t) :
-  s.piecewise f g ⁻¹' t = s ∩ f ⁻¹' t ∪ sᶜ ∩ g ⁻¹' t :=
-ext $ λ x, by by_cases x ∈ s; simp *
+  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 :=

src/measure_theory/integration.lean

@@ -412,7 +412,7 @@ by simp only [hs, coe_restrict]
 
 theorem restrict_preimage (f : α →ₛ β) {s : set α} (hs : measurable_set s)
   {t : set β} (ht : (0:β) ∉ t) : restrict f s ⁻¹' t = s ∩ f ⁻¹' t :=
-by simp [hs, indicator_preimage_of_not_mem _ _ ht]
+by simp [hs, indicator_preimage_of_not_mem _ _ ht, inter_comm]
 
 theorem restrict_preimage_singleton (f : α →ₛ β) {s : set α} (hs : measurable_set s)
   {r : β} (hr : r ≠ 0) : restrict f s ⁻¹' {r} = s ∩ f ⁻¹' {r} :=

src/measure_theory/measurable_space.lean

@@ -204,6 +204,11 @@ by { rw inter_eq_compl_compl_union_compl, exact (h₁.compl.union h₂.compl).co
   measurable_set (s₁ \ s₂) :=
 h₁.inter h₂.compl
 
+@[simp] lemma measurable_set.ite {t s₁ s₂ : set α} (ht : measurable_set t) (h₁ : measurable_set s₁)
+  (h₂ : measurable_set s₂) :
+  measurable_set (t.ite s₁ s₂) :=
+(h₁.inter ht).union (h₂.diff ht)
+
 @[simp] lemma measurable_set.disjointed {f : ℕ → set α} (h : ∀ i, measurable_set (f i)) (n) :
   measurable_set (disjointed f n) :=
 disjointed_induct (h n) (assume t i ht, measurable_set.diff ht $ h _)
@@ -516,8 +521,8 @@ lemma measurable.piecewise {s : set α} {_ : decidable_pred s} {f g : α → β}
   measurable (piecewise s f g) :=
 begin
   intros t ht,
-  simp only [piecewise_preimage],
-  exact (hs.inter $ hf ht).union (hs.compl.inter $ hg ht)
+  rw piecewise_preimage,
+  exact hs.ite (hf ht) (hg ht)
 end
 
 /-- this is slightly different from `measurable.piecewise`. It can be used to show

src/measure_theory/set_integral.lean

@@ -632,8 +632,8 @@ begin
   assume t ht,
   obtain ⟨u, u_open, hu⟩ : ∃ (u : set α), is_open u ∧ f ⁻¹' t ∩ s = u ∩ s :=
     _root_.continuous_on_iff'.1 hf t ht,
-  rw [indicator_preimage, inter_comm, hu],
-  exact (u_open.measurable_set.inter hs).union (hs.compl.inter (measurable_const ht.measurable_set))
+  rw [indicator_preimage, set.ite, hu],
+  exact (u_open.measurable_set.inter hs).union ((measurable_zero ht.measurable_set).diff hs)
 end
 
 lemma continuous_on.integrable_at_nhds_within