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 : α)
:
theorem
tsum_setProd_singleton_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[AddCommMonoid α]
[TopologicalSpace α]
(b : β)
(t : Set γ)
(f : β × γ → α)
:
theorem
tsum_setProd_singleton_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[AddCommMonoid α]
[TopologicalSpace α]
(s : Set β)
(c : γ)
(f : β × γ → α)
:
theorem
Summable.prod_symm
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[AddCommMonoid α]
[TopologicalSpace α]
{f : β × γ → α}
(hf : Summable f)
:
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))
:
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 : β → γ)
:
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)
:
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}
:
theorem
Pi.summable
{α : Type u_1}
{ι : Type u_5}
{π : α → Type u_6}
[(x : α) → AddCommMonoid (π x)]
[(x : α) → TopologicalSpace (π x)]
{f : ι → (x : α) → π 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)
:
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)
:
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)
:
@[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)
:
theorem
Summable.star
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[TopologicalSpace α]
[StarAddMonoid α]
[ContinuousStar α]
{f : β → α}
(hf : Summable f)
:
theorem
Summable.ofStar
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[TopologicalSpace α]
[StarAddMonoid α]
[ContinuousStar α]
{f : β → α}
(hf : Summable fun (b : β) => star (f b))
:
Summable f
@[simp]
theorem
summable_star_iff
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[TopologicalSpace α]
[StarAddMonoid α]
[ContinuousStar α]
{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 α]
: