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 β]
:
theorem
summable_congr
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[TopologicalSpace α]
{f : β → α}
{g : β → α}
(hfg : ∀ (b : β), f b = g b)
:
theorem
multipliable_congr
{α : Type u_1}
{β : Type u_2}
[CommMonoid α]
[TopologicalSpace α]
{f : β → α}
{g : β → α}
(hfg : ∀ (b : β), f b = g b)
:
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)
:
theorem
HasSum.congr_fun
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[TopologicalSpace α]
{f : β → α}
{g : β → α}
{a : α}
(hf : HasSum f a)
(h : ∀ (x : β), g x = f x)
:
HasSum g a
theorem
HasProd.congr_fun
{α : Type u_1}
{β : Type u_2}
[CommMonoid α]
[TopologicalSpace α]
{f : β → α}
{g : β → α}
{a : α}
(hf : HasProd f a)
(h : ∀ (x : β), g x = f x)
:
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' ∧ ∑ x ∈ u', g x = ∑ b ∈ v', 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' ∧ ∏ x ∈ u', g x = ∏ b ∈ v', 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' ∧ ∑ 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)
:
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)
:
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)
:
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 β}
:
theorem
hasProd_subtype_iff_mulIndicator
{α : Type u_1}
{β : Type u_2}
[CommMonoid α]
[TopologicalSpace α]
{f : β → α}
{a : α}
{s : Set β}
:
theorem
summable_subtype_iff_indicator
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[TopologicalSpace α]
{f : β → α}
{s : Set β}
:
theorem
multipliable_subtype_iff_mulIndicator
{α : Type u_1}
{β : Type u_2}
[CommMonoid α]
[TopologicalSpace α]
{f : β → α}
{s : Set β}
:
Multipliable (f ∘ Subtype.val) ↔ Multipliable (s.mulIndicator f)
@[simp]
theorem
hasSum_subtype_support
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[TopologicalSpace α]
{f : β → α}
{a : α}
:
@[simp]
theorem
hasProd_subtype_mulSupport
{α : Type u_1}
{β : Type u_2}
[CommMonoid α]
[TopologicalSpace α]
{f : β → α}
{a : α}
:
theorem
Finset.summable
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[TopologicalSpace α]
(s : Finset β)
(f : β → α)
:
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 : s.Finite)
(f : β → α)
:
theorem
Set.Finite.multipliable
{α : Type u_1}
{β : Type u_2}
[CommMonoid α]
[TopologicalSpace α]
{s : Set β}
(hs : s.Finite)
(f : β → α)
:
Multipliable (f ∘ Subtype.val)
theorem
summable_of_finite_support
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[TopologicalSpace α]
{f : β → α}
(h : (Function.support f).Finite)
:
Summable f
theorem
multipliable_of_finite_mulSupport
{α : Type u_1}
{β : Type u_2}
[CommMonoid α]
[TopologicalSpace α]
{f : β → α}
(h : (Function.mulSupport f).Finite)
:
theorem
Summable.of_finite
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[TopologicalSpace α]
[Finite β]
{f : β → α}
:
Summable f
theorem
Multipliable.of_finite
{α : Type u_1}
{β : Type u_2}
[CommMonoid α]
[TopologicalSpace α]
[Finite β]
{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 ({m}.restrict f) (f m)
@[simp]
theorem
hasProd_singleton
{α : Type u_1}
{β : Type u_2}
[CommMonoid α]
[TopologicalSpace α]
(m : β)
(f : β → α)
:
HasProd ({m}.restrict f) (f m)
theorem
hasSum_ite_eq
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[TopologicalSpace α]
(b : β)
[DecidablePred fun (x : β) => x = b]
(a : α)
:
theorem
hasProd_ite_eq
{α : Type u_1}
{β : Type u_2}
[CommMonoid α]
[TopologicalSpace α]
(b : β)
[DecidablePred fun (x : β) => x = b]
(a : α)
:
theorem
Equiv.hasSum_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[AddCommMonoid α]
[TopologicalSpace α]
{f : β → α}
{a : α}
(e : γ ≃ β)
:
theorem
Equiv.hasProd_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[CommMonoid α]
[TopologicalSpace α]
{f : β → α}
{a : α}
(e : γ ≃ β)
:
theorem
Function.Injective.hasSum_range_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[AddCommMonoid α]
[TopologicalSpace α]
{f : β → α}
{a : α}
{g : γ → β}
(hg : Function.Injective g)
:
theorem
Function.Injective.hasProd_range_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[CommMonoid α]
[TopologicalSpace α]
{f : β → α}
{a : α}
{g : γ → β}
(hg : Function.Injective g)
:
theorem
Equiv.summable_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[AddCommMonoid α]
[TopologicalSpace α]
{f : β → α}
(e : γ ≃ β)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
theorem
Inducing.hasSum_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[AddCommMonoid α]
[TopologicalSpace α]
[AddCommMonoid γ]
[TopologicalSpace γ]
{G : Type u_5}
[FunLike G α γ]
[AddMonoidHomClass G α γ]
{g : G}
(hg : Inducing ⇑g)
(f : β → α)
(a : α)
:
theorem
Inducing.hasProd_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[CommMonoid α]
[TopologicalSpace α]
[CommMonoid γ]
[TopologicalSpace γ]
{G : Type u_5}
[FunLike G α γ]
[MonoidHomClass G α γ]
{g : G}
(hg : Inducing ⇑g)
(f : β → α)
(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)
:
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)
:
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_tsum
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[AddCommMonoid α]
[TopologicalSpace α]
{f : β → α}
[AddCommMonoid γ]
[TopologicalSpace γ]
[T2Space γ]
(hf : Summable f)
{G : Type u_5}
[FunLike G α γ]
[AddMonoidHomClass G α γ]
(g : G)
(hg : Continuous ⇑g)
:
g (∑' (i : β), f i) = ∑' (i : β), g (f i)
theorem
Multipliable.map_tprod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[CommMonoid α]
[TopologicalSpace α]
{f : β → α}
[CommMonoid γ]
[TopologicalSpace γ]
[T2Space γ]
(hf : Multipliable f)
{G : Type u_5}
[FunLike G α γ]
[MonoidHomClass G α γ]
(g : G)
(hg : Continuous ⇑g)
:
g (∏' (i : β), f i) = ∏' (i : β), g (f i)
theorem
Inducing.summable_iff_tsum_comp_mem_range
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[AddCommMonoid α]
[TopologicalSpace α]
[AddCommMonoid γ]
[TopologicalSpace γ]
[T2Space γ]
{G : Type u_5}
[FunLike G α γ]
[AddMonoidHomClass G α γ]
{g : G}
(hg : Inducing ⇑g)
(f : β → α)
:
theorem
Inducing.multipliable_iff_tprod_comp_mem_range
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[CommMonoid α]
[TopologicalSpace α]
[CommMonoid γ]
[TopologicalSpace γ]
[T2Space γ]
{G : Type u_5}
[FunLike G α γ]
[MonoidHomClass G α γ]
{g : G}
(hg : Inducing ⇑g)
(f : β → α)
:
Multipliable f ↔ Multipliable (⇑g ∘ f) ∧ ∏' (i : β), g (f i) ∈ Set.range ⇑g
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))
:
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)
:
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)
:
theorem
HasSum.add
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[TopologicalSpace α]
{f : β → α}
{g : β → α}
{a : α}
{b : α}
[ContinuousAdd α]
(hf : HasSum f a)
(hg : HasSum g 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)
:
theorem
Summable.add
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[TopologicalSpace α]
{f : β → α}
{g : β → α}
[ContinuousAdd α]
(hf : Summable f)
(hg : Summable g)
:
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 γ}
:
theorem
hasProd_prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[CommMonoid α]
[TopologicalSpace α]
[ContinuousMul α]
{f : γ → β → α}
{a : γ → α}
{s : Finset γ}
:
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 : β) => ∑ i ∈ s, 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 : β) => ∏ i ∈ s, 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)
:
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)
:
theorem
hasSum_sum_disjoint
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[TopologicalSpace α]
{f : β → α}
[ContinuousAdd α]
{ι : Type u_5}
(s : Finset ι)
{t : ι → Set β}
{a : ι → α}
(hs : (↑s).Pairwise (Disjoint on t))
(hf : ∀ i ∈ s, HasSum (f ∘ Subtype.val) (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 : (↑s).Pairwise (Disjoint on t))
(hf : ∀ i ∈ s, HasProd (f ∘ Subtype.val) (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)
:
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)
:
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)
:
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)
:
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))
:
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)
:
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)
:
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))
:
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')
:
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')
:
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')
:
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')
:
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 : (Function.support f).Finite)
:
∑' (b : β), f b = ∑ᶠ (b : β), f b
theorem
tprod_eq_finprod
{α : Type u_1}
{β : Type u_2}
[CommMonoid α]
[TopologicalSpace α]
{f : β → α}
(hf : (Function.mulSupport f).Finite)
:
∏' (b : β), f b = ∏ᶠ (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 = ∑ b ∈ s, 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 = ∏ b ∈ s, 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 = ∑ b ∈ s, 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 = ∏ b ∈ s, 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 = ∑ b : β, f b
theorem
tprod_fintype
{α : Type u_1}
{β : Type u_2}
[CommMonoid α]
[TopologicalSpace α]
[Fintype β]
(f : β → α)
:
∏' (b : β), f b = ∏ b : β, f b
theorem
sum_eq_tsum_indicator
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[TopologicalSpace α]
(f : β → α)
(s : Finset β)
:
∑ x ∈ s, f x = ∑' (x : β), (↑s).indicator f x
theorem
prod_eq_tprod_mulIndicator
{α : Type u_1}
{β : Type u_2}
[CommMonoid α]
[TopologicalSpace α]
(f : β → α)
(s : Finset β)
:
∏ x ∈ s, f x = ∏' (x : β), (↑s).mulIndicator f x
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 : α)
:
@[simp]
theorem
tprod_ite_eq
{α : Type u_1}
{β : Type u_2}
[CommMonoid α]
[TopologicalSpace α]
(b : β)
[DecidablePred fun (x : β) => x = b]
(a : α)
:
@[simp]
theorem
Finset.tsum_subtype
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[TopologicalSpace α]
(s : Finset β)
(f : β → α)
:
@[simp]
theorem
Finset.tprod_subtype
{α : Type u_1}
{β : Type u_2}
[CommMonoid α]
[TopologicalSpace α]
(s : Finset β)
(f : β → α)
:
theorem
Finset.tsum_subtype'
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[TopologicalSpace α]
(s : Finset β)
(f : β → α)
:
∑' (x : ↑↑s), f ↑x = ∑ x ∈ s, f x
theorem
Finset.tprod_subtype'
{α : Type u_1}
{β : Type u_2}
[CommMonoid α]
[TopologicalSpace α]
(s : Finset β)
(f : β → α)
:
∏' (x : ↑↑s), f ↑x = ∏ x ∈ s, 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
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 : β), s.indicator f x
theorem
tprod_subtype
{α : Type u_1}
{β : Type u_2}
[CommMonoid α]
[TopologicalSpace α]
(s : Set β)
(f : β → α)
:
∏' (x : ↑s), f ↑x = ∏' (x : β), s.mulIndicator 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)
:
theorem
tprod_image
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[CommMonoid α]
[TopologicalSpace α]
{g : γ → β}
(f : β → α)
{s : Set γ}
(hg : Set.InjOn g s)
:
theorem
tsum_range
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[AddCommMonoid α]
[TopologicalSpace α]
{g : γ → β}
(f : β → α)
(hg : Function.Injective g)
:
theorem
tprod_range
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[CommMonoid α]
[TopologicalSpace α]
{g : γ → β}
(f : β → α)
(hg : Function.Injective g)
:
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)
:
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)
:
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)
:
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)
:
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)
:
theorem
tprod_mul
{α : Type u_1}
{β : Type u_2}
[CommMonoid α]
[TopologicalSpace α]
{f : β → α}
{g : β → α}
[T2Space α]
[ContinuousMul α]
(hf : Multipliable f)
(hg : Multipliable g)
:
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 : β), ∑ i ∈ s, f i b = ∑ i ∈ s, ∑' (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 : β), ∏ i ∈ s, f i b = ∏ i ∈ s, ∏' (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))
:
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))
:
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))
:
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))
:
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))
:
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))
:
theorem
tsum_finset_bUnion_disjoint
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[TopologicalSpace α]
{f : β → α}
[T2Space α]
[ContinuousAdd α]
{ι : Type u_5}
{s : Finset ι}
{t : ι → Set β}
(hd : (↑s).Pairwise (Disjoint on t))
(hf : ∀ i ∈ s, Summable (f ∘ Subtype.val))
:
∑' (x : ↑(⋃ i ∈ s, t i)), f ↑x = ∑ i ∈ s, ∑' (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 : (↑s).Pairwise (Disjoint on t))
(hf : ∀ i ∈ s, Multipliable (f ∘ Subtype.val))
:
∏' (x : ↑(⋃ i ∈ s, t i)), f ↑x = ∏ i ∈ s, ∏' (x : ↑(t i)), f ↑x