# 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`.

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

Constant one function has product `1`

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

Constant zero function has sum `0`

source
theorem hasProd_empty {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} {L : SummationFilter β} [IsEmpty β] :
HasProd f 1 L
source
theorem hasSum_empty {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {L : SummationFilter β} [IsEmpty β] :
HasSum f 0 L
source
theorem HasProd.of_subsingleton_cod {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} {L : SummationFilter β} [Subsingleton α] :
HasProd f 1 L
source
theorem HasSum.of_subsingleton_cod {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {L : SummationFilter β} [Subsingleton α] :
HasSum f 0 L
source
theorem multipliable_one {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {L : SummationFilter β} :
Multipliable (fun (x : β) => 1) L
source
theorem summable_zero {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {L : SummationFilter β} :
Summable (fun (x : β) => 0) L
source
theorem multipliable_empty {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} {L : SummationFilter β} [IsEmpty β] :
Multipliable f L
source
theorem summable_empty {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {L : SummationFilter β} [IsEmpty β] :
Summable f L
source
theorem Multipliable.of_subsingleton_cod {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} {L : SummationFilter β} [Subsingleton α] :
Multipliable f L
source
theorem Summable.of_subsingleton_cod {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {L : SummationFilter β} [Subsingleton α] :
Summable f L
source
theorem multipliable_congr {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f g : β → α} {L : SummationFilter β} (hfg : ∀ (b : β), f b = g b) :
Multipliable f L ↔ Multipliable g L

See `multipliable_congr_cofinite` for a version allowing the functions to disagree on a finite set.

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

See `summable_congr_cofinite` for a version allowing the functions to disagree on a finite set.

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

See `Multipliable.congr_cofinite` for a version allowing the functions to disagree on a finite set.

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

See `Summable.congr_cofinite` for a version allowing the functions to disagree on a finite set.

source
theorem HasProd.congr_fun {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f g : β → α} {a : α} {L : SummationFilter β} (hf : HasProd f a L) (h : ∀ (x : β), g x = f x) :
HasProd g a L
source
theorem HasSum.congr_fun {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f g : β → α} {a : α} {L : SummationFilter β} (hf : HasSum f a L) (h : ∀ (x : β), g x = f x) :
HasSum g a L
source
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' ∧ ∏ x ∈ u', g x = ∏ b ∈ v', f b) (hf : HasProd g a) :
HasProd f a
source
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' ∧ ∑ x ∈ u', g x = ∑ b ∈ v', f b) (hf : HasSum g a) :
HasSum f a
source
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' ∧ ∏ x ∈ u', g x = ∏ b ∈ v', f b) (h₂ : ∀ (v : Finset β), ∃ (u : Finset γ), ∀ (u' : Finset γ), u ⊆ u' → ∃ (v' : Finset β), v ⊆ v' ∧ ∏ b ∈ v', f b = ∏ x ∈ u', g x) :
HasProd f a ↔ HasProd g a
source
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' ∧ ∑ x ∈ u', g x = ∑ b ∈ v', f b) (h₂ : ∀ (v : Finset β), ∃ (u : Finset γ), ∀ (u' : Finset γ), u ⊆ u' → ∃ (v' : Finset β), v ⊆ v' ∧ ∑ b ∈ v', f b = ∑ x ∈ u', g x) :
HasSum f a ↔ HasSum g a
source
theorem Function.Injective.multipliable_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] {f : β → α} {g : γ → β} (hg : Injective g) (hf : ∀ x ∉ Set.range g, f x = 1) :
Multipliable (f ∘ g) ↔ Multipliable f
source
theorem Function.Injective.summable_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {g : γ → β} (hg : Injective g) (hf : ∀ x ∉ Set.range g, f x = 0) :
Summable (f ∘ g) ↔ Summable f
source
@[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
source
@[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
source
@[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
source
@[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
source
theorem hasProd_subtype_iff_mulIndicator {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} {s : Set β} :
HasProd (f ∘ Subtype.val) a ↔ HasProd (s.mulIndicator f) a
source
theorem hasSum_subtype_iff_indicator {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} {s : Set β} :
HasSum (f ∘ Subtype.val) a ↔ HasSum (s.indicator f) a
source
theorem multipliable_subtype_iff_mulIndicator {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} {s : Set β} :
Multipliable (f ∘ Subtype.val) ↔ Multipliable (s.mulIndicator f)
source
theorem summable_subtype_iff_indicator {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {s : Set β} :
Summable (f ∘ Subtype.val) ↔ Summable (s.indicator f)
source
@[simp]
theorem hasProd_subtype_mulSupport {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} :
HasProd (f ∘ Subtype.val) a ↔ HasProd f a
source
@[simp]
theorem hasSum_subtype_support {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} :
HasSum (f ∘ Subtype.val) a ↔ HasSum f a
source
theorem Finset.multipliable {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] (s : Finset β) (f : β → α) :
Multipliable (f ∘ Subtype.val)
source
theorem Finset.summable {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (s : Finset β) (f : β → α) :
Summable (f ∘ Subtype.val)
source
theorem Set.Finite.multipliable {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {s : Set β} (hs : s.Finite) (f : β → α) :
Multipliable (f ∘ Subtype.val)
source
theorem Set.Finite.summable {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {s : Set β} (hs : s.Finite) (f : β → α) :
Summable (f ∘ Subtype.val)
source
theorem multipliable_of_finite_mulSupport {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} {L : SummationFilter β} [L.HasSupport] (h : (Function.mulSupport f).Finite) :
Multipliable f L
source
theorem summable_of_finite_support {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {L : SummationFilter β} [L.HasSupport] (h : (Function.support f).Finite) :
Summable f L
source
theorem Multipliable.of_finite {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {L : SummationFilter β} [Finite β] [L.HasSupport] {f : β → α} :
Multipliable f L
source
theorem Summable.of_finite {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {L : SummationFilter β} [Finite β] [L.HasSupport] {f : β → α} :
Summable f L
source
theorem hasProd_single {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} (b : β) (hf : ∀ (b' : β), b' ≠ b → f b' = 1) (L : SummationFilter β := SummationFilter.unconditional β) [L.LeAtTop] :
HasProd f (f b) L
source
theorem hasSum_single {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} (b : β) (hf : ∀ (b' : β), b' ≠ b → f b' = 0) (L : SummationFilter β := SummationFilter.unconditional β) [L.LeAtTop] :
HasSum f (f b) L
source
@[simp]
theorem hasProd_unique {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] [Unique β] (f : β → α) (L : SummationFilter β := SummationFilter.unconditional β) [L.LeAtTop] :
HasProd f (f default) L
source
@[simp]
theorem hasSum_unique {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [Unique β] (f : β → α) (L : SummationFilter β := SummationFilter.unconditional β) [L.LeAtTop] :
HasSum f (f default) L
source
@[simp]
theorem hasProd_singleton {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] (m : β) (f : β → α) :
HasProd ({m}.restrict f) (f m)
source
@[simp]
theorem hasSum_singleton {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (m : β) (f : β → α) :
HasSum ({m}.restrict f) (f m)
source
theorem hasProd_ite_eq {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] (b : β) [DecidablePred fun (x : β) => x = b] (a : α) (L : SummationFilter β := SummationFilter.unconditional β) [L.LeAtTop] :
HasProd (fun (b' : β) => if b' = b then a else 1) a L
source
theorem hasSum_ite_eq {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (b : β) [DecidablePred fun (x : β) => x = b] (a : α) (L : SummationFilter β := SummationFilter.unconditional β) [L.LeAtTop] :
HasSum (fun (b' : β) => if b' = b then a else 0) a L
source
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
source
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
source
theorem Function.Injective.hasProd_range_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} {g : γ → β} (hg : Injective g) :
HasProd (fun (x : ↑(Set.range g)) => f ↑x) a ↔ HasProd (f ∘ g) a
source
theorem Function.Injective.hasSum_range_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} {g : γ → β} (hg : Injective g) :
HasSum (fun (x : ↑(Set.range g)) => f ↑x) a ↔ HasSum (f ∘ g) a
source
theorem Equiv.multipliable_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] {f : β → α} (e : γ ≃ β) :
Multipliable (f ∘ ⇑e) ↔ Multipliable f
source
theorem Equiv.summable_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} (e : γ ≃ β) :
Summable (f ∘ ⇑e) ↔ Summable f
source
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
source
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
source
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
source
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
source
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
source
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
source
theorem HasProd.map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} {L : SummationFilter β} [CommMonoid γ] [TopologicalSpace γ] (hf : HasProd f a L) {G : Type u_4} [FunLike G α γ] [MonoidHomClass G α γ] (g : G) (hg : Continuous ⇑g) :
HasProd (⇑g ∘ f) (g a) L
source
theorem HasSum.map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} {L : SummationFilter β} [AddCommMonoid γ] [TopologicalSpace γ] (hf : HasSum f a L) {G : Type u_4} [FunLike G α γ] [AddMonoidHomClass G α γ] (g : G) (hg : Continuous ⇑g) :
HasSum (⇑g ∘ f) (g a) L
source
theorem Topology.IsInducing.hasProd_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] {L : SummationFilter β} [CommMonoid γ] [TopologicalSpace γ] {G : Type u_4} [FunLike G α γ] [MonoidHomClass G α γ] {g : G} (hg : IsInducing ⇑g) (f : β → α) (a : α) :
HasProd (⇑g ∘ f) (g a) L ↔ HasProd f a L
source
theorem Topology.IsInducing.hasSum_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {L : SummationFilter β} [AddCommMonoid γ] [TopologicalSpace γ] {G : Type u_4} [FunLike G α γ] [AddMonoidHomClass G α γ] {g : G} (hg : IsInducing ⇑g) (f : β → α) (a : α) :
HasSum (⇑g ∘ f) (g a) L ↔ HasSum f a L
source
theorem Multipliable.map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] {f : β → α} {L : SummationFilter β} [CommMonoid γ] [TopologicalSpace γ] (hf : Multipliable f L) {G : Type u_4} [FunLike G α γ] [MonoidHomClass G α γ] (g : G) (hg : Continuous ⇑g) :
Multipliable (⇑g ∘ f) L
source
theorem Summable.map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {L : SummationFilter β} [AddCommMonoid γ] [TopologicalSpace γ] (hf : Summable f L) {G : Type u_4} [FunLike G α γ] [AddMonoidHomClass G α γ] (g : G) (hg : Continuous ⇑g) :
Summable (⇑g ∘ f) L
source
theorem Multipliable.map_iff_of_leftInverse {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] {f : β → α} {L : SummationFilter β} [CommMonoid γ] [TopologicalSpace γ] {G : Type u_4} {G' : Type u_5} [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) L ↔ Multipliable f L
source
theorem Summable.map_iff_of_leftInverse {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {L : SummationFilter β} [AddCommMonoid γ] [TopologicalSpace γ] {G : Type u_4} {G' : Type u_5} [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) L ↔ Summable f L
source
theorem Multipliable.map_tprod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] {f : β → α} {L : SummationFilter β} [L.NeBot] [CommMonoid γ] [TopologicalSpace γ] [T2Space γ] (hf : Multipliable f L) {G : Type u_4} [FunLike G α γ] [MonoidHomClass G α γ] (g : G) (hg : Continuous ⇑g) :
g (∏'[L] (i : β), f i) = ∏'[L] (i : β), g (f i)
source
theorem Summable.map_tsum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {L : SummationFilter β} [L.NeBot] [AddCommMonoid γ] [TopologicalSpace γ] [T2Space γ] (hf : Summable f L) {G : Type u_4} [FunLike G α γ] [AddMonoidHomClass G α γ] (g : G) (hg : Continuous ⇑g) :
g (∑'[L] (i : β), f i) = ∑'[L] (i : β), g (f i)
source
theorem Topology.IsClosedEmbedding.map_tprod {ι : Type u_4} {α : Type u_5} {α' : Type u_6} {G : Type u_7} [CommMonoid α] [CommMonoid α'] [TopologicalSpace α] [TopologicalSpace α'] [T2Space α'] (f : ι → α) {L : SummationFilter ι} {g : G} [FunLike G α α'] [MonoidHomClass G α α'] (hge : IsClosedEmbedding ⇑g) :
g (∏'[L] (i : ι), f i) = ∏'[L] (i : ι), g (f i)
source
theorem Topology.IsClosedEmbedding.map_tsum {ι : Type u_4} {α : Type u_5} {α' : Type u_6} {G : Type u_7} [AddCommMonoid α] [AddCommMonoid α'] [TopologicalSpace α] [TopologicalSpace α'] [T2Space α'] (f : ι → α) {L : SummationFilter ι} {g : G} [FunLike G α α'] [AddMonoidHomClass G α α'] (hge : IsClosedEmbedding ⇑g) :
g (∑'[L] (i : ι), f i) = ∑'[L] (i : ι), g (f i)
source
theorem Function.LeftInverse.map_tprod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] {L : SummationFilter β} {G : Type u_4} (f : β → α) [CommMonoid γ] [TopologicalSpace γ] [T2Space γ] {g : G} [FunLike G α γ] [MonoidHomClass G α γ] (hg : Continuous ⇑g) {g' : γ → α} (hg' : Continuous g') (hgg' : LeftInverse g' ⇑g) :
g (∏'[L] (b : β), f b) = ∏'[L] (b : β), g (f b)

Special case of `Topology.IsClosedEmbedding.map_tprod`, logically weaker but possibly easier to apply in practice.

source
theorem Function.LeftInverse.map_tsum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {L : SummationFilter β} {G : Type u_4} (f : β → α) [AddCommMonoid γ] [TopologicalSpace γ] [T2Space γ] {g : G} [FunLike G α γ] [AddMonoidHomClass G α γ] (hg : Continuous ⇑g) {g' : γ → α} (hg' : Continuous g') (hgg' : LeftInverse g' ⇑g) :
g (∑'[L] (b : β), f b) = ∑'[L] (b : β), g (f b)

Special case of `Topology.IsClosedEmbedding.map_tsum`, logically weaker but possibly easier to apply in practice.

source
theorem Topology.IsInducing.multipliable_iff_tprod_comp_mem_range {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] {L : SummationFilter β} [CommMonoid γ] [TopologicalSpace γ] [T2Space γ] {G : Type u_4} [FunLike G α γ] [MonoidHomClass G α γ] {g : G} (hg : IsInducing ⇑g) (f : β → α) :
Multipliable f L ↔ Multipliable (⇑g ∘ f) L ∧ ∏'[L] (i : β), g (f i) ∈ Set.range ⇑g
source
theorem Topology.IsInducing.summable_iff_tsum_comp_mem_range {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {L : SummationFilter β} [AddCommMonoid γ] [TopologicalSpace γ] [T2Space γ] {G : Type u_4} [FunLike G α γ] [AddMonoidHomClass G α γ] {g : G} (hg : IsInducing ⇑g) (f : β → α) :
Summable f L ↔ Summable (⇑g ∘ f) L ∧ ∑'[L] (i : β), g (f i) ∈ Set.range ⇑g
source
theorem Multipliable.map_iff_of_equiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] {f : β → α} {L : SummationFilter β} [CommMonoid γ] [TopologicalSpace γ] {G : Type u_4} [EquivLike G α γ] [MulEquivClass G α γ] (g : G) (hg : Continuous ⇑g) (hg' : Continuous (EquivLike.inv g)) :
Multipliable (⇑g ∘ f) L ↔ Multipliable f L

"A special case of `Multipliable.map_iff_of_leftInverse` for convenience"

source
theorem Summable.map_iff_of_equiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {L : SummationFilter β} [AddCommMonoid γ] [TopologicalSpace γ] {G : Type u_4} [EquivLike G α γ] [AddEquivClass G α γ] (g : G) (hg : Continuous ⇑g) (hg' : Continuous (EquivLike.inv g)) :
Summable (⇑g ∘ f) L ↔ Summable f L

A special case of `Summable.map_iff_of_leftInverse` for convenience

source
theorem Function.Surjective.multipliable_iff_of_hasProd_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] {α' : Type u_4} [CommMonoid α'] [TopologicalSpace α'] {e : α' → α} (hes : Surjective e) {f : β → α} {g : γ → α'} (he : ∀ {a : α'}, HasProd f (e a) ↔ HasProd g a) :
Multipliable f ↔ Multipliable g
source
theorem Function.Surjective.summable_iff_of_hasSum_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {α' : Type u_4} [AddCommMonoid α'] [TopologicalSpace α'] {e : α' → α} (hes : Surjective e) {f : β → α} {g : γ → α'} (he : ∀ {a : α'}, HasSum f (e a) ↔ HasSum g a) :
Summable f ↔ Summable g
source
theorem HasProd.mul {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f g : β → α} {a b : α} {L : SummationFilter β} [ContinuousMul α] (hf : HasProd f a L) (hg : HasProd g b L) :
HasProd (fun (b : β) => f b * g b) (a * b) L
source
theorem HasSum.add {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f g : β → α} {a b : α} {L : SummationFilter β} [ContinuousAdd α] (hf : HasSum f a L) (hg : HasSum g b L) :
HasSum (fun (b : β) => f b + g b) (a + b) L
source
theorem Multipliable.mul {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f g : β → α} {L : SummationFilter β} [ContinuousMul α] (hf : Multipliable f L) (hg : Multipliable g L) :
Multipliable (fun (b : β) => f b * g b) L
source
theorem Summable.add {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f g : β → α} {L : SummationFilter β} [ContinuousAdd α] (hf : Summable f L) (hg : Summable g L) :
Summable (fun (b : β) => f b + g b) L
source
theorem hasProd_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] {L : SummationFilter β} [ContinuousMul α] {f : γ → β → α} {a : γ → α} {s : Finset γ} :
(∀ i ∈ s, HasProd (f i) (a i) L) → HasProd (fun (b : β) => ∏ i ∈ s, f i b) (∏ i ∈ s, a i) L
source
theorem hasSum_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {L : SummationFilter β} [ContinuousAdd α] {f : γ → β → α} {a : γ → α} {s : Finset γ} :
(∀ i ∈ s, HasSum (f i) (a i) L) → HasSum (fun (b : β) => ∑ i ∈ s, f i b) (∑ i ∈ s, a i) L
source
theorem multipliable_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] {L : SummationFilter β} [ContinuousMul α] {f : γ → β → α} {s : Finset γ} (hf : ∀ i ∈ s, Multipliable (f i) L) :
Multipliable (fun (b : β) => ∏ i ∈ s, f i b) L
source
theorem summable_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {L : SummationFilter β} [ContinuousAdd α] {f : γ → β → α} {s : Finset γ} (hf : ∀ i ∈ s, Summable (f i) L) :
Summable (fun (b : β) => ∑ i ∈ s, f i b) L
source
theorem HasProd.mul_disjoint {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} {a b : α} [ContinuousMul α] {s t : Set β} (hs : Disjoint s t) (ha : HasProd (f ∘ Subtype.val) a) (hb : HasProd (f ∘ Subtype.val) b) :
HasProd (f ∘ Subtype.val) (a * b)
source
theorem HasSum.add_disjoint {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {a b : α} [ContinuousAdd α] {s t : Set β} (hs : Disjoint s t) (ha : HasSum (f ∘ Subtype.val) a) (hb : HasSum (f ∘ Subtype.val) b) :
HasSum (f ∘ Subtype.val) (a + b)
source
theorem hasProd_prod_disjoint {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} [ContinuousMul α] {ι : Type u_4} (s : Finset ι) {t : ι → Set β} {a : ι → α} (hs : (↑s).Pairwise (Function.onFun Disjoint t)) (hf : ∀ i ∈ s, HasProd (f ∘ Subtype.val) (a i)) :
HasProd (f ∘ Subtype.val) (∏ i ∈ s, a i)
source
theorem hasSum_sum_disjoint {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} [ContinuousAdd α] {ι : Type u_4} (s : Finset ι) {t : ι → Set β} {a : ι → α} (hs : (↑s).Pairwise (Function.onFun Disjoint t)) (hf : ∀ i ∈ s, HasSum (f ∘ Subtype.val) (a i)) :
HasSum (f ∘ Subtype.val) (∑ i ∈ s, a i)
source
theorem HasProd.mul_isCompl {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} {a b : α} [ContinuousMul α] {s t : Set β} (hs : IsCompl s t) (ha : HasProd (f ∘ Subtype.val) a) (hb : HasProd (f ∘ Subtype.val) b) :
HasProd f (a * b)
source
theorem HasSum.add_isCompl {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {a b : α} [ContinuousAdd α] {s t : Set β} (hs : IsCompl s t) (ha : HasSum (f ∘ Subtype.val) a) (hb : HasSum (f ∘ Subtype.val) b) :
HasSum f (a + b)
source
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)
source
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)
source
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
source
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
source
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)
source
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)
source
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
source
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
source
theorem HasProd.update' {β : Type u_2} {L : SummationFilter β} [L.LeAtTop] [L.NeBot] {α : Type u_4} [TopologicalSpace α] [CommMonoid α] [T2Space α] [ContinuousMul α] [DecidableEq β] {f : β → α} {a a' : α} (hf : HasProd f a L) (b : β) (x : α) (hf' : HasProd (Function.update f b x) a' L) :
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.

source
theorem HasSum.update' {β : Type u_2} {L : SummationFilter β} [L.LeAtTop] [L.NeBot] {α : Type u_4} [TopologicalSpace α] [AddCommMonoid α] [T2Space α] [ContinuousAdd α] [DecidableEq β] {f : β → α} {a a' : α} (hf : HasSum f a L) (b : β) (x : α) (hf' : HasSum (Function.update f b x) a' L) :
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.

source
theorem eq_mul_of_hasProd_ite {β : Type u_2} {L : SummationFilter β} [L.LeAtTop] [L.NeBot] {α : Type u_4} [TopologicalSpace α] [CommMonoid α] [T2Space α] [ContinuousMul α] [DecidableEq β] {f : β → α} {a : α} (hf : HasProd f a L) (b : β) (a' : α) (hf' : HasProd (fun (n : β) => if n = b then 1 else f n) a' L) :
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.

source
theorem eq_add_of_hasSum_ite {β : Type u_2} {L : SummationFilter β} [L.LeAtTop] [L.NeBot] {α : Type u_4} [TopologicalSpace α] [AddCommMonoid α] [T2Space α] [ContinuousAdd α] [DecidableEq β] {f : β → α} {a : α} (hf : HasSum f a L) (b : β) (a' : α) (hf' : HasSum (fun (n : β) => if n = b then 0 else f n) a' L) :
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.

source
theorem tprod_congr_set_coe {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] (f : β → α) {s t : Set β} (h : s = t) :
∏' (x : ↑s), f ↑x = ∏' (x : ↑t), f ↑x
source
theorem tsum_congr_set_coe {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (f : β → α) {s t : Set β} (h : s = t) :
∑' (x : ↑s), f ↑x = ∑' (x : ↑t), f ↑x
source
theorem tprod_congr_subtype {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] (f : β → α) {P Q : β → Prop} (h : ∀ (x : β), P x ↔ Q x) :
∏' (x : { x : β // P x }), f ↑x = ∏' (x : { x : β // Q x }), f ↑x
source
theorem tsum_congr_subtype {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (f : β → α) {P Q : β → Prop} (h : ∀ (x : β), P x ↔ Q x) :
∑' (x : { x : β // P x }), f ↑x = ∑' (x : { x : β // Q x }), f ↑x
source
theorem tprod_eq_finprod {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} {L : SummationFilter β} [L.LeAtTop] (hf : (Function.mulSupport f).Finite) :
∏'[L] (b : β), f b = ∏ᶠ (b : β), f b
source
theorem tsum_eq_finsum {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {L : SummationFilter β} [L.LeAtTop] (hf : (Function.support f).Finite) :
∑'[L] (b : β), f b = ∑ᶠ (b : β), f b
source
theorem tprod_eq_prod' {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} {L : SummationFilter β} [L.LeAtTop] {s : Finset β} (hf : Function.mulSupport f ⊆ ↑s) :
∏'[L] (b : β), f b = ∏ b ∈ s, f b
source
theorem tsum_eq_sum' {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {L : SummationFilter β} [L.LeAtTop] {s : Finset β} (hf : Function.support f ⊆ ↑s) :
∑'[L] (b : β), f b = ∑ b ∈ s, f b
source
theorem tprod_eq_prod {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} {L : SummationFilter β} [L.LeAtTop] {s : Finset β} (hf : ∀ b ∉ s, f b = 1) :
∏'[L] (b : β), f b = ∏ b ∈ s, f b
source
theorem tsum_eq_sum {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {L : SummationFilter β} [L.LeAtTop] {s : Finset β} (hf : ∀ b ∉ s, f b = 0) :
∑'[L] (b : β), f b = ∑ b ∈ s, f b
source
@[simp]
theorem tprod_one {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {L : SummationFilter β} :
∏'[L] (x : β), 1 = 1
source
@[simp]
theorem tsum_zero {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {L : SummationFilter β} :
∑'[L] (x : β), 0 = 0
source
@[simp]
theorem tprod_empty {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} {L : SummationFilter β} [IsEmpty β] :
∏'[L] (b : β), f b = 1
source
@[simp]
theorem tsum_empty {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {L : SummationFilter β} [IsEmpty β] :
∑'[L] (b : β), f b = 0
source
theorem tprod_congr {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {L : SummationFilter β} {f g : β → α} (hfg : ∀ (b : β), f b = g b) :
∏'[L] (b : β), f b = ∏'[L] (b : β), g b
source
theorem tsum_congr {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {L : SummationFilter β} {f g : β → α} (hfg : ∀ (b : β), f b = g b) :
∑'[L] (b : β), f b = ∑'[L] (b : β), g b
source
theorem tprod_congr₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] {L : SummationFilter β} {f g : β → γ → α} {M : SummationFilter γ} (hfg : ∀ (b : β) (c : γ), f b c = g b c) :
∏'[L] (b : β), ∏'[M] (c : γ), f b c = ∏'[L] (b : β), ∏'[M] (c : γ), g b c
source
theorem tsum_congr₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {L : SummationFilter β} {f g : β → γ → α} {M : SummationFilter γ} (hfg : ∀ (b : β) (c : γ), f b c = g b c) :
∑'[L] (b : β), ∑'[M] (c : γ), f b c = ∑'[L] (b : β), ∑'[M] (c : γ), g b c
source
theorem tprod_fintype {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {L : SummationFilter β} [L.LeAtTop] [Fintype β] (f : β → α) :
∏'[L] (b : β), f b = ∏ b : β, f b
source
theorem tsum_fintype {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {L : SummationFilter β} [L.LeAtTop] [Fintype β] (f : β → α) :
∑'[L] (b : β), f b = ∑ b : β, f b
source
theorem prod_eq_tprod_mulIndicator {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] (f : β → α) (s : Finset β) (L : SummationFilter β := SummationFilter.unconditional β) [L.LeAtTop] :
∏ x ∈ s, f x = ∏'[L] (x : β), (↑s).mulIndicator f x
source
theorem sum_eq_tsum_indicator {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (f : β → α) (s : Finset β) (L : SummationFilter β := SummationFilter.unconditional β) [L.LeAtTop] :
∑ x ∈ s, f x = ∑'[L] (x : β), (↑s).indicator f x
source
theorem tprod_bool {α : Type u_1} [CommMonoid α] [TopologicalSpace α] (f : Bool → α) :
∏' (i : Bool), f i = f false * f true
source
theorem tsum_bool {α : Type u_1} [AddCommMonoid α] [TopologicalSpace α] (f : Bool → α) :
∑' (i : Bool), f i = f false + f true
source
theorem tprod_eq_mulSingle {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {L : SummationFilter β} [L.LeAtTop] {f : β → α} (b : β) (hf : ∀ (b' : β), b' ≠ b → f b' = 1) :
∏'[L] (b : β), f b = f b
source
theorem tsum_eq_single {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {L : SummationFilter β} [L.LeAtTop] {f : β → α} (b : β) (hf : ∀ (b' : β), b' ≠ b → f b' = 0) :
∑'[L] (b : β), f b = f b
source
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
source
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
source
@[simp]
theorem tprod_ite_eq {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] (b : β) [DecidablePred fun (x : β) => x = b] (a : β → α) (L : SummationFilter β := SummationFilter.unconditional β) [L.LeAtTop] :
(∏'[L] (b' : β), if b' = b then a b' else 1) = a b
source
@[simp]
theorem tsum_ite_eq {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (b : β) [DecidablePred fun (x : β) => x = b] (a : β → α) (L : SummationFilter β := SummationFilter.unconditional β) [L.LeAtTop] :
(∑'[L] (b' : β), if b' = b then a b' else 0) = a b
source
@[simp]
theorem Finset.tprod_subtype {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] (s : Finset β) (f : β → α) :
∏' (x : { x : β // x ∈ s }), f ↑x = ∏ x ∈ s, f x
source
@[simp]
theorem Finset.tsum_subtype {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (s : Finset β) (f : β → α) :
∑' (x : { x : β // x ∈ s }), f ↑x = ∑ x ∈ s, f x
source
theorem Finset.tprod_subtype' {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] (s : Finset β) (f : β → α) :
∏' (x : ↑↑s), f ↑x = ∏ x ∈ s, f x
source
theorem Finset.tsum_subtype' {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (s : Finset β) (f : β → α) :
∑' (x : ↑↑s), f ↑x = ∑ x ∈ s, f x
source
@[simp]
theorem tprod_singleton {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] (b : β) (f : β → α) :
∏' (x : ↑{b}), f ↑x = f b
source
@[simp]
theorem tsum_singleton {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (b : β) (f : β → α) :
∑' (x : ↑{b}), f ↑x = f b
source
theorem Function.Injective.tprod_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] {g : γ → β} (hg : Injective g) {f : β → α} (hf : mulSupport f ⊆ Set.range g) :
∏' (c : γ), f (g c) = ∏' (b : β), f b
source
theorem Function.Injective.tsum_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {g : γ → β} (hg : Injective g) {f : β → α} (hf : support f ⊆ Set.range g) :
∑' (c : γ), f (g c) = ∑' (b : β), f b
source
theorem Equiv.tprod_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] (e : γ ≃ β) (f : β → α) :
∏' (c : γ), f (e c) = ∏' (b : β), f b
source
theorem Equiv.tsum_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] (e : γ ≃ β) (f : β → α) :
∑' (c : γ), f (e c) = ∑' (b : β), f b
source
@[simp]
theorem tprod_comp_neg {α : Type u_1} [CommMonoid α] [TopologicalSpace α] {β : Type u_4} [InvolutiveNeg β] (f : β → α) :
∏' (d : β), f (-d) = ∏' (d : β), f d
source
@[simp]
theorem tsum_comp_neg {α : Type u_1} [AddCommMonoid α] [TopologicalSpace α] {β : Type u_4} [InvolutiveNeg β] (f : β → α) :
∑' (d : β), f (-d) = ∑' (d : β), f d

### `tprod` on subsets - part 1 #

source
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
source
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
source
theorem tprod_subtype_mulSupport {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] (f : β → α) :
∏' (x : ↑(Function.mulSupport f)), f ↑x = ∏' (x : β), f x
source
theorem tsum_subtype_support {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (f : β → α) :
∑' (x : ↑(Function.support f)), f ↑x = ∑' (x : β), f x
source
theorem tprod_subtype {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] (s : Set β) (f : β → α) :
∏' (x : ↑s), f ↑x = ∏' (x : β), s.mulIndicator f x
source
theorem tsum_subtype {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (s : Set β) (f : β → α) :
∑' (x : ↑s), f ↑x = ∑' (x : β), s.indicator f x
source
@[simp]
theorem tprod_univ {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] (f : β → α) :
∏' (x : ↑Set.univ), f ↑x = ∏' (x : β), f x
source
@[simp]
theorem tsum_univ {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (f : β → α) :
∑' (x : ↑Set.univ), f ↑x = ∑' (x : β), f x
source
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)
source
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)
source
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)
source
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)
source
theorem tprod_setElem_eq_tprod_setElem_diff {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} (s 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`.

source
theorem tsum_setElem_eq_tsum_setElem_diff {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} (s 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`.

source
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}`.

source
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}`.

source
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
source
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
source
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
source
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
source
theorem tprod_dite_right {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {L : SummationFilter β} (P : Prop) [Decidable P] (x : β → ¬P → α) :
(∏'[L] (b : β), if h : P then 1 else x b h) = if h : P then 1 else ∏'[L] (b : β), x b h
source
theorem tsum_dite_right {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {L : SummationFilter β} (P : Prop) [Decidable P] (x : β → ¬P → α) :
(∑'[L] (b : β), if h : P then 0 else x b h) = if h : P then 0 else ∑'[L] (b : β), x b h
source
theorem tprod_dite_left {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {L : SummationFilter β} (P : Prop) [Decidable P] (x : β → P → α) :
(∏'[L] (b : β), if h : P then x b h else 1) = if h : P then ∏'[L] (b : β), x b h else 1
source
theorem tsum_dite_left {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {L : SummationFilter β} (P : Prop) [Decidable P] (x : β → P → α) :
(∑'[L] (b : β), if h : P then x b h else 0) = if h : P then ∑'[L] (b : β), x b h else 0
source
@[simp]
theorem tprod_extend_one {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {γ : Type u_4} {g : γ → β} (hg : Function.Injective g) (f : γ → α) :
∏' (y : β), Function.extend g f 1 y = ∏' (x : γ), f x
source
@[simp]
theorem tsum_extend_zero {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {γ : Type u_4} {g : γ → β} (hg : Function.Injective g) (f : γ → α) :
∑' (y : β), Function.extend g f 0 y = ∑' (x : γ), f x
source
theorem Function.Surjective.tprod_eq_tprod_of_hasProd_iff_hasProd {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] [T2Space α] {α' : Type u_4} [CommMonoid α'] [TopologicalSpace α'] {e : α' → α} (hes : Surjective e) (h1 : e 1 = 1) {f : β → α} {g : γ → α'} (h : ∀ {a : α'}, HasProd f (e a) ↔ HasProd g a) :
∏' (b : β), f b = e (∏' (c : γ), g c)
source
theorem Function.Surjective.tsum_eq_tsum_of_hasSum_iff_hasSum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] [T2Space α] {α' : Type u_4} [AddCommMonoid α'] [TopologicalSpace α'] {e : α' → α} (hes : Surjective e) (h1 : e 0 = 0) {f : β → α} {g : γ → α'} (h : ∀ {a : α'}, HasSum f (e a) ↔ HasSum g a) :
∑' (b : β), f b = e (∑' (c : γ), g c)
source
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
source
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
source
theorem Multipliable.tprod_mul {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f g : β → α} {L : SummationFilter β} [T2Space α] [ContinuousMul α] [L.NeBot] (hf : Multipliable f L) (hg : Multipliable g L) :
∏'[L] (b : β), f b * g b = (∏'[L] (b : β), f b) * ∏'[L] (b : β), g b
source
theorem Summable.tsum_add {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f g : β → α} {L : SummationFilter β} [T2Space α] [ContinuousAdd α] [L.NeBot] (hf : Summable f L) (hg : Summable g L) :
∑'[L] (b : β), (f b + g b) = ∑'[L] (b : β), f b + ∑'[L] (b : β), g b
source
theorem Multipliable.tprod_finsetProd {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] {L : SummationFilter β} [T2Space α] [ContinuousMul α] [L.NeBot] {f : γ → β → α} {s : Finset γ} (hf : ∀ i ∈ s, Multipliable (f i) L) :
∏'[L] (b : β), ∏ i ∈ s, f i b = ∏ i ∈ s, ∏'[L] (b : β), f i b
source
theorem Summable.tsum_finsetSum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {L : SummationFilter β} [T2Space α] [ContinuousAdd α] [L.NeBot] {f : γ → β → α} {s : Finset γ} (hf : ∀ i ∈ s, Summable (f i) L) :
∑'[L] (b : β), ∑ i ∈ s, f i b = ∑ i ∈ s, ∑'[L] (b : β), f i b
source
theorem Multipliable.tprod_eq_mul_tprod_ite' {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {L : SummationFilter β} [T2Space α] [ContinuousMul α] [DecidableEq β] [L.LeAtTop] [L.NeBot] {f : β → α} (b : β) (hf : Multipliable (Function.update f b 1) L) :
∏'[L] (x : β), f x = f b * ∏'[L] (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`.

source
theorem Summable.tsum_eq_add_tsum_ite' {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {L : SummationFilter β} [T2Space α] [ContinuousAdd α] [DecidableEq β] [L.LeAtTop] [L.NeBot] {f : β → α} (b : β) (hf : Summable (Function.update f b 0) L) :
∑'[L] (x : β), f x = f b + ∑'[L] (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`.

source
theorem Multipliable.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
source
theorem Summable.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
source
theorem Multipliable.tprod_union_disjoint {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} [T2Space α] [ContinuousMul α] {s 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
source
theorem Summable.tsum_union_disjoint {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} [T2Space α] [ContinuousAdd α] {s 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
source
theorem Multipliable.tprod_finset_bUnion_disjoint {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} [T2Space α] [ContinuousMul α] {ι : Type u_4} {s : Finset ι} {t : ι → Set β} (hd : (↑s).Pairwise (Function.onFun Disjoint t)) (hf : ∀ i ∈ s, Multipliable (f ∘ Subtype.val)) :
∏' (x : ↑(⋃ i ∈ s, t i)), f ↑x = ∏ i ∈ s, ∏' (x : ↑(t i)), f ↑x
source
theorem Summable.tsum_finset_bUnion_disjoint {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} [T2Space α] [ContinuousAdd α] {ι : Type u_4} {s : Finset ι} {t : ι → Set β} (hd : (↑s).Pairwise (Function.onFun Disjoint t)) (hf : ∀ i ∈ s, Summable (f ∘ Subtype.val)) :
∑' (x : ↑(⋃ i ∈ s, t i)), f ↑x = ∑ i ∈ s, ∑' (x : ↑(t i)), f ↑x
source
theorem hasProd_zero_of_exists_eq_zero {α : Type u_1} {β : Type u_2} [CommMonoidWithZero α] [TopologicalSpace α] {f : β → α} {L : SummationFilter β} (hf : ∃ (b : β), f b = 0) [L.LeAtTop] :
HasProd f 0 L
source
theorem multipliable_of_exists_eq_zero {α : Type u_1} {β : Type u_2} [CommMonoidWithZero α] [TopologicalSpace α] {f : β → α} {L : SummationFilter β} (hf : ∃ (b : β), f b = 0) [L.LeAtTop] :
Multipliable f L
source
theorem tprod_of_exists_eq_zero {α : Type u_1} {β : Type u_2} [CommMonoidWithZero α] [TopologicalSpace α] {f : β → α} {L : SummationFilter β} [T2Space α] [L.NeBot] [L.LeAtTop] (hf : ∃ (b : β), f b = 0) :
∏'[L] (b : β), f b = 0