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} [AddCommMonoid α] [TopologicalSpace α] : HasSum (fun (x : β) => 0) 0

Constant zero function has sum 0

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

Constant one function has product 1

theorem hasSum_empty {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} [IsEmpty β] : HasSum f 0

theorem hasProd_empty {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} [IsEmpty β] : HasProd f 1

theorem summable_zero {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] : Summable fun (x : β) => 0

theorem multipliable_one {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] : Multipliable fun (x : β) => 1

theorem summable_empty {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} [IsEmpty β] : Summable f

theorem multipliable_empty {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} [IsEmpty β] : Multipliable f

theorem summable_congr {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {g : β → α} (hfg : ∀ (b : β), f b = g b) : Summable f ↔ Summable g

theorem multipliable_congr {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} {g : β → α} (hfg : ∀ (b : β), f b = g b) : Multipliable f ↔ Multipliable g

theorem Summable.congr {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {g : β → α} (hf : Summable f) (hfg : ∀ (b : β), f b = g b) : Summable g

theorem Multipliable.congr {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} {g : β → α} (hf : Multipliable f) (hfg : ∀ (b : β), f b = g b) : Multipliable g

theorem HasSum.congr_fun {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {g : β → α} {a : α} (hf : HasSum f a) (h : g = f) : HasSum g a

theorem HasProd.congr_fun {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} {g : β → α} {a : α} (hf : HasProd f a) (h : g = f) : HasProd g a

theorem HasSum.hasSum_of_sum_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} {g : γ → α} (h_eq : ∀ (u : Finset γ), ∃ (v : Finset β), ∀ (v' : Finset β), v ⊆ v' → ∃ (u' : Finset γ), u ⊆ u' ∧ (Finset.sum u' fun (x : γ) => g x) = Finset.sum v' fun (b : β) => f b) (hf : HasSum g a) : HasSum f a

theorem HasProd.hasProd_of_prod_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} {g : γ → α} (h_eq : ∀ (u : Finset γ), ∃ (v : Finset β), ∀ (v' : Finset β), v ⊆ v' → ∃ (u' : Finset γ), u ⊆ u' ∧ (Finset.prod u' fun (x : γ) => g x) = Finset.prod v' fun (b : β) => f b) (hf : HasProd g a) : HasProd f a

theorem hasSum_iff_hasSum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} {g : γ → α} (h₁ : ∀ (u : Finset γ), ∃ (v : Finset β), ∀ (v' : Finset β), v ⊆ v' → ∃ (u' : Finset γ), u ⊆ u' ∧ (Finset.sum u' fun (x : γ) => g x) = Finset.sum v' fun (b : β) => f b) (h₂ : ∀ (v : Finset β), ∃ (u : Finset γ), ∀ (u' : Finset γ), u ⊆ u' → ∃ (v' : Finset β), v ⊆ v' ∧ (Finset.sum v' fun (b : β) => f b) = Finset.sum u' fun (x : γ) => g x) : HasSum f a ↔ HasSum g a

theorem hasProd_iff_hasProd {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} {g : γ → α} (h₁ : ∀ (u : Finset γ), ∃ (v : Finset β), ∀ (v' : Finset β), v ⊆ v' → ∃ (u' : Finset γ), u ⊆ u' ∧ (Finset.prod u' fun (x : γ) => g x) = Finset.prod v' fun (b : β) => f b) (h₂ : ∀ (v : Finset β), ∃ (u : Finset γ), ∀ (u' : Finset γ), u ⊆ u' → ∃ (v' : Finset β), v ⊆ v' ∧ (Finset.prod v' fun (b : β) => f b) = Finset.prod u' fun (x : γ) => g x) : HasProd f a ↔ HasProd g a

theorem Function.Injective.summable_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {g : γ → β} (hg : Function.Injective g) (hf : ∀ x ∉ Set.range g, f x = 0) : Summable (f ∘ g) ↔ Summable f

theorem Function.Injective.multipliable_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] {f : β → α} {g : γ → β} (hg : Function.Injective g) (hf : ∀ x ∉ Set.range g, f x = 1) : Multipliable (f ∘ g) ↔ Multipliable f

@[simp]

theorem hasSum_extend_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} {g : β → γ} (hg : Function.Injective g) : HasSum (Function.extend g f 0) a ↔ HasSum f a

@[simp]

theorem hasProd_extend_one {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} {g : β → γ} (hg : Function.Injective g) : HasProd (Function.extend g f 1) a ↔ HasProd f a

@[simp]

theorem summable_extend_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {g : β → γ} (hg : Function.Injective g) : Summable (Function.extend g f 0) ↔ Summable f

@[simp]

theorem multipliable_extend_one {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] {f : β → α} {g : β → γ} (hg : Function.Injective g) : Multipliable (Function.extend g f 1) ↔ Multipliable f

theorem hasSum_subtype_iff_indicator {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} {s : Set β} : HasSum (f ∘ Subtype.val) a ↔ HasSum (Set.indicator s f) a

theorem hasProd_subtype_iff_mulIndicator {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} {s : Set β} : HasProd (f ∘ Subtype.val) a ↔ HasProd (Set.mulIndicator s f) a

theorem summable_subtype_iff_indicator {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {s : Set β} : Summable (f ∘ Subtype.val) ↔ Summable (Set.indicator s f)

theorem multipliable_subtype_iff_mulIndicator {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} {s : Set β} : Multipliable (f ∘ Subtype.val) ↔ Multipliable (Set.mulIndicator s f)

@[simp]

theorem hasSum_subtype_support {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} : HasSum (f ∘ Subtype.val) a ↔ HasSum f a

@[simp]

theorem hasProd_subtype_mulSupport {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} : HasProd (f ∘ Subtype.val) a ↔ HasProd f a

theorem Finset.summable {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (s : Finset β) (f : β → α) : Summable (f ∘ Subtype.val)

theorem Finset.multipliable {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] (s : Finset β) (f : β → α) : Multipliable (f ∘ Subtype.val)

theorem Set.Finite.summable {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {s : Set β} (hs : Set.Finite s) (f : β → α) : Summable (f ∘ Subtype.val)

theorem Set.Finite.multipliable {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {s : Set β} (hs : Set.Finite s) (f : β → α) : Multipliable (f ∘ Subtype.val)

theorem summable_of_finite_support {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} (h : Set.Finite (Function.support f)) : Summable f

theorem multipliable_of_finite_mulSupport {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} (h : Set.Finite (Function.mulSupport f)) : Multipliable f

theorem hasSum_single {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} (b : β) (hf : ∀ (b' : β), b' ≠ b → f b' = 0) : HasSum f (f b)

theorem hasProd_single {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} (b : β) (hf : ∀ (b' : β), b' ≠ b → f b' = 1) : HasProd f (f b)

@[simp]

theorem hasSum_unique {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [Unique β] (f : β → α) : HasSum f (f default)

@[simp]

theorem hasProd_unique {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] [Unique β] (f : β → α) : HasProd f (f default)

@[simp]

theorem hasSum_singleton {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (m : β) (f : β → α) : HasSum (Set.restrict {m} f) (f m)

@[simp]

theorem hasProd_singleton {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] (m : β) (f : β → α) : HasProd (Set.restrict {m} f) (f m)

theorem hasSum_ite_eq {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (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} [CommMonoid α] [TopologicalSpace α] (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} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} (e : γ ≃ β) : HasSum (f ∘ ⇑e) a ↔ HasSum f a

theorem Equiv.hasProd_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] {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} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} {g : γ → β} (hg : Function.Injective g) : 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} [CommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} {g : γ → β} (hg : Function.Injective g) : 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} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} (e : γ ≃ β) : Summable (f ∘ ⇑e) ↔ Summable f

theorem Equiv.multipliable_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] {f : β → α} (e : γ ≃ β) : Multipliable (f ∘ ⇑e) ↔ Multipliable f

theorem Equiv.hasSum_iff_of_support {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} {g : γ → α} (e : ↑(Function.support f) ≃ ↑(Function.support g)) (he : ∀ (x : ↑(Function.support f)), 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} [CommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} {g : γ → α} (e : ↑(Function.mulSupport f) ≃ ↑(Function.mulSupport g)) (he : ∀ (x : ↑(Function.mulSupport f)), g ↑(e x) = f ↑x) : HasProd f a ↔ HasProd g a

theorem hasSum_iff_hasSum_of_ne_zero_bij {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} {g : γ → α} (i : ↑(Function.support g) → β) (hi : Function.Injective i) (hf : Function.support f ⊆ Set.range i) (hfg : ∀ (x : ↑(Function.support g)), 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} [CommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} {g : γ → α} (i : ↑(Function.mulSupport g) → β) (hi : Function.Injective i) (hf : Function.mulSupport f ⊆ Set.range i) (hfg : ∀ (x : ↑(Function.mulSupport g)), f (i x) = g ↑x) : HasProd f a ↔ HasProd g a

theorem Equiv.summable_iff_of_support {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {g : γ → α} (e : ↑(Function.support f) ≃ ↑(Function.support g)) (he : ∀ (x : ↑(Function.support f)), g ↑(e x) = f ↑x) : Summable f ↔ Summable g

theorem Equiv.multipliable_iff_of_mulSupport {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] {f : β → α} {g : γ → α} (e : ↑(Function.mulSupport f) ≃ ↑(Function.mulSupport g)) (he : ∀ (x : ↑(Function.mulSupport f)), g ↑(e x) = f ↑x) : Multipliable f ↔ Multipliable g

theorem HasSum.map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} [AddCommMonoid γ] [TopologicalSpace γ] (hf : HasSum f a) {G : Type u_5} [FunLike G α γ] [AddMonoidHomClass G α γ] (g : G) (hg : Continuous ⇑g) : HasSum (⇑g ∘ f) (g a)

theorem HasProd.map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} [CommMonoid γ] [TopologicalSpace γ] (hf : HasProd f a) {G : Type u_5} [FunLike G α γ] [MonoidHomClass G α γ] (g : G) (hg : Continuous ⇑g) : HasProd (⇑g ∘ f) (g a)

theorem Summable.map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} [AddCommMonoid γ] [TopologicalSpace γ] (hf : Summable f) {G : Type u_5} [FunLike G α γ] [AddMonoidHomClass G α γ] (g : G) (hg : Continuous ⇑g) : Summable (⇑g ∘ f)

theorem Multipliable.map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] {f : β → α} [CommMonoid γ] [TopologicalSpace γ] (hf : Multipliable f) {G : Type u_5} [FunLike G α γ] [MonoidHomClass G α γ] (g : G) (hg : Continuous ⇑g) : Multipliable (⇑g ∘ f)

theorem Summable.map_iff_of_leftInverse {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} [AddCommMonoid γ] [TopologicalSpace γ] {G : Type u_5} {G' : Type u_6} [FunLike G α γ] [AddMonoidHomClass G α γ] [FunLike G' γ α] [AddMonoidHomClass G' γ α] (g : G) (g' : G') (hg : Continuous ⇑g) (hg' : Continuous ⇑g') (hinv : Function.LeftInverse ⇑g' ⇑g) : Summable (⇑g ∘ f) ↔ Summable f

theorem Multipliable.map_iff_of_leftInverse {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] {f : β → α} [CommMonoid γ] [TopologicalSpace γ] {G : Type u_5} {G' : Type u_6} [FunLike G α γ] [MonoidHomClass G α γ] [FunLike G' γ α] [MonoidHomClass G' γ α] (g : G) (g' : G') (hg : Continuous ⇑g) (hg' : Continuous ⇑g') (hinv : Function.LeftInverse ⇑g' ⇑g) : Multipliable (⇑g ∘ f) ↔ Multipliable f

theorem Summable.map_iff_of_equiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} [AddCommMonoid γ] [TopologicalSpace γ] {G : Type u_5} [EquivLike G α γ] [AddEquivClass G α γ] (g : G) (hg : Continuous ⇑g) (hg' : Continuous (EquivLike.inv g)) : Summable (⇑g ∘ f) ↔ Summable 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} [CommMonoid α] [TopologicalSpace α] {f : β → α} [CommMonoid γ] [TopologicalSpace γ] {G : Type u_5} [EquivLike G α γ] [MulEquivClass G α γ] (g : G) (hg : Continuous ⇑g) (hg' : Continuous (EquivLike.inv g)) : Multipliable (⇑g ∘ f) ↔ Multipliable 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} [AddCommMonoid α] [TopologicalSpace α] {α' : Type u_5} [AddCommMonoid α'] [TopologicalSpace α'] {e : α' → α} (hes : Function.Surjective e) {f : β → α} {g : γ → α'} (he : ∀ {a : α'}, HasSum f (e a) ↔ HasSum g a) : Summable f ↔ Summable g

theorem Function.Surjective.multipliable_iff_of_hasProd_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] {α' : Type u_5} [CommMonoid α'] [TopologicalSpace α'] {e : α' → α} (hes : Function.Surjective e) {f : β → α} {g : γ → α'} (he : ∀ {a : α'}, HasProd f (e a) ↔ HasProd g a) : Multipliable f ↔ Multipliable g

theorem HasSum.add {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {g : β → α} {a : α} {b : α} [ContinuousAdd α] (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} [CommMonoid α] [TopologicalSpace α] {f : β → α} {g : β → α} {a : α} {b : α} [ContinuousMul α] (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} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {g : β → α} [ContinuousAdd α] (hf : Summable f) (hg : Summable g) : Summable fun (b : β) => f b + g b

theorem Multipliable.mul {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} {g : β → α} [ContinuousMul α] (hf : Multipliable f) (hg : Multipliable g) : Multipliable fun (b : β) => f b * g b

theorem hasSum_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] [ContinuousAdd α] {f : γ → β → α} {a : γ → α} {s : Finset γ} : (∀ i ∈ s, HasSum (f i) (a i)) → HasSum (fun (b : β) => Finset.sum s fun (i : γ) => f i b) (Finset.sum s fun (i : γ) => a i)

theorem hasProd_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] [ContinuousMul α] {f : γ → β → α} {a : γ → α} {s : Finset γ} : (∀ i ∈ s, HasProd (f i) (a i)) → HasProd (fun (b : β) => Finset.prod s fun (i : γ) => f i b) (Finset.prod s fun (i : γ) => a i)

theorem summable_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] [ContinuousAdd α] {f : γ → β → α} {s : Finset γ} (hf : ∀ i ∈ s, Summable (f i)) : Summable fun (b : β) => Finset.sum s fun (i : γ) => f i b

theorem multipliable_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] [ContinuousMul α] {f : γ → β → α} {s : Finset γ} (hf : ∀ i ∈ s, Multipliable (f i)) : Multipliable fun (b : β) => Finset.prod s fun (i : γ) => f i b

theorem HasSum.add_disjoint {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} {b : α} [ContinuousAdd α] {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} [CommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} {b : α} [ContinuousMul α] {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} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} [ContinuousAdd α] {ι : Type u_5} (s : Finset ι) {t : ι → Set β} {a : ι → α} (hs : Set.Pairwise (↑s) (Disjoint on t)) (hf : ∀ i ∈ s, HasSum (f ∘ Subtype.val) (a i)) : HasSum (f ∘ Subtype.val) (Finset.sum s fun (i : ι) => a i)

theorem hasProd_prod_disjoint {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} [ContinuousMul α] {ι : Type u_5} (s : Finset ι) {t : ι → Set β} {a : ι → α} (hs : Set.Pairwise (↑s) (Disjoint on t)) (hf : ∀ i ∈ s, HasProd (f ∘ Subtype.val) (a i)) : HasProd (f ∘ Subtype.val) (Finset.prod s fun (i : ι) => a i)

theorem HasSum.add_isCompl {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} {b : α} [ContinuousAdd α] {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} [CommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} {b : α} [ContinuousMul α] {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} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} {b : α} [ContinuousAdd α] {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} [CommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} {b : α} [ContinuousMul α] {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} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} [ContinuousAdd α] {s : Set β} (hs : Summable (f ∘ Subtype.val)) (hsc : Summable (f ∘ Subtype.val)) : Summable f

theorem Multipliable.mul_compl {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} [ContinuousMul α] {s : Set β} (hs : Multipliable (f ∘ Subtype.val)) (hsc : Multipliable (f ∘ Subtype.val)) : Multipliable f

theorem HasSum.compl_add {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} {b : α} [ContinuousAdd α] {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} [CommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} {b : α} [ContinuousMul α] {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} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} [ContinuousAdd α] {s : Set β} (hs : Summable (f ∘ Subtype.val)) (hsc : Summable (f ∘ Subtype.val)) : Summable f

theorem Multipliable.compl_add {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} [ContinuousMul α] {s : Set β} (hs : Multipliable (f ∘ Subtype.val)) (hsc : Multipliable (f ∘ Subtype.val)) : Multipliable f

theorem HasSum.update' {α : Type u_5} {β : Type u_6} [TopologicalSpace α] [AddCommMonoid α] [T2Space α] [ContinuousAdd α] [DecidableEq β] {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} [TopologicalSpace α] [CommMonoid α] [T2Space α] [ContinuousMul α] [DecidableEq β] {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} [TopologicalSpace α] [AddCommMonoid α] [T2Space α] [ContinuousAdd α] [DecidableEq β] {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} [TopologicalSpace α] [CommMonoid α] [T2Space α] [ContinuousMul α] [DecidableEq β] {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} [AddCommMonoid α] [TopologicalSpace α] (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} [CommMonoid α] [TopologicalSpace α] (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} [AddCommMonoid α] [TopologicalSpace α] (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} [CommMonoid α] [TopologicalSpace α] (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} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} (hf : Set.Finite (Function.support f)) : ∑' (b : β), f b = finsum fun (b : β) => f b

theorem tprod_eq_finprod {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} (hf : Set.Finite (Function.mulSupport f)) : ∏' (b : β), f b = finprod fun (b : β) => f b

theorem tsum_eq_sum' {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {s : Finset β} (hf : Function.support f ⊆ ↑s) : ∑' (b : β), f b = Finset.sum s fun (b : β) => f b

theorem tprod_eq_prod' {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} {s : Finset β} (hf : Function.mulSupport f ⊆ ↑s) : ∏' (b : β), f b = Finset.prod s fun (b : β) => f b

theorem tsum_eq_sum {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {s : Finset β} (hf : ∀ b ∉ s, f b = 0) : ∑' (b : β), f b = Finset.sum s fun (b : β) => f b

theorem tprod_eq_prod {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} {s : Finset β} (hf : ∀ b ∉ s, f b = 1) : ∏' (b : β), f b = Finset.prod s fun (b : β) => f b

@[simp]

theorem tsum_zero {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] : ∑' (x : β), 0 = 0

@[simp]

theorem tprod_one {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] : ∏' (x : β), 1 = 1

@[simp]

theorem tsum_empty {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} [IsEmpty β] : ∑' (b : β), f b = 0

@[simp]

theorem tprod_empty {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} [IsEmpty β] : ∏' (b : β), f b = 1

theorem tsum_congr {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {g : β → α} (hfg : ∀ (b : β), f b = g b) : ∑' (b : β), f b = ∑' (b : β), g b

theorem tprod_congr {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} {g : β → α} (hfg : ∀ (b : β), f b = g b) : ∏' (b : β), f b = ∏' (b : β), g b

theorem tsum_fintype {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [Fintype β] (f : β → α) : ∑' (b : β), f b = Finset.sum Finset.univ fun (b : β) => f b

theorem tprod_fintype {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] [Fintype β] (f : β → α) : ∏' (b : β), f b = Finset.prod Finset.univ fun (b : β) => f b

theorem sum_eq_tsum_indicator {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (f : β → α) (s : Finset β) : (Finset.sum s fun (x : β) => f x) = ∑' (x : β), Set.indicator (↑s) f x

theorem prod_eq_tprod_mulIndicator {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] (f : β → α) (s : Finset β) : (Finset.prod s fun (x : β) => f x) = ∏' (x : β), Set.mulIndicator (↑s) f x

theorem tsum_bool {α : Type u_1} [AddCommMonoid α] [TopologicalSpace α] (f : Bool → α) : ∑' (i : Bool), f i = f false + f true

theorem tprod_bool {α : Type u_1} [CommMonoid α] [TopologicalSpace α] (f : Bool → α) : ∏' (i : Bool), f i = f false * f true

theorem tsum_eq_single {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} (b : β) (hf : ∀ (b' : β), b' ≠ b → f b' = 0) : ∑' (b : β), f b = f b

theorem tprod_eq_mulSingle {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} (b : β) (hf : ∀ (b' : β), b' ≠ b → f b' = 1) : ∏' (b : β), f b = f b

theorem tsum_tsum_eq_single {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] (f : β → γ → α) (b : β) (c : γ) (hfb : ∀ (b' : β), b' ≠ b → f b' c = 0) (hfc : ∀ (b' : β) (c' : γ), c' ≠ c → f 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} [CommMonoid α] [TopologicalSpace α] (f : β → γ → α) (b : β) (c : γ) (hfb : ∀ (b' : β), b' ≠ b → f b' c = 1) (hfc : ∀ (b' : β) (c' : γ), c' ≠ c → f b' c' = 1) : ∏' (b' : β) (c' : γ), f b' c' = f b c

@[simp]

theorem tsum_ite_eq {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (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} [CommMonoid α] [TopologicalSpace α] (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} [AddCommMonoid α] [TopologicalSpace α] (s : Finset β) (f : β → α) : ∑' (x : { x : β // x ∈ s }), f ↑x = Finset.sum s fun (x : β) => f x

@[simp]

theorem Finset.tprod_subtype {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] (s : Finset β) (f : β → α) : ∏' (x : { x : β // x ∈ s }), f ↑x = Finset.prod s fun (x : β) => f x

theorem Finset.tsum_subtype' {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (s : Finset β) (f : β → α) : ∑' (x : ↑↑s), f ↑x = Finset.sum s fun (x : β) => f x

theorem Finset.tprod_subtype' {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] (s : Finset β) (f : β → α) : ∏' (x : ↑↑s), f ↑x = Finset.prod s fun (x : β) => f x

@[simp]

theorem tsum_singleton {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (b : β) (f : β → α) : ∑' (x : ↑{b}), f ↑x = f b

@[simp]

theorem tprod_singleton {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] (b : β) (f : β → α) : ∏' (x : ↑{b}), f ↑x = f b

theorem Function.Injective.tsum_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {g : γ → β} (hg : Function.Injective g) {f : β → α} (hf : Function.support f ⊆ Set.range g) : ∑' (c : γ), f (g c) = ∑' (b : β), f b

theorem Function.Injective.tprod_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] {g : γ → β} (hg : Function.Injective g) {f : β → α} (hf : Function.mulSupport f ⊆ Set.range g) : ∏' (c : γ), f (g c) = ∏' (b : β), f b

theorem Equiv.tsum_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] (e : γ ≃ β) (f : β → α) : ∑' (c : γ), f (e c) = ∑' (b : β), f b

theorem Equiv.tprod_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] (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} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {s : Set β} (hs : Function.support f ⊆ s) : ∑' (x : ↑s), f ↑x = ∑' (x : β), f x

theorem tprod_subtype_eq_of_mulSupport_subset {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} {s : Set β} (hs : Function.mulSupport f ⊆ s) : ∏' (x : ↑s), f ↑x = ∏' (x : β), f x

theorem tsum_subtype_support {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (f : β → α) : ∑' (x : ↑(Function.support f)), f ↑x = ∑' (x : β), f x

theorem tprod_subtype_mulSupport {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] (f : β → α) : ∏' (x : ↑(Function.mulSupport f)), f ↑x = ∏' (x : β), f x

theorem tsum_subtype {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (s : Set β) (f : β → α) : ∑' (x : ↑s), f ↑x = ∑' (x : β), Set.indicator s f x

theorem tprod_subtype {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] (s : Set β) (f : β → α) : ∏' (x : ↑s), f ↑x = ∏' (x : β), Set.mulIndicator s f x

@[simp]

theorem tsum_univ {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (f : β → α) : ∑' (x : ↑Set.univ), f ↑x = ∑' (x : β), f x

@[simp]

theorem tprod_univ {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] (f : β → α) : ∏' (x : ↑Set.univ), f ↑x = ∏' (x : β), f x

theorem tsum_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {g : γ → β} (f : β → α) {s : Set γ} (hg : Set.InjOn g s) : ∑' (x : ↑(g '' s)), f ↑x = ∑' (x : ↑s), f (g ↑x)

theorem tprod_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] {g : γ → β} (f : β → α) {s : Set γ} (hg : Set.InjOn g s) : ∏' (x : ↑(g '' s)), f ↑x = ∏' (x : ↑s), f (g ↑x)

theorem tsum_range {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {g : γ → β} (f : β → α) (hg : Function.Injective g) : ∑' (x : ↑(Set.range g)), f ↑x = ∑' (x : γ), f (g x)

theorem tprod_range {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] {g : γ → β} (f : β → α) (hg : Function.Injective g) : ∏' (x : ↑(Set.range g)), f ↑x = ∏' (x : γ), f (g x)

theorem tsum_setElem_eq_tsum_setElem_diff {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} (s : Set β) (t : Set β) (hf₀ : ∀ b ∈ t, 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} [CommMonoid α] [TopologicalSpace α] {f : β → α} (s : Set β) (t : Set β) (hf₀ : ∀ b ∈ t, 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} [AddCommMonoid α] [TopologicalSpace α] {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} [CommMonoid α] [TopologicalSpace α] {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} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {g : γ → α} (i : ↑(Function.support g) → β) (hi : Function.Injective i) (hf : Function.support f ⊆ Set.range i) (hfg : ∀ (x : ↑(Function.support g)), 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} [CommMonoid α] [TopologicalSpace α] {f : β → α} {g : γ → α} (i : ↑(Function.mulSupport g) → β) (hi : Function.Injective i) (hf : Function.mulSupport f ⊆ Set.range i) (hfg : ∀ (x : ↑(Function.mulSupport g)), 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} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {g : γ → α} (e : ↑(Function.support f) ≃ ↑(Function.support g)) (he : ∀ (x : ↑(Function.support f)), 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} [CommMonoid α] [TopologicalSpace α] {f : β → α} {g : γ → α} (e : ↑(Function.mulSupport f) ≃ ↑(Function.mulSupport g)) (he : ∀ (x : ↑(Function.mulSupport f)), g ↑(e x) = f ↑x) : ∏' (x : β), f x = ∏' (y : γ), g y

theorem tsum_dite_right {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (P : Prop) [Decidable P] (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} [CommMonoid α] [TopologicalSpace α] (P : Prop) [Decidable P] (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} [AddCommMonoid α] [TopologicalSpace α] (P : Prop) [Decidable P] (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} [CommMonoid α] [TopologicalSpace α] (P : Prop) [Decidable P] (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} [AddCommMonoid α] [TopologicalSpace α] {γ : Type u_5} {g : γ → β} (hg : Function.Injective g) (f : γ → α) : ∑' (y : β), Function.extend g f 0 y = ∑' (x : γ), f x

@[simp]

theorem tprod_extend_one {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {γ : Type u_5} {g : γ → β} (hg : Function.Injective g) (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} [AddCommMonoid α] [TopologicalSpace α] [T2Space α] {α' : Type u_5} [AddCommMonoid α'] [TopologicalSpace α'] {e : α' → α} (hes : Function.Surjective e) (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} [CommMonoid α] [TopologicalSpace α] [T2Space α] {α' : Type u_5} [CommMonoid α'] [TopologicalSpace α'] {e : α' → α} (hes : Function.Surjective e) (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} [AddCommMonoid α] [TopologicalSpace α] [T2Space α] {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} [CommMonoid α] [TopologicalSpace α] [T2Space α] {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} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {g : β → α} [T2Space α] [ContinuousAdd α] (hf : Summable f) (hg : Summable g) : ∑' (b : β), (f b + g b) = ∑' (b : β), f b + ∑' (b : β), g b

theorem tprod_mul {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} {g : β → α} [T2Space α] [ContinuousMul α] (hf : Multipliable f) (hg : Multipliable g) : ∏' (b : β), f b * g b = (∏' (b : β), f b) * ∏' (b : β), g b

theorem tsum_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] [T2Space α] [ContinuousAdd α] {f : γ → β → α} {s : Finset γ} (hf : ∀ i ∈ s, Summable (f i)) : (∑' (b : β), Finset.sum s fun (i : γ) => f i b) = Finset.sum s fun (i : γ) => ∑' (b : β), f i b

theorem tprod_of_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] [T2Space α] [ContinuousMul α] {f : γ → β → α} {s : Finset γ} (hf : ∀ i ∈ s, Multipliable (f i)) : (∏' (b : β), Finset.prod s fun (i : γ) => f i b) = Finset.prod s fun (i : γ) => ∏' (b : β), f i b

theorem tsum_eq_add_tsum_ite' {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [T2Space α] [ContinuousAdd α] [DecidableEq β] {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} [CommMonoid α] [TopologicalSpace α] [T2Space α] [ContinuousMul α] [DecidableEq β] {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} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} [T2Space α] [ContinuousAdd α] {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} [CommMonoid α] [TopologicalSpace α] {f : β → α} [T2Space α] [ContinuousMul α] {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} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} [T2Space α] [ContinuousAdd α] {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} [CommMonoid α] [TopologicalSpace α] {f : β → α} [T2Space α] [ContinuousMul α] {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} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} [T2Space α] [ContinuousAdd α] {ι : Type u_5} {s : Finset ι} {t : ι → Set β} (hd : Set.Pairwise (↑s) (Disjoint on t)) (hf : ∀ i ∈ s, Summable (f ∘ Subtype.val)) : ∑' (x : ↑(⋃ i ∈ s, t i)), f ↑x = Finset.sum s fun (i : ι) => ∑' (x : ↑(t i)), f ↑x

theorem tprod_finset_bUnion_disjoint {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} [T2Space α] [ContinuousMul α] {ι : Type u_5} {s : Finset ι} {t : ι → Set β} (hd : Set.Pairwise (↑s) (Disjoint on t)) (hf : ∀ i ∈ s, Multipliable (f ∘ Subtype.val)) : ∏' (x : ↑(⋃ i ∈ s, t i)), f ↑x = Finset.prod s fun (i : ι) => ∏' (x : ↑(t i)), f ↑x