feat(data/sigma,data/finset,algebra): add support for the sigma type to finset and big operators

Author: johoelzl

algebra/big_operators.lean

@@ -113,6 +113,19 @@ calc (s.product t).prod f = (s.prod $ λx, (t.image $ λy, (x, y)).prod f) :
     prod_bind $ assume x hx y hy h, ext $ by simp [mem_image_iff]; cc
   ... = _ : begin congr, apply funext, intro x, apply prod_image, simp {contextual := tt} end
 
+lemma prod_sigma {σ : α → Type*} [∀a, decidable_eq (σ a)]
+  {s : finset α} {t : Πa, finset (σ a)} {f : sigma σ → β} :
+  (s.sigma t).prod f = (s.prod $ λa, (t a).prod $ λs, f ⟨a, s⟩) :=
+have ∀a₁ a₂:α, ∀s₁ : finset (σ a₁), ∀s₂ : finset (σ a₂), a₁ ≠ a₂ →
+    s₁.image (sigma.mk a₁) ∩ s₂.image (sigma.mk a₂) = ∅,
+  from assume b₁ b₂ s₁ s₂ h, ext $ assume ⟨b₃, c₃⟩,
+    by simp [mem_image_iff, sigma.mk_eq_mk_iff, heq_iff_eq] {contextual := tt}; cc,
+calc (s.bind (λa, (t a).image (λs, sigma.mk a s))).prod f =
+      s.prod (λa, ((t a).image (λs, sigma.mk a s)).prod f) :
+    prod_bind $ assume a₁ ha a₂ ha₂ h, this a₁ a₂ (t a₁) (t a₂) h
+  ... = (s.prod $ λa, (t a).prod $ λs, f ⟨a, s⟩) :
+    by simp [prod_image, sigma.mk_eq_mk_iff, heq_iff_eq]
+
 lemma prod_mul_distrib : s.prod (λx, f x * g x) = s.prod f * s.prod g :=
 eq.trans (by simp; refl) fold_op_distrib
 
@@ -263,6 +276,7 @@ run_cmd transport_multiplicative_to_additive [
   (`finset.prod_inv_distrib, `finset.sum_neg_distrib),
   (`finset.prod_const_one, `finset.sum_const_zero),
   (`finset.prod_comm, `finset.sum_comm),
+  (`finset.prod_sigma, `finset.sum_sigma),
   (`finset.prod_subset, `finset.sum_subset)]
 
 namespace finset

data/finset/fold.lean

@@ -5,12 +5,19 @@ Author: Johannes Hölzl
 
 Fold on finite sets
 -/
-import data.list.set data.list.perm tactic.finish data.finset.basic
+import data.list.set data.list.perm data.finset.basic data.sigma tactic.finish
 open list subtype nat finset
 
 universes u v w
 variables {α : Type u} {β : Type v} {γ : Type w}
 
+section logic
+
+lemma heq_iff_eq {a₁ a₂ : α} : a₁ == a₂ ↔ a₁ = a₂ :=
+iff.intro eq_of_heq heq_of_eq
+
+end logic
+
 namespace list
 
 @[congr] lemma map_congr {f g : α → β} : ∀ {l : list α}, (∀ x ∈ l, f x = g x) → map f l = map g l
@@ -149,4 +156,22 @@ by simp [finset.product, mem_bind_iff, mem_image_iff]
 
 end prod
 
-end finset
+section sigma
+variables {σ : α → Type*} [decidable_eq α] [∀a, decidable_eq (σ a)]
+  {s : finset α} {t : Πa, finset (σ a)}
+
+protected def sigma (s : finset α) (t : Πa, finset (σ a)) : finset (Σa, σ a) :=
+s.bind $ λa, (t a).image $ λb, ⟨a, b⟩
+
+lemma mem_sigma_iff {p : sigma σ} : p ∈ s.sigma t ↔ p.1 ∈ s ∧ p.2 ∈ t (p.1) :=
+by cases p with a b;
+   simp [finset.sigma, mem_bind_iff, mem_image_iff, iff_def, sigma.mk_eq_mk_iff, heq_iff_eq]
+        {contextual := tt}
+
+lemma sigma_mono {s₁ s₂ : finset α} {t₁ t₂ : Πa, finset (σ a)} :
+  s₁ ⊆ s₂ → (∀a, t₁ a ⊆ t₂ a) → s₁.sigma t₁ ⊆ s₂.sigma t₂ :=
+by simp [subset_iff, mem_sigma_iff] {contextual := tt}
+
+end sigma
+
+end finset

