Lemmas on infinite sums 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
hasSum_empty
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[TopologicalSpace α]
{f : β → α}
[IsEmpty β]
:
HasSum f 0
theorem
summable_zero
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[TopologicalSpace α]
:
Summable fun (x : β) => 0
theorem
summable_empty
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[TopologicalSpace α]
{f : β → α}
[IsEmpty β]
:
Summable f
theorem
summable_congr
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[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
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
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)
:
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)
:
@[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
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
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
summable_subtype_iff_indicator
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[TopologicalSpace α]
{f : β → α}
{s : Set β}
:
Summable (f ∘ Subtype.val) ↔ Summable (Set.indicator s f)
@[simp]
theorem
hasSum_subtype_support
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[TopologicalSpace α]
{f : β → α}
{a : α}
:
theorem
Finset.summable
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[TopologicalSpace α]
(s : Finset β)
(f : β → α)
:
theorem
Set.Finite.summable
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[TopologicalSpace α]
{s : Set β}
(hs : Set.Finite s)
(f : β → α)
:
theorem
summable_of_finite_support
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[TopologicalSpace α]
{f : β → α}
(h : Set.Finite (Function.support f))
:
Summable 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)
@[simp]
theorem
hasSum_unique
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[TopologicalSpace α]
[Unique β]
(f : β → α)
:
HasSum f (f default)
@[simp]
theorem
hasSum_singleton
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[TopologicalSpace α]
(m : β)
(f : β → α)
:
HasSum (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 : α)
:
theorem
Equiv.hasSum_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[AddCommMonoid α]
[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
Equiv.summable_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[AddCommMonoid α]
[TopologicalSpace α]
{f : β → α}
(e : γ ≃ β)
:
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
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
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
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
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
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
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
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
HasSum.add
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[TopologicalSpace α]
{f : β → α}
{g : β → α}
{a : α}
{b : α}
[ContinuousAdd α]
(hf : HasSum f a)
(hg : HasSum g b)
:
theorem
Summable.add
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[TopologicalSpace α]
{f : β → α}
{g : β → α}
[ContinuousAdd α]
(hf : Summable f)
(hg : Summable g)
:
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
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
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
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
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
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
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
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
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
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
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
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
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
tsum_eq_finsum
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[TopologicalSpace α]
{f : β → α}
(hf : Set.Finite (Function.support f))
:
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
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
@[simp]
theorem
tsum_zero
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[TopologicalSpace α]
:
∑' (x : β), 0 = 0
@[simp]
theorem
tsum_empty
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[TopologicalSpace α]
{f : β → α}
[IsEmpty β]
:
∑' (b : β), f b = 0
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
tsum_fintype
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[TopologicalSpace α]
[Fintype β]
(f : β → α)
:
∑' (b : β), f b = Finset.sum 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
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
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
@[simp]
theorem
tsum_ite_eq
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[TopologicalSpace α]
(b : β)
[DecidablePred fun (x : β) => x = b]
(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
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
@[simp]
theorem
tsum_singleton
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[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
Equiv.tsum_eq
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[AddCommMonoid α]
[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
tsum_subtype_support
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[TopologicalSpace α]
(f : β → α)
:
∑' (x : ↑(Function.support 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
@[simp]
theorem
tsum_univ
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[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
tsum_range
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[AddCommMonoid α]
[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 over f a with a ∈ s is the same as the
sum over 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 over f a with a ∈ s is the same as the sum over 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
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
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
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
@[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
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)
(h0 : e 0 = 0)
{f : β → α}
{g : γ → α'}
(h : ∀ {a : α'}, HasSum f (e a) ↔ HasSum 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
tsum_add
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[TopologicalSpace α]
{f : β → α}
{g : β → α}
[T2Space α]
[ContinuousAdd α]
(hf : Summable f)
(hg : Summable 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 : β), Finset.sum s fun (i : γ) => f i b) = Finset.sum 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))
:
Version of tsum_eq_add_tsum_ite for AddCommMonoid rather than AddCommGroup.
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
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
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