# Lemmas on infinite sums and products in topological monoids #

This file contains many simple lemmas on tsum, HasSum etc, which are placed here in order to keep the basic file of definitions as short as possible.

Results requiring a group (rather than monoid) structure on the target should go in Group.lean.

theorem hasSum_zero {α : Type u_1} {β : Type u_2} [] [] :
HasSum (fun (x : β) => 0) 0

Constant zero function has sum 0

theorem hasProd_one {α : Type u_1} {β : Type u_2} [] [] :
HasProd (fun (x : β) => 1) 1

Constant one function has product 1

theorem hasSum_empty {α : Type u_1} {β : Type u_2} [] [] {f : βα} [] :
HasSum f 0
theorem hasProd_empty {α : Type u_1} {β : Type u_2} [] [] {f : βα} [] :
theorem summable_zero {α : Type u_1} {β : Type u_2} [] [] :
Summable fun (x : β) => 0
theorem multipliable_one {α : Type u_1} {β : Type u_2} [] [] :
Multipliable fun (x : β) => 1
theorem summable_empty {α : Type u_1} {β : Type u_2} [] [] {f : βα} [] :
theorem multipliable_empty {α : Type u_1} {β : Type u_2} [] [] {f : βα} [] :
theorem summable_congr {α : Type u_1} {β : Type u_2} [] [] {f : βα} {g : βα} (hfg : ∀ (b : β), f b = g b) :
theorem multipliable_congr {α : Type u_1} {β : Type u_2} [] [] {f : βα} {g : βα} (hfg : ∀ (b : β), f b = g b) :
theorem Summable.congr {α : Type u_1} {β : Type u_2} [] [] {f : βα} {g : βα} (hf : ) (hfg : ∀ (b : β), f b = g b) :
theorem Multipliable.congr {α : Type u_1} {β : Type u_2} [] [] {f : βα} {g : βα} (hf : ) (hfg : ∀ (b : β), f b = g b) :
theorem HasSum.congr_fun {α : Type u_1} {β : Type u_2} [] [] {f : βα} {g : βα} {a : α} (hf : HasSum f a) (h : ∀ (x : β), g x = f x) :
HasSum g a
theorem HasProd.congr_fun {α : Type u_1} {β : Type u_2} [] [] {f : βα} {g : βα} {a : α} (hf : HasProd f a) (h : ∀ (x : β), g x = f x) :
theorem HasSum.hasSum_of_sum_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {f : βα} {a : α} {g : γα} (h_eq : ∀ (u : ), ∃ (v : ), ∀ (v' : ), v v'∃ (u' : ), u u' xu', g x = bv', f b) (hf : HasSum g a) :
HasSum f a
theorem HasProd.hasProd_of_prod_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {f : βα} {a : α} {g : γα} (h_eq : ∀ (u : ), ∃ (v : ), ∀ (v' : ), v v'∃ (u' : ), u u' xu', g x = bv', f b) (hf : HasProd g a) :
theorem hasSum_iff_hasSum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {f : βα} {a : α} {g : γα} (h₁ : ∀ (u : ), ∃ (v : ), ∀ (v' : ), v v'∃ (u' : ), u u' xu', g x = bv', f b) (h₂ : ∀ (v : ), ∃ (u : ), ∀ (u' : ), u u'∃ (v' : ), v v' bv', f b = xu', g x) :
HasSum f a HasSum g a
theorem hasProd_iff_hasProd {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {f : βα} {a : α} {g : γα} (h₁ : ∀ (u : ), ∃ (v : ), ∀ (v' : ), v v'∃ (u' : ), u u' xu', g x = bv', f b) (h₂ : ∀ (v : ), ∃ (u : ), ∀ (u' : ), u u'∃ (v' : ), v v' bv', f b = xu', g x) :
theorem Function.Injective.summable_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {f : βα} {g : γβ} (hg : ) (hf : x, f x = 0) :
theorem Function.Injective.multipliable_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {f : βα} {g : γβ} (hg : ) (hf : x, f x = 1) :
@[simp]
theorem hasSum_extend_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {f : βα} {a : α} {g : βγ} (hg : ) :
@[simp]
theorem hasProd_extend_one {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {f : βα} {a : α} {g : βγ} (hg : ) :
@[simp]
theorem summable_extend_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {f : βα} {g : βγ} (hg : ) :
@[simp]
theorem multipliable_extend_one {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {f : βα} {g : βγ} (hg : ) :
theorem hasSum_subtype_iff_indicator {α : Type u_1} {β : Type u_2} [] [] {f : βα} {a : α} {s : Set β} :
HasSum (f Subtype.val) a HasSum (s.indicator f) a
theorem hasProd_subtype_iff_mulIndicator {α : Type u_1} {β : Type u_2} [] [] {f : βα} {a : α} {s : Set β} :
HasProd (f Subtype.val) a HasProd (s.mulIndicator f) a
theorem summable_subtype_iff_indicator {α : Type u_1} {β : Type u_2} [] [] {f : βα} {s : Set β} :
Summable (f Subtype.val) Summable (s.indicator f)
theorem multipliable_subtype_iff_mulIndicator {α : Type u_1} {β : Type u_2} [] [] {f : βα} {s : Set β} :
Multipliable (f Subtype.val) Multipliable (s.mulIndicator f)
@[simp]
theorem hasSum_subtype_support {α : Type u_1} {β : Type u_2} [] [] {f : βα} {a : α} :
HasSum (f Subtype.val) a HasSum f a
@[simp]
theorem hasProd_subtype_mulSupport {α : Type u_1} {β : Type u_2} [] [] {f : βα} {a : α} :
HasProd (f Subtype.val) a HasProd f a
theorem Finset.summable {α : Type u_1} {β : Type u_2} [] [] (s : ) (f : βα) :
Summable (f Subtype.val)
theorem Finset.multipliable {α : Type u_1} {β : Type u_2} [] [] (s : ) (f : βα) :
Multipliable (f Subtype.val)
theorem Set.Finite.summable {α : Type u_1} {β : Type u_2} [] [] {s : Set β} (hs : s.Finite) (f : βα) :
Summable (f Subtype.val)
theorem Set.Finite.multipliable {α : Type u_1} {β : Type u_2} [] [] {s : Set β} (hs : s.Finite) (f : βα) :
Multipliable (f Subtype.val)
theorem summable_of_finite_support {α : Type u_1} {β : Type u_2} [] [] {f : βα} (h : .Finite) :
theorem multipliable_of_finite_mulSupport {α : Type u_1} {β : Type u_2} [] [] {f : βα} (h : .Finite) :
theorem Summable.of_finite {α : Type u_1} {β : Type u_2} [] [] [] {f : βα} :
theorem Multipliable.of_finite {α : Type u_1} {β : Type u_2} [] [] [] {f : βα} :
theorem hasSum_single {α : Type u_1} {β : Type u_2} [] [] {f : βα} (b : β) (hf : ∀ (b' : β), b' bf b' = 0) :
HasSum f (f b)
theorem hasProd_single {α : Type u_1} {β : Type u_2} [] [] {f : βα} (b : β) (hf : ∀ (b' : β), b' bf b' = 1) :
HasProd f (f b)
@[simp]
theorem hasSum_unique {α : Type u_1} {β : Type u_2} [] [] [] (f : βα) :
HasSum f (f default)
@[simp]
theorem hasProd_unique {α : Type u_1} {β : Type u_2} [] [] [] (f : βα) :
HasProd f (f default)
@[simp]
theorem hasSum_singleton {α : Type u_1} {β : Type u_2} [] [] (m : β) (f : βα) :
HasSum ({m}.restrict f) (f m)
@[simp]
theorem hasProd_singleton {α : Type u_1} {β : Type u_2} [] [] (m : β) (f : βα) :
HasProd ({m}.restrict f) (f m)
theorem hasSum_ite_eq {α : Type u_1} {β : Type u_2} [] [] (b : β) [DecidablePred fun (x : β) => x = b] (a : α) :
HasSum (fun (b' : β) => if b' = b then a else 0) a
theorem hasProd_ite_eq {α : Type u_1} {β : Type u_2} [] [] (b : β) [DecidablePred fun (x : β) => x = b] (a : α) :
HasProd (fun (b' : β) => if b' = b then a else 1) a
theorem Equiv.hasSum_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {f : βα} {a : α} (e : γ β) :
HasSum (f e) a HasSum f a
theorem Equiv.hasProd_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {f : βα} {a : α} (e : γ β) :
HasProd (f e) a HasProd f a
theorem Function.Injective.hasSum_range_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {f : βα} {a : α} {g : γβ} (hg : ) :
HasSum (fun (x : (Set.range g)) => f x) a HasSum (f g) a
theorem Function.Injective.hasProd_range_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {f : βα} {a : α} {g : γβ} (hg : ) :
HasProd (fun (x : (Set.range g)) => f x) a HasProd (f g) a
theorem Equiv.summable_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {f : βα} (e : γ β) :
Summable (f e)
theorem Equiv.multipliable_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {f : βα} (e : γ β) :
Multipliable (f e)
theorem Equiv.hasSum_iff_of_support {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {f : βα} {a : α} {g : γα} (e : ) (he : ∀ (x : ), g (e x) = f x) :
HasSum f a HasSum g a
theorem Equiv.hasProd_iff_of_mulSupport {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {f : βα} {a : α} {g : γα} (e : ) (he : ∀ (x : ), g (e x) = f x) :
theorem hasSum_iff_hasSum_of_ne_zero_bij {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {f : βα} {a : α} {g : γα} (i : β) (hi : ) (hf : ) (hfg : ∀ (x : ), f (i x) = g x) :
HasSum f a HasSum g a
theorem hasProd_iff_hasProd_of_ne_one_bij {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {f : βα} {a : α} {g : γα} (i : β) (hi : ) (hf : ) (hfg : ∀ (x : ), f (i x) = g x) :
theorem Equiv.summable_iff_of_support {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {f : βα} {g : γα} (e : ) (he : ∀ (x : ), g (e x) = f x) :
theorem Equiv.multipliable_iff_of_mulSupport {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {f : βα} {g : γα} (e : ) (he : ∀ (x : ), g (e x) = f x) :
theorem HasSum.map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {f : βα} {a : α} [] [] (hf : HasSum f a) {G : Type u_5} [FunLike G α γ] [] (g : G) (hg : ) :
HasSum (g f) (g a)
theorem HasProd.map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {f : βα} {a : α} [] [] (hf : HasProd f a) {G : Type u_5} [FunLike G α γ] [] (g : G) (hg : ) :
HasProd (g f) (g a)
theorem Inducing.hasSum_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] {G : Type u_5} [FunLike G α γ] [] {g : G} (hg : Inducing g) (f : βα) (a : α) :
HasSum (g f) (g a) HasSum f a
theorem Inducing.hasProd_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] {G : Type u_5} [FunLike G α γ] [] {g : G} (hg : Inducing g) (f : βα) (a : α) :
HasProd (g f) (g a) HasProd f a
theorem Summable.map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {f : βα} [] [] (hf : ) {G : Type u_5} [FunLike G α γ] [] (g : G) (hg : ) :
Summable (g f)
theorem Multipliable.map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {f : βα} [] [] (hf : ) {G : Type u_5} [FunLike G α γ] [] (g : G) (hg : ) :
Multipliable (g f)
theorem Summable.map_iff_of_leftInverse {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {f : βα} [] [] {G : Type u_5} {G' : Type u_6} [FunLike G α γ] [] [FunLike G' γ α] [] (g : G) (g' : G') (hg : ) (hg' : Continuous g') (hinv : Function.LeftInverse g' g) :
Summable (g f)
theorem Multipliable.map_iff_of_leftInverse {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {f : βα} [] [] {G : Type u_5} {G' : Type u_6} [FunLike G α γ] [] [FunLike G' γ α] [MonoidHomClass G' γ α] (g : G) (g' : G') (hg : ) (hg' : Continuous g') (hinv : Function.LeftInverse g' g) :
Multipliable (g f)
theorem Summable.map_tsum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {f : βα} [] [] [] (hf : ) {G : Type u_5} [FunLike G α γ] [] (g : G) (hg : ) :
g (∑' (i : β), f i) = ∑' (i : β), g (f i)
theorem Multipliable.map_tprod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {f : βα} [] [] [] (hf : ) {G : Type u_5} [FunLike G α γ] [] (g : G) (hg : ) :
g (∏' (i : β), f i) = ∏' (i : β), g (f i)
theorem Inducing.summable_iff_tsum_comp_mem_range {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] [] {G : Type u_5} [FunLike G α γ] [] {g : G} (hg : Inducing g) (f : βα) :
Summable (g f) ∑' (i : β), g (f i)
theorem Inducing.multipliable_iff_tprod_comp_mem_range {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] [] {G : Type u_5} [FunLike G α γ] [] {g : G} (hg : Inducing g) (f : βα) :
Multipliable (g f) ∏' (i : β), g (f i)
theorem Summable.map_iff_of_equiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {f : βα} [] [] {G : Type u_5} [EquivLike G α γ] [] (g : G) (hg : ) (hg' : ) :
Summable (g f)

A special case of Summable.map_iff_of_leftInverse for convenience

theorem Multipliable.map_iff_of_equiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {f : βα} [] [] {G : Type u_5} [EquivLike G α γ] [] (g : G) (hg : ) (hg' : ) :
Multipliable (g f)

"A special case of Multipliable.map_iff_of_leftInverse for convenience"

theorem Function.Surjective.summable_iff_of_hasSum_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {α' : Type u_5} [] [] {e : α'α} (hes : ) {f : βα} {g : γα'} (he : ∀ {a : α'}, HasSum f (e a) HasSum g a) :
theorem Function.Surjective.multipliable_iff_of_hasProd_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {α' : Type u_5} [] [] {e : α'α} (hes : ) {f : βα} {g : γα'} (he : ∀ {a : α'}, HasProd f (e a) HasProd g a) :
theorem HasSum.add {α : Type u_1} {β : Type u_2} [] [] {f : βα} {g : βα} {a : α} {b : α} [] (hf : HasSum f a) (hg : HasSum g b) :
HasSum (fun (b : β) => f b + g b) (a + b)
theorem HasProd.mul {α : Type u_1} {β : Type u_2} [] [] {f : βα} {g : βα} {a : α} {b : α} [] (hf : HasProd f a) (hg : HasProd g b) :
HasProd (fun (b : β) => f b * g b) (a * b)
theorem Summable.add {α : Type u_1} {β : Type u_2} [] [] {f : βα} {g : βα} [] (hf : ) (hg : ) :
Summable fun (b : β) => f b + g b
theorem Multipliable.mul {α : Type u_1} {β : Type u_2} [] [] {f : βα} {g : βα} [] (hf : ) (hg : ) :
Multipliable fun (b : β) => f b * g b
theorem hasSum_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {f : γβα} {a : γα} {s : } :
(∀ is, HasSum (f i) (a i))HasSum (fun (b : β) => is, f i b) (∑ is, a i)
theorem hasProd_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {f : γβα} {a : γα} {s : } :
(∀ is, HasProd (f i) (a i))HasProd (fun (b : β) => is, f i b) (∏ is, a i)
theorem summable_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {f : γβα} {s : } (hf : is, Summable (f i)) :
Summable fun (b : β) => is, f i b
theorem multipliable_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {f : γβα} {s : } (hf : is, Multipliable (f i)) :
Multipliable fun (b : β) => is, f i b
theorem HasSum.add_disjoint {α : Type u_1} {β : Type u_2} [] [] {f : βα} {a : α} {b : α} [] {s : Set β} {t : Set β} (hs : Disjoint s t) (ha : HasSum (f Subtype.val) a) (hb : HasSum (f Subtype.val) b) :
HasSum (f Subtype.val) (a + b)
theorem HasProd.mul_disjoint {α : Type u_1} {β : Type u_2} [] [] {f : βα} {a : α} {b : α} [] {s : Set β} {t : Set β} (hs : Disjoint s t) (ha : HasProd (f Subtype.val) a) (hb : HasProd (f Subtype.val) b) :
HasProd (f Subtype.val) (a * b)
theorem hasSum_sum_disjoint {α : Type u_1} {β : Type u_2} [] [] {f : βα} [] {ι : Type u_5} (s : ) {t : ιSet β} {a : ια} (hs : (↑s).Pairwise (Disjoint on t)) (hf : is, HasSum (f Subtype.val) (a i)) :
HasSum (f Subtype.val) (∑ is, a i)
theorem hasProd_prod_disjoint {α : Type u_1} {β : Type u_2} [] [] {f : βα} [] {ι : Type u_5} (s : ) {t : ιSet β} {a : ια} (hs : (↑s).Pairwise (Disjoint on t)) (hf : is, HasProd (f Subtype.val) (a i)) :
HasProd (f Subtype.val) (∏ is, a i)
theorem HasSum.add_isCompl {α : Type u_1} {β : Type u_2} [] [] {f : βα} {a : α} {b : α} [] {s : Set β} {t : Set β} (hs : IsCompl s t) (ha : HasSum (f Subtype.val) a) (hb : HasSum (f Subtype.val) b) :
HasSum f (a + b)
theorem HasProd.mul_isCompl {α : Type u_1} {β : Type u_2} [] [] {f : βα} {a : α} {b : α} [] {s : Set β} {t : Set β} (hs : IsCompl s t) (ha : HasProd (f Subtype.val) a) (hb : HasProd (f Subtype.val) b) :
HasProd f (a * b)
theorem HasSum.add_compl {α : Type u_1} {β : Type u_2} [] [] {f : βα} {a : α} {b : α} [] {s : Set β} (ha : HasSum (f Subtype.val) a) (hb : HasSum (f Subtype.val) b) :
HasSum f (a + b)
theorem HasProd.mul_compl {α : Type u_1} {β : Type u_2} [] [] {f : βα} {a : α} {b : α} [] {s : Set β} (ha : HasProd (f Subtype.val) a) (hb : HasProd (f Subtype.val) b) :
HasProd f (a * b)
theorem Summable.add_compl {α : Type u_1} {β : Type u_2} [] [] {f : βα} [] {s : Set β} (hs : Summable (f Subtype.val)) (hsc : Summable (f Subtype.val)) :
theorem Multipliable.mul_compl {α : Type u_1} {β : Type u_2} [] [] {f : βα} [] {s : Set β} (hs : Multipliable (f Subtype.val)) (hsc : Multipliable (f Subtype.val)) :
theorem HasSum.compl_add {α : Type u_1} {β : Type u_2} [] [] {f : βα} {a : α} {b : α} [] {s : Set β} (ha : HasSum (f Subtype.val) a) (hb : HasSum (f Subtype.val) b) :
HasSum f (a + b)
theorem HasProd.compl_mul {α : Type u_1} {β : Type u_2} [] [] {f : βα} {a : α} {b : α} [] {s : Set β} (ha : HasProd (f Subtype.val) a) (hb : HasProd (f Subtype.val) b) :
HasProd f (a * b)
theorem Summable.compl_add {α : Type u_1} {β : Type u_2} [] [] {f : βα} [] {s : Set β} (hs : Summable (f Subtype.val)) (hsc : Summable (f Subtype.val)) :
theorem Multipliable.compl_add {α : Type u_1} {β : Type u_2} [] [] {f : βα} [] {s : Set β} (hs : Multipliable (f Subtype.val)) (hsc : Multipliable (f Subtype.val)) :
theorem HasSum.update' {α : Type u_5} {β : Type u_6} [] [] [] [] [] {f : βα} {a : α} {a' : α} (hf : HasSum f a) (b : β) (x : α) (hf' : HasSum (Function.update f b x) a') :
a + x = a' + f b

Version of HasSum.update for AddCommMonoid rather than AddCommGroup. Rather than showing that f.update has a specific sum in terms of HasSum, it gives a relationship between the sums of f and f.update given that both exist.

theorem HasProd.update' {α : Type u_5} {β : Type u_6} [] [] [] [] [] {f : βα} {a : α} {a' : α} (hf : HasProd f a) (b : β) (x : α) (hf' : HasProd (Function.update f b x) a') :
a * x = a' * f b

Version of HasProd.update for CommMonoid rather than CommGroup. Rather than showing that f.update has a specific product in terms of HasProd, it gives a relationship between the products of f and f.update given that both exist.

theorem eq_add_of_hasSum_ite {α : Type u_5} {β : Type u_6} [] [] [] [] [] {f : βα} {a : α} (hf : HasSum f a) (b : β) (a' : α) (hf' : HasSum (fun (n : β) => if n = b then 0 else f n) a') :
a = a' + f b

Version of hasSum_ite_sub_hasSum for AddCommMonoid rather than AddCommGroup. Rather than showing that the ite expression has a specific sum in terms of HasSum, it gives a relationship between the sums of f and ite (n = b) 0 (f n) given that both exist.

theorem eq_mul_of_hasProd_ite {α : Type u_5} {β : Type u_6} [] [] [] [] [] {f : βα} {a : α} (hf : HasProd f a) (b : β) (a' : α) (hf' : HasProd (fun (n : β) => if n = b then 1 else f n) a') :
a = a' * f b

Version of hasProd_ite_div_hasProd for CommMonoid rather than CommGroup. Rather than showing that the ite expression has a specific product in terms of HasProd, it gives a relationship between the products of f and ite (n = b) 0 (f n) given that both exist.

theorem tsum_congr_set_coe {α : Type u_1} {β : Type u_2} [] [] (f : βα) {s : Set β} {t : Set β} (h : s = t) :
∑' (x : s), f x = ∑' (x : t), f x
theorem tprod_congr_set_coe {α : Type u_1} {β : Type u_2} [] [] (f : βα) {s : Set β} {t : Set β} (h : s = t) :
∏' (x : s), f x = ∏' (x : t), f x
theorem tsum_congr_subtype {α : Type u_1} {β : Type u_2} [] [] (f : βα) {P : βProp} {Q : βProp} (h : ∀ (x : β), P x Q x) :
∑' (x : { x : β // P x }), f x = ∑' (x : { x : β // Q x }), f x
theorem tprod_congr_subtype {α : Type u_1} {β : Type u_2} [] [] (f : βα) {P : βProp} {Q : βProp} (h : ∀ (x : β), P x Q x) :
∏' (x : { x : β // P x }), f x = ∏' (x : { x : β // Q x }), f x
theorem tsum_eq_finsum {α : Type u_1} {β : Type u_2} [] [] {f : βα} (hf : .Finite) :
∑' (b : β), f b = ∑ᶠ (b : β), f b
theorem tprod_eq_finprod {α : Type u_1} {β : Type u_2} [] [] {f : βα} (hf : .Finite) :
∏' (b : β), f b = ∏ᶠ (b : β), f b
theorem tsum_eq_sum' {α : Type u_1} {β : Type u_2} [] [] {f : βα} {s : } (hf : ) :
∑' (b : β), f b = bs, f b
theorem tprod_eq_prod' {α : Type u_1} {β : Type u_2} [] [] {f : βα} {s : } (hf : ) :
∏' (b : β), f b = bs, f b
theorem tsum_eq_sum {α : Type u_1} {β : Type u_2} [] [] {f : βα} {s : } (hf : bs, f b = 0) :
∑' (b : β), f b = bs, f b
theorem tprod_eq_prod {α : Type u_1} {β : Type u_2} [] [] {f : βα} {s : } (hf : bs, f b = 1) :
∏' (b : β), f b = bs, f b
@[simp]
theorem tsum_zero {α : Type u_1} {β : Type u_2} [] [] :
∑' (x : β), 0 = 0
@[simp]
theorem tprod_one {α : Type u_1} {β : Type u_2} [] [] :
∏' (x : β), 1 = 1
@[simp]
theorem tsum_empty {α : Type u_1} {β : Type u_2} [] [] {f : βα} [] :
∑' (b : β), f b = 0
@[simp]
theorem tprod_empty {α : Type u_1} {β : Type u_2} [] [] {f : βα} [] :
∏' (b : β), f b = 1
theorem tsum_congr {α : Type u_1} {β : Type u_2} [] [] {f : βα} {g : βα} (hfg : ∀ (b : β), f b = g b) :
∑' (b : β), f b = ∑' (b : β), g b
theorem tprod_congr {α : Type u_1} {β : Type u_2} [] [] {f : βα} {g : βα} (hfg : ∀ (b : β), f b = g b) :
∏' (b : β), f b = ∏' (b : β), g b
theorem tsum_fintype {α : Type u_1} {β : Type u_2} [] [] [] (f : βα) :
∑' (b : β), f b = b : β, f b
theorem tprod_fintype {α : Type u_1} {β : Type u_2} [] [] [] (f : βα) :
∏' (b : β), f b = b : β, f b
theorem sum_eq_tsum_indicator {α : Type u_1} {β : Type u_2} [] [] (f : βα) (s : ) :
xs, f x = ∑' (x : β), (↑s).indicator f x
theorem prod_eq_tprod_mulIndicator {α : Type u_1} {β : Type u_2} [] [] (f : βα) (s : ) :
xs, f x = ∏' (x : β), (↑s).mulIndicator f x
theorem tsum_bool {α : Type u_1} [] [] (f : Boolα) :
∑' (i : Bool), f i = + f true
theorem tprod_bool {α : Type u_1} [] [] (f : Boolα) :
∏' (i : Bool), f i = * f true
theorem tsum_eq_single {α : Type u_1} {β : Type u_2} [] [] {f : βα} (b : β) (hf : ∀ (b' : β), b' bf b' = 0) :
∑' (b : β), f b = f b
theorem tprod_eq_mulSingle {α : Type u_1} {β : Type u_2} [] [] {f : βα} (b : β) (hf : ∀ (b' : β), b' bf b' = 1) :
∏' (b : β), f b = f b
theorem tsum_tsum_eq_single {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] (f : βγα) (b : β) (c : γ) (hfb : ∀ (b' : β), b' bf b' c = 0) (hfc : ∀ (b' : β) (c' : γ), c' cf b' c' = 0) :
∑' (b' : β) (c' : γ), f b' c' = f b c
theorem tprod_tprod_eq_mulSingle {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] (f : βγα) (b : β) (c : γ) (hfb : ∀ (b' : β), b' bf b' c = 1) (hfc : ∀ (b' : β) (c' : γ), c' cf b' c' = 1) :
∏' (b' : β) (c' : γ), f b' c' = f b c
@[simp]
theorem tsum_ite_eq {α : Type u_1} {β : Type u_2} [] [] (b : β) [DecidablePred fun (x : β) => x = b] (a : α) :
(∑' (b' : β), if b' = b then a else 0) = a
@[simp]
theorem tprod_ite_eq {α : Type u_1} {β : Type u_2} [] [] (b : β) [DecidablePred fun (x : β) => x = b] (a : α) :
(∏' (b' : β), if b' = b then a else 1) = a
@[simp]
theorem Finset.tsum_subtype {α : Type u_1} {β : Type u_2} [] [] (s : ) (f : βα) :
∑' (x : { x : β // x s }), f x = xs, f x
@[simp]
theorem Finset.tprod_subtype {α : Type u_1} {β : Type u_2} [] [] (s : ) (f : βα) :
∏' (x : { x : β // x s }), f x = xs, f x
theorem Finset.tsum_subtype' {α : Type u_1} {β : Type u_2} [] [] (s : ) (f : βα) :
∑' (x : s), f x = xs, f x
theorem Finset.tprod_subtype' {α : Type u_1} {β : Type u_2} [] [] (s : ) (f : βα) :
∏' (x : s), f x = xs, f x
@[simp]
theorem tsum_singleton {α : Type u_1} {β : Type u_2} [] [] (b : β) (f : βα) :
∑' (x : {b}), f x = f b
@[simp]
theorem tprod_singleton {α : Type u_1} {β : Type u_2} [] [] (b : β) (f : βα) :
∏' (x : {b}), f x = f b
theorem Function.Injective.tsum_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {g : γβ} (hg : ) {f : βα} (hf : ) :
∑' (c : γ), f (g c) = ∑' (b : β), f b
theorem Function.Injective.tprod_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {g : γβ} (hg : ) {f : βα} (hf : ) :
∏' (c : γ), f (g c) = ∏' (b : β), f b
theorem Equiv.tsum_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] (e : γ β) (f : βα) :
∑' (c : γ), f (e c) = ∑' (b : β), f b
theorem Equiv.tprod_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] (e : γ β) (f : βα) :
∏' (c : γ), f (e c) = ∏' (b : β), f b

### tprod on subsets - part 1 #

theorem tsum_subtype_eq_of_support_subset {α : Type u_1} {β : Type u_2} [] [] {f : βα} {s : Set β} (hs : ) :
∑' (x : s), f x = ∑' (x : β), f x
theorem tprod_subtype_eq_of_mulSupport_subset {α : Type u_1} {β : Type u_2} [] [] {f : βα} {s : Set β} (hs : ) :
∏' (x : s), f x = ∏' (x : β), f x
theorem tsum_subtype_support {α : Type u_1} {β : Type u_2} [] [] (f : βα) :
∑' (x : ), f x = ∑' (x : β), f x
theorem tprod_subtype_mulSupport {α : Type u_1} {β : Type u_2} [] [] (f : βα) :
∏' (x : ), f x = ∏' (x : β), f x
theorem tsum_subtype {α : Type u_1} {β : Type u_2} [] [] (s : Set β) (f : βα) :
∑' (x : s), f x = ∑' (x : β), s.indicator f x
theorem tprod_subtype {α : Type u_1} {β : Type u_2} [] [] (s : Set β) (f : βα) :
∏' (x : s), f x = ∏' (x : β), s.mulIndicator f x
@[simp]
theorem tsum_univ {α : Type u_1} {β : Type u_2} [] [] (f : βα) :
∑' (x : Set.univ), f x = ∑' (x : β), f x
@[simp]
theorem tprod_univ {α : Type u_1} {β : Type u_2} [] [] (f : βα) :
∏' (x : Set.univ), f x = ∏' (x : β), f x
theorem tsum_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {g : γβ} (f : βα) {s : Set γ} (hg : ) :
∑' (x : (g '' s)), f x = ∑' (x : s), f (g x)
theorem tprod_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {g : γβ} (f : βα) {s : Set γ} (hg : ) :
∏' (x : (g '' s)), f x = ∏' (x : s), f (g x)
theorem tsum_range {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {g : γβ} (f : βα) (hg : ) :
∑' (x : (Set.range g)), f x = ∑' (x : γ), f (g x)
theorem tprod_range {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {g : γβ} (f : βα) (hg : ) :
∏' (x : (Set.range g)), f x = ∏' (x : γ), f (g x)
theorem tsum_setElem_eq_tsum_setElem_diff {α : Type u_1} {β : Type u_2} [] [] {f : βα} (s : Set β) (t : Set β) (hf₀ : bt, f b = 0) :
∑' (a : s), f a = ∑' (a : (s \ t)), f a

If f b = 0 for all b ∈ t, then the sum of f a with a ∈ s is the same as the sum of f a with a ∈ s ∖ t.

theorem tprod_setElem_eq_tprod_setElem_diff {α : Type u_1} {β : Type u_2} [] [] {f : βα} (s : Set β) (t : Set β) (hf₀ : bt, f b = 1) :
∏' (a : s), f a = ∏' (a : (s \ t)), f a

If f b = 1 for all b ∈ t, then the product of f a with a ∈ s is the same as the product of f a with a ∈ s ∖ t.

theorem tsum_eq_tsum_diff_singleton {α : Type u_1} {β : Type u_2} [] [] {f : βα} (s : Set β) {b : β} (hf₀ : f b = 0) :
∑' (a : s), f a = ∑' (a : (s \ {b})), f a

If f b = 0, then the sum of f a with a ∈ s is the same as the sum of f a for a ∈ s ∖ {b}.

theorem tprod_eq_tprod_diff_singleton {α : Type u_1} {β : Type u_2} [] [] {f : βα} (s : Set β) {b : β} (hf₀ : f b = 1) :
∏' (a : s), f a = ∏' (a : (s \ {b})), f a

If f b = 1, then the product of f a with a ∈ s is the same as the product of f a for a ∈ s ∖ {b}.

theorem tsum_eq_tsum_of_ne_zero_bij {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {f : βα} {g : γα} (i : β) (hi : ) (hf : ) (hfg : ∀ (x : ), f (i x) = g x) :
∑' (x : β), f x = ∑' (y : γ), g y
theorem tprod_eq_tprod_of_ne_one_bij {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {f : βα} {g : γα} (i : β) (hi : ) (hf : ) (hfg : ∀ (x : ), f (i x) = g x) :
∏' (x : β), f x = ∏' (y : γ), g y
theorem Equiv.tsum_eq_tsum_of_support {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {f : βα} {g : γα} (e : ) (he : ∀ (x : ), g (e x) = f x) :
∑' (x : β), f x = ∑' (y : γ), g y
theorem Equiv.tprod_eq_tprod_of_mulSupport {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {f : βα} {g : γα} (e : ) (he : ∀ (x : ), g (e x) = f x) :
∏' (x : β), f x = ∏' (y : γ), g y
theorem tsum_dite_right {α : Type u_1} {β : Type u_2} [] [] (P : Prop) [] (x : β¬Pα) :
(∑' (b : β), if h : P then 0 else x b h) = if h : P then 0 else ∑' (b : β), x b h
theorem tprod_dite_right {α : Type u_1} {β : Type u_2} [] [] (P : Prop) [] (x : β¬Pα) :
(∏' (b : β), if h : P then 1 else x b h) = if h : P then 1 else ∏' (b : β), x b h
theorem tsum_dite_left {α : Type u_1} {β : Type u_2} [] [] (P : Prop) [] (x : βPα) :
(∑' (b : β), if h : P then x b h else 0) = if h : P then ∑' (b : β), x b h else 0
theorem tprod_dite_left {α : Type u_1} {β : Type u_2} [] [] (P : Prop) [] (x : βPα) :
(∏' (b : β), if h : P then x b h else 1) = if h : P then ∏' (b : β), x b h else 1
@[simp]
theorem tsum_extend_zero {α : Type u_1} {β : Type u_2} [] [] {γ : Type u_5} {g : γβ} (hg : ) (f : γα) :
∑' (y : β), Function.extend g f 0 y = ∑' (x : γ), f x
@[simp]
theorem tprod_extend_one {α : Type u_1} {β : Type u_2} [] [] {γ : Type u_5} {g : γβ} (hg : ) (f : γα) :
∏' (y : β), Function.extend g f 1 y = ∏' (x : γ), f x
theorem Function.Surjective.tsum_eq_tsum_of_hasSum_iff_hasSum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {α' : Type u_5} [] [] {e : α'α} (hes : ) (h1 : e 0 = 0) {f : βα} {g : γα'} (h : ∀ {a : α'}, HasSum f (e a) HasSum g a) :
∑' (b : β), f b = e (∑' (c : γ), g c)
theorem Function.Surjective.tprod_eq_tprod_of_hasProd_iff_hasProd {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {α' : Type u_5} [] [] {e : α'α} (hes : ) (h1 : e 1 = 1) {f : βα} {g : γα'} (h : ∀ {a : α'}, HasProd f (e a) HasProd g a) :
∏' (b : β), f b = e (∏' (c : γ), g c)
theorem tsum_eq_tsum_of_hasSum_iff_hasSum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {f : βα} {g : γα} (h : ∀ {a : α}, HasSum f a HasSum g a) :
∑' (b : β), f b = ∑' (c : γ), g c
theorem tprod_eq_tprod_of_hasProd_iff_hasProd {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {f : βα} {g : γα} (h : ∀ {a : α}, HasProd f a HasProd g a) :
∏' (b : β), f b = ∏' (c : γ), g c
theorem tsum_add {α : Type u_1} {β : Type u_2} [] [] {f : βα} {g : βα} [] [] (hf : ) (hg : ) :
∑' (b : β), (f b + g b) = ∑' (b : β), f b + ∑' (b : β), g b
theorem tprod_mul {α : Type u_1} {β : Type u_2} [] [] {f : βα} {g : βα} [] [] (hf : ) (hg : ) :
∏' (b : β), f b * g b = (∏' (b : β), f b) * ∏' (b : β), g b
theorem tsum_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] {f : γβα} {s : } (hf : is, Summable (f i)) :
∑' (b : β), is, f i b = is, ∑' (b : β), f i b
theorem tprod_of_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] {f : γβα} {s : } (hf : is, Multipliable (f i)) :
∏' (b : β), is, f i b = is, ∏' (b : β), f i b
theorem tsum_eq_add_tsum_ite' {α : Type u_1} {β : Type u_2} [] [] [] [] [] {f : βα} (b : β) (hf : Summable (Function.update f b 0)) :
∑' (x : β), f x = f b + ∑' (x : β), if x = b then 0 else f x

Version of tsum_eq_add_tsum_ite for AddCommMonoid rather than AddCommGroup. Requires a different convergence assumption involving Function.update.

theorem tprod_eq_mul_tprod_ite' {α : Type u_1} {β : Type u_2} [] [] [] [] [] {f : βα} (b : β) (hf : Multipliable (Function.update f b 1)) :
∏' (x : β), f x = f b * ∏' (x : β), if x = b then 1 else f x

Version of tprod_eq_mul_tprod_ite for CommMonoid rather than CommGroup. Requires a different convergence assumption involving Function.update.

theorem tsum_add_tsum_compl {α : Type u_1} {β : Type u_2} [] [] {f : βα} [] [] {s : Set β} (hs : Summable (f Subtype.val)) (hsc : Summable (f Subtype.val)) :
∑' (x : s), f x + ∑' (x : s), f x = ∑' (x : β), f x
theorem tprod_mul_tprod_compl {α : Type u_1} {β : Type u_2} [] [] {f : βα} [] [] {s : Set β} (hs : Multipliable (f Subtype.val)) (hsc : Multipliable (f Subtype.val)) :
(∏' (x : s), f x) * ∏' (x : s), f x = ∏' (x : β), f x
theorem tsum_union_disjoint {α : Type u_1} {β : Type u_2} [] [] {f : βα} [] [] {s : Set β} {t : Set β} (hd : Disjoint s t) (hs : Summable (f Subtype.val)) (ht : Summable (f Subtype.val)) :
∑' (x : (s t)), f x = ∑' (x : s), f x + ∑' (x : t), f x
theorem tprod_union_disjoint {α : Type u_1} {β : Type u_2} [] [] {f : βα} [] [] {s : Set β} {t : Set β} (hd : Disjoint s t) (hs : Multipliable (f Subtype.val)) (ht : Multipliable (f Subtype.val)) :
∏' (x : (s t)), f x = (∏' (x : s), f x) * ∏' (x : t), f x
theorem tsum_finset_bUnion_disjoint {α : Type u_1} {β : Type u_2} [] [] {f : βα} [] [] {ι : Type u_5} {s : } {t : ιSet β} (hd : (↑s).Pairwise (Disjoint on t)) (hf : is, Summable (f Subtype.val)) :
∑' (x : (⋃ is, t i)), f x = is, ∑' (x : (t i)), f x
theorem tprod_finset_bUnion_disjoint {α : Type u_1} {β : Type u_2} [] [] {f : βα} [] [] {ι : Type u_5} {s : } {t : ιSet β} (hd : (↑s).Pairwise (Disjoint on t)) (hf : is, Multipliable (f Subtype.val)) :
∏' (x : (⋃ is, t i)), f x = is, ∏' (x : (t i)), f x