data/sigma/basic.lean

@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2017 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Johannes Hölzl
+-/
+
+variables {α : Type*} {β : α → Type*}
+
+instance [inhabited α] [inhabited (β (default α))] : inhabited (sigma β) :=
+⟨⟨default α, default (β (default α))⟩⟩
+
+instance [h₁ : decidable_eq α] [h₂ : ∀a, decidable_eq (β a)] : decidable_eq (sigma β)
+| ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ := match a₁, b₁, a₂, b₂, h₁ a₁ a₂ with
+  | _, b₁, _, b₂, is_true (eq.refl a) :=
+    match b₁, b₂, h₂ a b₁ b₂ with
+    | _, _, is_true (eq.refl b) := is_true rfl
+    | b₁, b₂, is_false n := is_false (assume h, sigma.no_confusion h (λe₁ e₂, n $ eq_of_heq e₂))
+    end
+  | a₁, _, a₂, _, is_false n := is_false (assume h, sigma.no_confusion h (λe₁ e₂, n e₁))
+  end
+
+namespace sigma
+
+lemma mk_eq_mk_iff {a₁ a₂ : α} {b₁ : β a₁} {b₂ : β a₂} :
+  @sigma.mk α β a₁ b₁ = @sigma.mk α β a₂ b₂ ↔ (a₁ = a₂ ∧ b₁ == b₂) :=
+iff.intro sigma.mk.inj $
+  assume ⟨h₁, h₂⟩, match a₁, a₂, b₁, b₂, h₁, h₂ with _, _, _, _, eq.refl a, heq.refl b := rfl end
+
+variables {α₁ : Type*} {α₂ : Type*} {β₁ : α₁ → Type*} {β₂ : α₂ → Type*}
+
+def map (f₁ : α₁ → α₂) (f₂ : Πa, β₁ a → β₂ (f₁ a)) : sigma β₁ → sigma β₂
+| ⟨a, b⟩ := ⟨f₁ a, f₂ a b⟩
+
+end sigma

data/sigma/default.lean

@@ -0,0 +1 @@
+import data.sigma.basic

topology/infinite_sum.lean

@@ -143,6 +143,49 @@ have (λs:finset β, s.sum (g ∘ f)) = g ∘ (λs:finset β, s.sum f),
 show tendsto (λs:finset β, s.sum (g ∘ f)) at_top (nhds (g a)),
   by rw [this]; exact tendsto_compose hf (continuous_iff_tendsto.mp h₃ a)
 
