Documentation

Mathlib.Topology.Algebra.InfiniteSum.Constructions

Topological sums and functorial constructions #

Lemmas on the interaction of tsum, HasSum etc with products, Sigma and Pi types, MulOpposite, etc.

Product, Sigma and Pi types #

theorem hasSum_pi_single {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [DecidableEq β] (b : β) (a : α) :
@[simp]
theorem tsum_pi_single {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [DecidableEq β] (b : β) (a : α) :
∑' (b' : β), Pi.single b a b' = a
theorem tsum_setProd_singleton_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] (b : β) (t : Set γ) (f : β × γα) :
∑' (x : ({b} ×ˢ t)), f x = ∑' (c : t), f (b, c)
theorem tsum_setProd_singleton_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] (s : Set β) (c : γ) (f : β × γα) :
∑' (x : (s ×ˢ {c})), f x = ∑' (b : s), f (b, c)
theorem Summable.prod_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : β × γα} (hf : Summable f) :
Summable fun (p : γ × β) => f (Prod.swap p)
theorem HasSum.prod_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] [AddCommMonoid γ] [TopologicalSpace γ] {f : βα} {g : βγ} {a : α} {b : γ} (hf : HasSum f a) (hg : HasSum g b) :
HasSum (fun (x : β) => (f x, g x)) (a, b)
theorem HasSum.sigma {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [ContinuousAdd α] [RegularSpace α] {γ : βType u_5} {f : (b : β) × γ bα} {g : βα} {a : α} (ha : HasSum f a) (hf : ∀ (b : β), HasSum (fun (c : γ b) => f { fst := b, snd := c }) (g b)) :
HasSum g a
theorem HasSum.prod_fiberwise {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] [ContinuousAdd α] [RegularSpace α] {f : β × γα} {g : βα} {a : α} (ha : HasSum f a) (hf : ∀ (b : β), HasSum (fun (c : γ) => f (b, c)) (g b)) :
HasSum g a

If a series f on β × γ has sum a and for each b the restriction of f to {b} × γ has sum g b, then the series g has sum a.

theorem Summable.sigma' {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [ContinuousAdd α] [RegularSpace α] {γ : βType u_5} {f : (b : β) × γ bα} (ha : Summable f) (hf : ∀ (b : β), Summable fun (c : γ b) => f { fst := b, snd := c }) :
Summable fun (b : β) => ∑' (c : γ b), f { fst := b, snd := c }
theorem HasSum.sigma_of_hasSum {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [ContinuousAdd α] [T3Space α] {γ : βType u_5} {f : (b : β) × γ bα} {g : βα} {a : α} (ha : HasSum g a) (hf : ∀ (b : β), HasSum (fun (c : γ b) => f { fst := b, snd := c }) (g b)) (hf' : Summable f) :
HasSum f a
theorem tsum_sigma' {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [ContinuousAdd α] [T3Space α] {γ : βType u_5} {f : (b : β) × γ bα} (h₁ : ∀ (b : β), Summable fun (c : γ b) => f { fst := b, snd := c }) (h₂ : Summable f) :
∑' (p : (b : β) × γ b), f p = ∑' (b : β) (c : γ b), f { fst := b, snd := c }
theorem tsum_prod' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] [ContinuousAdd α] [T3Space α] {f : β × γα} (h : Summable f) (h₁ : ∀ (b : β), Summable fun (c : γ) => f (b, c)) :
∑' (p : β × γ), f p = ∑' (b : β) (c : γ), f (b, c)
theorem tsum_comm' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] [ContinuousAdd α] [T3Space α] {f : βγα} (h : Summable (Function.uncurry f)) (h₁ : ∀ (b : β), Summable (f b)) (h₂ : ∀ (c : γ), Summable fun (b : β) => f b c) :
∑' (c : γ) (b : β), f b c = ∑' (b : β) (c : γ), f b c
theorem Summable.sigma_factor {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [UniformAddGroup α] [CompleteSpace α] {γ : βType u_5} {f : (b : β) × γ bα} (ha : Summable f) (b : β) :
Summable fun (c : γ b) => f { fst := b, snd := c }
theorem Summable.sigma {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [UniformAddGroup α] [CompleteSpace α] {γ : βType u_5} {f : (b : β) × γ bα} (ha : Summable f) :
Summable fun (b : β) => ∑' (c : γ b), f { fst := b, snd := c }
theorem Summable.prod_factor {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommGroup α] [UniformSpace α] [UniformAddGroup α] [CompleteSpace α] {f : β × γα} (h : Summable f) (b : β) :
Summable fun (c : γ) => f (b, c)
theorem HasSum.tsum_fiberwise {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommGroup α] [UniformSpace α] [UniformAddGroup α] [CompleteSpace α] [T2Space α] {f : βα} {a : α} (hf : HasSum f a) (g : βγ) :
HasSum (fun (c : γ) => ∑' (b : (g ⁻¹' {c})), f b) a
theorem tsum_sigma {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [UniformAddGroup α] [CompleteSpace α] [T0Space α] {γ : βType u_5} {f : (b : β) × γ bα} (ha : Summable f) :
∑' (p : (b : β) × γ b), f p = ∑' (b : β) (c : γ b), f { fst := b, snd := c }
theorem tsum_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommGroup α] [UniformSpace α] [UniformAddGroup α] [CompleteSpace α] [T0Space α] {f : β × γα} (h : Summable f) :
∑' (p : β × γ), f p = ∑' (b : β) (c : γ), f (b, c)
theorem tsum_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommGroup α] [UniformSpace α] [UniformAddGroup α] [CompleteSpace α] [T0Space α] {f : βγα} (h : Summable (Function.uncurry f)) :
∑' (c : γ) (b : β), f b c = ∑' (b : β) (c : γ), f b c
theorem Pi.hasSum {α : Type u_1} {ι : Type u_5} {π : αType u_6} [(x : α) → AddCommMonoid (π x)] [(x : α) → TopologicalSpace (π x)] {f : ι(x : α) → π x} {g : (x : α) → π x} :
HasSum f g ∀ (x : α), HasSum (fun (i : ι) => f i x) (g x)
theorem Pi.summable {α : Type u_1} {ι : Type u_5} {π : αType u_6} [(x : α) → AddCommMonoid (π x)] [(x : α) → TopologicalSpace (π x)] {f : ι(x : α) → π x} :
Summable f ∀ (x : α), Summable fun (i : ι) => f i x
theorem tsum_apply {α : Type u_1} {ι : Type u_5} {π : αType u_6} [(x : α) → AddCommMonoid (π x)] [(x : α) → TopologicalSpace (π x)] [∀ (x : α), T2Space (π x)] {f : ι(x : α) → π x} {x : α} (hf : Summable f) :
tsum (fun (i : ι) => f i) x = ∑' (i : ι), f i x

Multiplicative opposite #

theorem HasSum.op {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βα} {a : α} (hf : HasSum f a) :
HasSum (fun (a : β) => MulOpposite.op (f a)) (MulOpposite.op a)
theorem Summable.op {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βα} (hf : Summable f) :
Summable (MulOpposite.op f)
theorem HasSum.unop {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βαᵐᵒᵖ} {a : αᵐᵒᵖ} (hf : HasSum f a) :
HasSum (fun (a : β) => MulOpposite.unop (f a)) (MulOpposite.unop a)
theorem Summable.unop {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βαᵐᵒᵖ} (hf : Summable f) :
Summable (MulOpposite.unop f)
@[simp]
theorem hasSum_op {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βα} {a : α} :
HasSum (fun (a : β) => MulOpposite.op (f a)) (MulOpposite.op a) HasSum f a
@[simp]
theorem hasSum_unop {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βαᵐᵒᵖ} {a : αᵐᵒᵖ} :
HasSum (fun (a : β) => MulOpposite.unop (f a)) (MulOpposite.unop a) HasSum f a
@[simp]
theorem summable_op {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βα} :
(Summable fun (a : β) => MulOpposite.op (f a)) Summable f
@[simp]
theorem summable_unop {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βαᵐᵒᵖ} :
(Summable fun (a : β) => MulOpposite.unop (f a)) Summable f
theorem tsum_op {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : βα} [T2Space α] :
∑' (x : β), MulOpposite.op (f x) = MulOpposite.op (∑' (x : β), f x)
theorem tsum_unop {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [T2Space α] {f : βαᵐᵒᵖ} :
∑' (x : β), MulOpposite.unop (f x) = MulOpposite.unop (∑' (x : β), f x)

Interaction with the star #

theorem HasSum.star {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [StarAddMonoid α] [ContinuousStar α] {f : βα} {a : α} (h : HasSum f a) :
HasSum (fun (b : β) => star (f b)) (star a)
theorem Summable.star {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [StarAddMonoid α] [ContinuousStar α] {f : βα} (hf : Summable f) :
Summable fun (b : β) => star (f b)
theorem Summable.ofStar {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [StarAddMonoid α] [ContinuousStar α] {f : βα} (hf : Summable fun (b : β) => star (f b)) :
@[simp]
theorem summable_star_iff {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [StarAddMonoid α] [ContinuousStar α] {f : βα} :
(Summable fun (b : β) => star (f b)) Summable f
@[simp]
theorem summable_star_iff' {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [StarAddMonoid α] [ContinuousStar α] {f : βα} :
theorem tsum_star {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [StarAddMonoid α] [ContinuousStar α] {f : βα} [T2Space α] :
star (∑' (b : β), f b) = ∑' (b : β), star (f b)