+lemma is_sum_sigma [regular_space α] {γ : β → Type*} {f : (Σ b:β, γ b) → α} {g : β → α} {a : α}
+  (hf : ∀b, is_sum (λc, f ⟨b, c⟩) (g b)) (ha : is_sum f a) : is_sum g a :=
+assume s' hs',
+let
+  ⟨s, hs, hss', hsc⟩ := nhds_is_closed hs',
+  ⟨u, hu⟩ := mem_at_top_iff.mp $ ha $ hs,
+  fsts := u.image sigma.fst,
+  snds := λb, u.bind (λp, (if h : p.1 = b then {cast (congr_arg γ h) p.2} else ∅ : finset (γ b)))
+in
+have u_subset : u ⊆ fsts.sigma snds,
+  from subset_iff.mpr $ assume ⟨b, c⟩ hu,
+  have hb : b ∈ fsts, from mem_image_iff.mpr ⟨_, hu, rfl⟩,
+  have hc : c ∈ snds b, from mem_bind_iff.mpr ⟨_, hu, by simp; refl⟩,
+  by simp [mem_sigma_iff, hb, hc] ,
+mem_at_top_iff.mpr $ exists.intro fsts $ assume bs (hbs : fsts ⊆ bs),
+  have h : ∀cs:(Πb, b ∈ bs → finset (γ b)),
+      (⋂b (hb : b ∈ bs), (λp:Πb, finset (γ b), p b) ⁻¹' {cs' | cs b hb ⊆ cs' }) ∩
+      (λp, bs.sum (λb, (p b).sum (λc, f ⟨b, c⟩))) ⁻¹' s ≠ ∅,
+    from assume cs,
+    let cs' := λb, (if h : b ∈ bs then cs b h else ∅) ∪ snds b in
+    have sum_eq : bs.sum (λb, (cs' b).sum (λc, f ⟨b, c⟩)) = (bs.sigma cs').sum f,
+      from sum_sigma.symm,
+    have (bs.sigma cs').sum f ∈ s,
+      from hu _ $ subset.trans u_subset $ sigma_mono hbs $
+        assume b, @finset.subset_union_right (γ b) _ _ _,
+    ne_empty_iff_exists_mem.mpr $ exists.intro cs' $
+    by simp [sum_eq, this]; { intros b hb, simp [cs', hb, finset.subset_union_right] },
+  have tendsto (λp:(Πb:β, finset (γ b)), bs.sum (λb, (p b).sum (λc, f ⟨b, c⟩)))
+      (⨅b (h : b ∈ bs), at_top.vmap (λp, p b)) (nhds (bs.sum g)),
+    from tendsto_sum $
+      assume c hc, tendsto_infi' c $ tendsto_infi' hc $ tendsto_compose tendsto_vmap (hf c),
+  have bs.sum g ∈ s,
+    from mem_closure_of_tendsto this hsc $ forall_sets_neq_empty_iff_neq_bot.mp $
+      by simp [mem_inf_sets, exists_imp_distrib, and_imp, forall_and_distrib',
+               filter.mem_infi_sets_finset, mem_vmap, skolem, mem_at_top_iff];
+      from
+        assume s₁ s₂ s₃ hs₁ hs₃ p hs₂ p' hp cs hp',
+        have (⋂b (h : b ∈ bs), (λp:(Πb, finset (γ b)), p b) ⁻¹' {cs' | cs b h ⊆ cs' }) ≤ (⨅b∈bs, p b),
+          from infi_le_infi $ assume b, infi_le_infi $ assume hb,
+            le_trans (preimage_mono $ hp' b hb) (hp b hb),
+        neq_bot_of_le_neq_bot (h _) (le_trans (inter_subset_inter (le_trans this hs₂) hs₃) hs₁),
+  hss' this
+
 end is_sum
 
 section is_sum_iff_is_sum_of_iso_ne_zero
@@ -203,67 +246,6 @@ iff.intro (is_sum_of_is_sum_ne_zero h₂ h₁ h₄ h₃) (is_sum_of_is_sum_ne_ze
 
 end is_sum_iff_is_sum_of_iso_ne_zero
 
-lemma is_sum_sigma
-  [add_comm_monoid α] [topological_space α] [topological_add_monoid α] [regular_space α]
-  {γ : β → Type*} {f : (Σ b:β, γ b) → α} {g : β → α} {a : α}
-  (hf : ∀b, is_sum (λc, f ⟨b, c⟩) (g b)) (ha : is_sum f a) : is_sum g a :=
-assume s' hs',
-let
-  ⟨s, hs, hss', hsc⟩ := nhds_is_closed hs',
-  ⟨u, hu⟩ := mem_at_top_iff.mp $ ha $ hs,
-  fsts := u.image sigma.fst,
-  snds := λb, u.bind (λp, (if h : p.1 = b then {cast (congr_arg γ h) p.2} else ∅ : finset (γ b)))
-in
-have sig_inj : ∀b, ∀c₁ c₂ : γ b, sigma.mk b c₁ = sigma.mk b c₂ ↔ c₁ = c₂,
-  from assume b c₁ c₂, ⟨assume h, by cases h; refl, assume h, by simp *⟩,
-have sig_image_inj : ∀b₁ b₂, ∀s₁ : finset (γ b₁), ∀s₂ : finset (γ b₂), b₁ ≠ b₂ →
-    s₁.image (sigma.mk b₁) ∩ s₂.image (sigma.mk b₂) = ∅,
-  from assume b₁ b₂ s₁ s₂ h, ext $ assume ⟨b₃, c₃⟩,
-    by simp [mem_image_iff];
-    from assume c₁ h₁ eq₁ c₂ h₂ eq₂,
-      have h₁ : b₁ = b₃, from congr_arg sigma.fst eq₁,
-      have h₂ : b₂ = b₃, from congr_arg sigma.fst eq₂,
-      h $ by simp [h₁, h₂],
-mem_at_top_iff.mpr $ exists.intro fsts $ assume bs (hbs : fsts ⊆ bs),
-  have h : ∀cs:(Πb, b ∈ bs → finset (γ b)),
-      (⋂b (hb : b ∈ bs), (λp:Πb, finset (γ b), p b) ⁻¹' {cs' | cs b hb ⊆ cs' }) ∩
-      (λp, bs.sum (λb, (p b).sum (λc, f ⟨b, c⟩))) ⁻¹' s ≠ ∅,
-    from assume cs,
-    let cs' := λb, (if h : b ∈ bs then cs b h else ∅) ∪ snds b in
-    let sig : finset (sigma γ) := bs.bind (λb, (cs' b).image (λc, ⟨b, c⟩)) in
-    have sum_eq : bs.sum (λb, (cs' b).sum (λc, f ⟨b, c⟩)) = sig.sum f,
-      from calc bs.sum (λb, (cs' b).sum (λc, f ⟨b, c⟩)) =
-            bs.sum (λb, ((cs' b).image (@sigma.mk β γ b)).sum f) :
-          by simp [sum_image, sig_inj]
-        ... = sig.sum f :
-          (sum_bind $ assume b₁ hb b₂ hb₂ h, sig_image_inj b₁ b₂ (cs' b₁) (cs' b₂) h).symm,
-    have sig.sum f ∈ s,
-      from hu _ $ subset_iff.mpr $ show ∀x:sigma γ, x ∈ u → x ∈ sig,
-        from assume ⟨b, c⟩ hbc,
-        have hb : b ∈ fsts, from mem_image_iff.mpr ⟨_, hbc, rfl⟩,
-        have hb' : b ∈ bs, from mem_of_subset_of_mem hbs hb,
-        have hc : c ∈ snds b, from mem_bind_iff.mpr ⟨_, hbc, by simp; refl⟩,
-        have hc' : c ∈ cs' b, by simp [hb', hc],
-        by simp [sig, mem_bind_iff];
-        from ⟨b, hb', mem_image_iff.mpr ⟨c, hc', rfl⟩⟩,
-    ne_empty_iff_exists_mem.mpr $ exists.intro cs' $
-    by simp [sum_eq, this]; { intros b hb, simp [cs', hb, finset.subset_union_right] },
-  have tendsto (λp:(Πb:β, finset (γ b)), bs.sum (λb, (p b).sum (λc, f ⟨b, c⟩)))
-      (⨅b (h : b ∈ bs), at_top.vmap (λp, p b)) (nhds (bs.sum g)),
-    from tendsto_sum $
-      assume c hc, tendsto_infi' c $ tendsto_infi' hc $ tendsto_compose tendsto_vmap (hf c),
-  have bs.sum g ∈ s,
-    from mem_closure_of_tendsto this hsc $ forall_sets_neq_empty_iff_neq_bot.mp $
-      by simp [mem_inf_sets, exists_imp_distrib, and_imp, forall_and_distrib',
-               filter.mem_infi_sets_finset, mem_vmap, skolem, mem_at_top_iff];
-      from
-        assume s₁ s₂ s₃ hs₁ hs₃ p hs₂ p' hp cs hp',
-        have (⋂b (h : b ∈ bs), (λp:(Πb, finset (γ b)), p b) ⁻¹' {cs' | cs b h ⊆ cs' }) ≤ (⨅b∈bs, p b),
-          from infi_le_infi $ assume b, infi_le_infi $ assume hb,
-            le_trans (preimage_mono $ hp' b hb) (hp b hb),
-        neq_bot_of_le_neq_bot (h _) (le_trans (inter_subset_inter (le_trans this hs₂) hs₃) hs₁),
-  hss' this
-
 section topological_group
 variables [add_comm_group α] [uniform_space α] [complete_space α] [uniform_add_group α]
 variables {f g : β → α} {a a₁ a₂ : α}