Topological sums and functorial constructions #
Lemmas on the interaction of tprod, tsum, HasProd, HasSum etc. with products, Sigma and Pi
types, MulOpposite, etc.
Product, Sigma and Pi types #
theorem
hasProd_pi_single
{α : Type u_1}
{β : Type u_2}
[CommMonoid α]
[TopologicalSpace α]
[DecidableEq β]
(b : β)
(a : α)
:
HasProd (Pi.mulSingle b a) a
theorem
hasSum_pi_single
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[TopologicalSpace α]
[DecidableEq β]
(b : β)
(a : α)
:
@[simp]
theorem
tprod_pi_single
{α : Type u_1}
{β : Type u_2}
[CommMonoid α]
[TopologicalSpace α]
[DecidableEq β]
(b : β)
(a : α)
:
@[simp]
theorem
tsum_pi_single
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[TopologicalSpace α]
[DecidableEq β]
(b : β)
(a : α)
:
theorem
Multipliable.prod_symm
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[CommMonoid α]
[TopologicalSpace α]
{f : β × γ → α}
(hf : Multipliable f)
:
Multipliable fun (p : γ × β) => f p.swap
theorem
Summable.prod_symm
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[AddCommMonoid α]
[TopologicalSpace α]
{f : β × γ → α}
(hf : Summable f)
:
theorem
HasProd.prodMk
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{L : SummationFilter β}
[CommMonoid α]
[TopologicalSpace α]
[CommMonoid γ]
[TopologicalSpace γ]
{f : β → α}
{g : β → γ}
{a : α}
{b : γ}
(hf : HasProd f a L)
(hg : HasProd g b L)
:
theorem
HasSum.prodMk
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{L : SummationFilter β}
[AddCommMonoid α]
[TopologicalSpace α]
[AddCommMonoid γ]
[TopologicalSpace γ]
{f : β → α}
{g : β → γ}
{a : α}
{b : γ}
(hf : HasSum f a L)
(hg : HasSum g b L)
:
@[deprecated HasSum.prodMk (since := "2025-03-10")]
theorem
HasSum.prod_mk
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{L : SummationFilter β}
[AddCommMonoid α]
[TopologicalSpace α]
[AddCommMonoid γ]
[TopologicalSpace γ]
{f : β → α}
{g : β → γ}
{a : α}
{b : γ}
(hf : HasSum f a L)
(hg : HasSum g b L)
:
Alias of HasSum.prodMk.
@[deprecated HasProd.prodMk (since := "2025-03-10")]
theorem
HasProd.prod_mk
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{L : SummationFilter β}
[CommMonoid α]
[TopologicalSpace α]
[CommMonoid γ]
[TopologicalSpace γ]
{f : β → α}
{g : β → γ}
{a : α}
{b : γ}
(hf : HasProd f a L)
(hg : HasProd g b L)
:
Alias of HasProd.prodMk.
theorem
HasProd.sum
{α : Type u_4}
{β : Type u_5}
{M : Type u_6}
[CommMonoid M]
[TopologicalSpace M]
[ContinuousMul M]
{f : α ⊕ β → M}
{a b : M}
(h₁ : HasProd (f ∘ Sum.inl) a)
(h₂ : HasProd (f ∘ Sum.inr) b)
:
theorem
HasSum.sum
{α : Type u_4}
{β : Type u_5}
{M : Type u_6}
[AddCommMonoid M]
[TopologicalSpace M]
[ContinuousAdd M]
{f : α ⊕ β → M}
{a b : M}
(h₁ : HasSum (f ∘ Sum.inl) a)
(h₂ : HasSum (f ∘ Sum.inr) b)
:
theorem
Multipliable.tprod_sum
{α : Type u_4}
{β : Type u_5}
{M : Type u_6}
[CommMonoid M]
[TopologicalSpace M]
[ContinuousMul M]
[T2Space M]
{f : α ⊕ β → M}
(h₁ : Multipliable (f ∘ Sum.inl))
(h₂ : Multipliable (f ∘ Sum.inr))
:
theorem
Summable.tsum_sum
{α : Type u_4}
{β : Type u_5}
{M : Type u_6}
[AddCommMonoid M]
[TopologicalSpace M]
[ContinuousAdd M]
[T2Space M]
{f : α ⊕ β → M}
(h₁ : Summable (f ∘ Sum.inl))
(h₂ : Summable (f ∘ Sum.inr))
:
For the statement that tsum commutes with Finset.sum,
see Summable.tsum_finsetSum.
@[deprecated Summable.tsum_sum (since := "2025-04-12")]
theorem
tsum_sum
{α : Type u_4}
{β : Type u_5}
{M : Type u_6}
[AddCommMonoid M]
[TopologicalSpace M]
[ContinuousAdd M]
[T2Space M]
{f : α ⊕ β → M}
(h₁ : Summable (f ∘ Sum.inl))
(h₂ : Summable (f ∘ Sum.inr))
:
Alias of Summable.tsum_sum.
For the statement that tsum commutes with Finset.sum,
see Summable.tsum_finsetSum.
@[deprecated Multipliable.tprod_sum (since := "2025-04-12")]
theorem
tprod_sum
{α : Type u_4}
{β : Type u_5}
{M : Type u_6}
[CommMonoid M]
[TopologicalSpace M]
[ContinuousMul M]
[T2Space M]
{f : α ⊕ β → M}
(h₁ : Multipliable (f ∘ Sum.inl))
(h₂ : Multipliable (f ∘ Sum.inr))
:
Alias of Multipliable.tprod_sum.
theorem
Multipliable.sum
{α : Type u_4}
{β : Type u_5}
{M : Type u_6}
[CommMonoid M]
[TopologicalSpace M]
[ContinuousMul M]
(f : α ⊕ β → M)
(h₁ : Multipliable (f ∘ Sum.inl))
(h₂ : Multipliable (f ∘ Sum.inr))
:
theorem
Summable.sum
{α : Type u_4}
{β : Type u_5}
{M : Type u_6}
[AddCommMonoid M]
[TopologicalSpace M]
[ContinuousAdd M]
(f : α ⊕ β → M)
(h₁ : Summable (f ∘ Sum.inl))
(h₂ : Summable (f ∘ Sum.inr))
:
Summable f
theorem
HasProd.sigma
{α : Type u_1}
{β : Type u_2}
[CommMonoid α]
[TopologicalSpace α]
[ContinuousMul α]
[RegularSpace α]
{γ : β → Type u_4}
{f : (b : β) × γ b → α}
{g : β → α}
{a : α}
(ha : HasProd f a)
(hf : ∀ (b : β), HasProd (fun (c : γ b) => f ⟨b, c⟩) (g b))
:
HasProd g a
theorem
HasSum.sigma
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[TopologicalSpace α]
[ContinuousAdd α]
[RegularSpace α]
{γ : β → Type u_4}
{f : (b : β) × γ b → α}
{g : β → α}
{a : α}
(ha : HasSum f a)
(hf : ∀ (b : β), HasSum (fun (c : γ b) => f ⟨b, c⟩) (g b))
:
HasSum g a
theorem
HasProd.prod_fiberwise
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[CommMonoid α]
[TopologicalSpace α]
[ContinuousMul α]
[RegularSpace α]
{f : β × γ → α}
{g : β → α}
{a : α}
(ha : HasProd f a)
(hf : ∀ (b : β), HasProd (fun (c : γ) => f (b, c)) (g b))
:
HasProd g a
If a function f on β × γ has product a and for each b the restriction of f to
{b} × γ has product g b, then the function g has product 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
Multipliable.sigma'
{α : Type u_1}
{β : Type u_2}
[CommMonoid α]
[TopologicalSpace α]
[ContinuousMul α]
[RegularSpace α]
{γ : β → Type u_4}
{f : (b : β) × γ b → α}
(ha : Multipliable f)
(hf : ∀ (b : β), Multipliable fun (c : γ b) => f ⟨b, c⟩)
:
Multipliable fun (b : β) => ∏' (c : γ b), f ⟨b, c⟩
theorem
Summable.sigma'
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[TopologicalSpace α]
[ContinuousAdd α]
[RegularSpace α]
{γ : β → Type u_4}
{f : (b : β) × γ b → α}
(ha : Summable f)
(hf : ∀ (b : β), Summable fun (c : γ b) => f ⟨b, c⟩)
:
theorem
HasProd.sigma_of_hasProd
{α : Type u_1}
{β : Type u_2}
[CommMonoid α]
[TopologicalSpace α]
[ContinuousMul α]
[T3Space α]
{γ : β → Type u_4}
{f : (b : β) × γ b → α}
{g : β → α}
{a : α}
(ha : HasProd g a)
(hf : ∀ (b : β), HasProd (fun (c : γ b) => f ⟨b, c⟩) (g b))
(hf' : Multipliable f)
:
HasProd f a
theorem
HasSum.sigma_of_hasSum
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[TopologicalSpace α]
[ContinuousAdd α]
[T3Space α]
{γ : β → Type u_4}
{f : (b : β) × γ b → α}
{g : β → α}
{a : α}
(ha : HasSum g a)
(hf : ∀ (b : β), HasSum (fun (c : γ b) => f ⟨b, c⟩) (g b))
(hf' : Summable f)
:
HasSum f a
theorem
Multipliable.tprod_sigma'
{α : Type u_1}
{β : Type u_2}
[CommMonoid α]
[TopologicalSpace α]
[ContinuousMul α]
[T3Space α]
{γ : β → Type u_4}
{f : (b : β) × γ b → α}
(h₁ : ∀ (b : β), Multipliable fun (c : γ b) => f ⟨b, c⟩)
(h₂ : Multipliable f)
:
theorem
Summable.tsum_sigma'
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[TopologicalSpace α]
[ContinuousAdd α]
[T3Space α]
{γ : β → Type u_4}
{f : (b : β) × γ b → α}
(h₁ : ∀ (b : β), Summable fun (c : γ b) => f ⟨b, c⟩)
(h₂ : Summable f)
:
@[deprecated Summable.tsum_sigma' (since := "2025-04-12")]
theorem
tsum_sigma'
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid α]
[TopologicalSpace α]
[ContinuousAdd α]
[T3Space α]
{γ : β → Type u_4}
{f : (b : β) × γ b → α}
(h₁ : ∀ (b : β), Summable fun (c : γ b) => f ⟨b, c⟩)
(h₂ : Summable f)
:
Alias of Summable.tsum_sigma'.
@[deprecated Multipliable.tprod_sigma' (since := "2025-04-12")]
theorem
tprod_sigma'
{α : Type u_1}
{β : Type u_2}
[CommMonoid α]
[TopologicalSpace α]
[ContinuousMul α]
[T3Space α]
{γ : β → Type u_4}
{f : (b : β) × γ b → α}
(h₁ : ∀ (b : β), Multipliable fun (c : γ b) => f ⟨b, c⟩)
(h₂ : Multipliable f)
:
Alias of Multipliable.tprod_sigma'.
theorem
Multipliable.tprod_prod'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[CommMonoid α]
[TopologicalSpace α]
[ContinuousMul α]
[T3Space α]
{f : β × γ → α}
(h : Multipliable f)
(h₁ : ∀ (b : β), Multipliable fun (c : γ) => f (b, c))
:
@[deprecated Summable.tsum_prod' (since := "2025-04-12")]
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))
:
Alias of Summable.tsum_prod'.
@[deprecated Multipliable.tprod_prod' (since := "2025-04-12")]
theorem
tprod_prod'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[CommMonoid α]
[TopologicalSpace α]
[ContinuousMul α]
[T3Space α]
{f : β × γ → α}
(h : Multipliable f)
(h₁ : ∀ (b : β), Multipliable fun (c : γ) => f (b, c))
:
Alias of Multipliable.tprod_prod'.
theorem
Multipliable.tprod_prod_uncurry
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[CommMonoid α]
[TopologicalSpace α]
[ContinuousMul α]
[T3Space α]
{f : β → γ → α}
(h : Multipliable (Function.uncurry f))
(h₁ : ∀ (b : β), Multipliable fun (c : γ) => f b c)
:
theorem
Summable.tsum_prod_uncurry
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[AddCommMonoid α]
[TopologicalSpace α]
[ContinuousAdd α]
[T3Space α]
{f : β → γ → α}
(h : Summable (Function.uncurry f))
(h₁ : ∀ (b : β), Summable fun (c : γ) => f b c)
:
@[deprecated Summable.tsum_prod_uncurry (since := "2025-04-12")]
theorem
tsum_prod_uncurry
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[AddCommMonoid α]
[TopologicalSpace α]
[ContinuousAdd α]
[T3Space α]
{f : β → γ → α}
(h : Summable (Function.uncurry f))
(h₁ : ∀ (b : β), Summable fun (c : γ) => f b c)
:
Alias of Summable.tsum_prod_uncurry.
@[deprecated Multipliable.tprod_prod_uncurry (since := "2025-04-12")]
theorem
tprod_prod_uncurry
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[CommMonoid α]
[TopologicalSpace α]
[ContinuousMul α]
[T3Space α]
{f : β → γ → α}
(h : Multipliable (Function.uncurry f))
(h₁ : ∀ (b : β), Multipliable fun (c : γ) => f b c)
:
Alias of Multipliable.tprod_prod_uncurry.
theorem
Multipliable.tprod_comm'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[CommMonoid α]
[TopologicalSpace α]
[ContinuousMul α]
[T3Space α]
{f : β → γ → α}
(h : Multipliable (Function.uncurry f))
(h₁ : ∀ (b : β), Multipliable (f b))
(h₂ : ∀ (c : γ), Multipliable fun (b : β) => f b c)
:
theorem
Summable.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)
:
@[deprecated Summable.tsum_comm' (since := "2025-04-12")]
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)
:
Alias of Summable.tsum_comm'.
@[deprecated Multipliable.tprod_comm' (since := "2025-04-12")]
theorem
tprod_comm'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[CommMonoid α]
[TopologicalSpace α]
[ContinuousMul α]
[T3Space α]
{f : β → γ → α}
(h : Multipliable (Function.uncurry f))
(h₁ : ∀ (b : β), Multipliable (f b))
(h₂ : ∀ (c : γ), Multipliable fun (b : β) => f b c)
:
Alias of Multipliable.tprod_comm'.
theorem
HasProd.of_sigma
{α : Type u_1}
{β : Type u_2}
[CommGroup α]
[UniformSpace α]
[IsUniformGroup α]
{γ : β → Type u_4}
{f : (b : β) × γ b → α}
{g : β → α}
{a : α}
(hf : ∀ (b : β), HasProd (fun (c : γ b) => f ⟨b, c⟩) (g b))
(hg : HasProd g a)
(h : CauchySeq fun (s : Finset ((b : β) × γ b)) => ∏ i ∈ s, f i)
:
HasProd f a
theorem
HasSum.of_sigma
{α : Type u_1}
{β : Type u_2}
[AddCommGroup α]
[UniformSpace α]
[IsUniformAddGroup α]
{γ : β → Type u_4}
{f : (b : β) × γ b → α}
{g : β → α}
{a : α}
(hf : ∀ (b : β), HasSum (fun (c : γ b) => f ⟨b, c⟩) (g b))
(hg : HasSum g a)
(h : CauchySeq fun (s : Finset ((b : β) × γ b)) => ∑ i ∈ s, f i)
:
HasSum f a
theorem
Multipliable.sigma_factor
{α : Type u_1}
{β : Type u_2}
[CommGroup α]
[UniformSpace α]
[IsUniformGroup α]
[CompleteSpace α]
{γ : β → Type u_4}
{f : (b : β) × γ b → α}
(ha : Multipliable f)
(b : β)
:
Multipliable fun (c : γ b) => f ⟨b, c⟩
theorem
Summable.sigma_factor
{α : Type u_1}
{β : Type u_2}
[AddCommGroup α]
[UniformSpace α]
[IsUniformAddGroup α]
[CompleteSpace α]
{γ : β → Type u_4}
{f : (b : β) × γ b → α}
(ha : Summable f)
(b : β)
:
theorem
Multipliable.sigma
{α : Type u_1}
{β : Type u_2}
[CommGroup α]
[UniformSpace α]
[IsUniformGroup α]
[CompleteSpace α]
{γ : β → Type u_4}
{f : (b : β) × γ b → α}
(ha : Multipliable f)
:
Multipliable fun (b : β) => ∏' (c : γ b), f ⟨b, c⟩
theorem
Summable.sigma
{α : Type u_1}
{β : Type u_2}
[AddCommGroup α]
[UniformSpace α]
[IsUniformAddGroup α]
[CompleteSpace α]
{γ : β → Type u_4}
{f : (b : β) × γ b → α}
(ha : Summable f)
:
theorem
Multipliable.prod_factor
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[CommGroup α]
[UniformSpace α]
[IsUniformGroup α]
[CompleteSpace α]
{f : β × γ → α}
(h : Multipliable f)
(b : β)
:
Multipliable fun (c : γ) => f (b, c)
theorem
Summable.prod_factor
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[AddCommGroup α]
[UniformSpace α]
[IsUniformAddGroup α]
[CompleteSpace α]
{f : β × γ → α}
(h : Summable f)
(b : β)
:
theorem
Multipliable.prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[CommGroup α]
[UniformSpace α]
[IsUniformGroup α]
[CompleteSpace α]
{f : β × γ → α}
(h : Multipliable f)
:
theorem
Summable.prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[AddCommGroup α]
[UniformSpace α]
[IsUniformAddGroup α]
[CompleteSpace α]
{f : β × γ → α}
(h : Summable f)
:
theorem
HasProd.tprod_fiberwise
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[CommGroup α]
[UniformSpace α]
[IsUniformGroup α]
[CompleteSpace α]
[T2Space α]
{f : β → α}
{a : α}
(hf : HasProd f a)
(g : β → γ)
:
theorem
HasSum.tsum_fiberwise
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[AddCommGroup α]
[UniformSpace α]
[IsUniformAddGroup α]
[CompleteSpace α]
[T2Space α]
{f : β → α}
{a : α}
(hf : HasSum f a)
(g : β → γ)
:
theorem
Multipliable.tprod_sigma
{α : Type u_1}
{β : Type u_2}
[CommGroup α]
[UniformSpace α]
[IsUniformGroup α]
[CompleteSpace α]
[T0Space α]
{γ : β → Type u_4}
{f : (b : β) × γ b → α}
(ha : Multipliable f)
:
theorem
Summable.tsum_sigma
{α : Type u_1}
{β : Type u_2}
[AddCommGroup α]
[UniformSpace α]
[IsUniformAddGroup α]
[CompleteSpace α]
[T0Space α]
{γ : β → Type u_4}
{f : (b : β) × γ b → α}
(ha : Summable f)
:
@[deprecated Summable.tsum_sigma (since := "2025-04-12")]
theorem
tsum_sigma
{α : Type u_1}
{β : Type u_2}
[AddCommGroup α]
[UniformSpace α]
[IsUniformAddGroup α]
[CompleteSpace α]
[T0Space α]
{γ : β → Type u_4}
{f : (b : β) × γ b → α}
(ha : Summable f)
:
Alias of Summable.tsum_sigma.
@[deprecated Multipliable.tprod_sigma (since := "2025-04-12")]
theorem
tprod_sigma
{α : Type u_1}
{β : Type u_2}
[CommGroup α]
[UniformSpace α]
[IsUniformGroup α]
[CompleteSpace α]
[T0Space α]
{γ : β → Type u_4}
{f : (b : β) × γ b → α}
(ha : Multipliable f)
:
Alias of Multipliable.tprod_sigma.
theorem
Multipliable.tprod_prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[CommGroup α]
[UniformSpace α]
[IsUniformGroup α]
[CompleteSpace α]
[T0Space α]
{f : β × γ → α}
(h : Multipliable f)
:
theorem
Summable.tsum_prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[AddCommGroup α]
[UniformSpace α]
[IsUniformAddGroup α]
[CompleteSpace α]
[T0Space α]
{f : β × γ → α}
(h : Summable f)
:
@[deprecated Summable.tsum_prod (since := "2025-04-12")]
theorem
tsum_prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[AddCommGroup α]
[UniformSpace α]
[IsUniformAddGroup α]
[CompleteSpace α]
[T0Space α]
{f : β × γ → α}
(h : Summable f)
:
Alias of Summable.tsum_prod.
@[deprecated Multipliable.tprod_prod (since := "2025-04-12")]
theorem
tprod_prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[CommGroup α]
[UniformSpace α]
[IsUniformGroup α]
[CompleteSpace α]
[T0Space α]
{f : β × γ → α}
(h : Multipliable f)
:
Alias of Multipliable.tprod_prod.
theorem
Multipliable.tprod_comm
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[CommGroup α]
[UniformSpace α]
[IsUniformGroup α]
[CompleteSpace α]
[T0Space α]
{f : β → γ → α}
(h : Multipliable (Function.uncurry f))
:
theorem
Summable.tsum_comm
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[AddCommGroup α]
[UniformSpace α]
[IsUniformAddGroup α]
[CompleteSpace α]
[T0Space α]
{f : β → γ → α}
(h : Summable (Function.uncurry f))
:
@[deprecated Summable.tsum_comm (since := "2025-04-12")]
theorem
tsum_comm
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[AddCommGroup α]
[UniformSpace α]
[IsUniformAddGroup α]
[CompleteSpace α]
[T0Space α]
{f : β → γ → α}
(h : Summable (Function.uncurry f))
:
Alias of Summable.tsum_comm.
@[deprecated Multipliable.tprod_comm (since := "2025-04-12")]
theorem
tprod_comm
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[CommGroup α]
[UniformSpace α]
[IsUniformGroup α]
[CompleteSpace α]
[T0Space α]
{f : β → γ → α}
(h : Multipliable (Function.uncurry f))
:
Alias of Multipliable.tprod_comm.
theorem
Pi.hasProd
{α : Type u_1}
{ι : Type u_4}
{X : α → Type u_5}
[(x : α) → CommMonoid (X x)]
[(x : α) → TopologicalSpace (X x)]
{L : SummationFilter ι}
{f : ι → (x : α) → X x}
{g : (x : α) → X x}
:
theorem
Pi.hasSum
{α : Type u_1}
{ι : Type u_4}
{X : α → Type u_5}
[(x : α) → AddCommMonoid (X x)]
[(x : α) → TopologicalSpace (X x)]
{L : SummationFilter ι}
{f : ι → (x : α) → X x}
{g : (x : α) → X x}
:
theorem
Pi.multipliable
{α : Type u_1}
{ι : Type u_4}
{X : α → Type u_5}
[(x : α) → CommMonoid (X x)]
[(x : α) → TopologicalSpace (X x)]
{L : SummationFilter ι}
{f : ι → (x : α) → X x}
:
theorem
Pi.summable
{α : Type u_1}
{ι : Type u_4}
{X : α → Type u_5}
[(x : α) → AddCommMonoid (X x)]
[(x : α) → TopologicalSpace (X x)]
{L : SummationFilter ι}
{f : ι → (x : α) → X x}
:
theorem
tprod_apply
{α : Type u_1}
{ι : Type u_4}
{X : α → Type u_5}
[(x : α) → CommMonoid (X x)]
[(x : α) → TopologicalSpace (X x)]
{L : SummationFilter ι}
[L.NeBot]
[∀ (x : α), T2Space (X x)]
{f : ι → (x : α) → X x}
{x : α}
(hf : Multipliable f L)
:
theorem
tsum_apply
{α : Type u_1}
{ι : Type u_4}
{X : α → Type u_5}
[(x : α) → AddCommMonoid (X x)]
[(x : α) → TopologicalSpace (X x)]
{L : SummationFilter ι}
[L.NeBot]
[∀ (x : α), T2Space (X x)]
{f : ι → (x : α) → X x}
{x : α}
(hf : Summable f L)
:
Multiplicative opposite #
theorem
HasSum.op
{α : Type u_1}
{β : Type u_2}
{L : SummationFilter β}
[AddCommMonoid α]
[TopologicalSpace α]
{f : β → α}
{a : α}
(hf : HasSum f a L)
:
HasSum (fun (a : β) => MulOpposite.op (f a)) (MulOpposite.op a) L
theorem
Summable.op
{α : Type u_1}
{β : Type u_2}
{L : SummationFilter β}
[AddCommMonoid α]
[TopologicalSpace α]
{f : β → α}
(hf : Summable f L)
:
Summable (MulOpposite.op ∘ f) L
theorem
HasSum.unop
{α : Type u_1}
{β : Type u_2}
{L : SummationFilter β}
[AddCommMonoid α]
[TopologicalSpace α]
{f : β → αᵐᵒᵖ}
{a : αᵐᵒᵖ}
(hf : HasSum f a L)
:
HasSum (fun (a : β) => MulOpposite.unop (f a)) (MulOpposite.unop a) L
theorem
Summable.unop
{α : Type u_1}
{β : Type u_2}
{L : SummationFilter β}
[AddCommMonoid α]
[TopologicalSpace α]
{f : β → αᵐᵒᵖ}
(hf : Summable f L)
:
Summable (MulOpposite.unop ∘ f) L
@[simp]
theorem
hasSum_op
{α : Type u_1}
{β : Type u_2}
{L : SummationFilter β}
[AddCommMonoid α]
[TopologicalSpace α]
{f : β → α}
{a : α}
:
@[simp]
theorem
hasSum_unop
{α : Type u_1}
{β : Type u_2}
{L : SummationFilter β}
[AddCommMonoid α]
[TopologicalSpace α]
{f : β → αᵐᵒᵖ}
{a : αᵐᵒᵖ}
:
@[simp]
theorem
summable_op
{α : Type u_1}
{β : Type u_2}
{L : SummationFilter β}
[AddCommMonoid α]
[TopologicalSpace α]
{f : β → α}
:
theorem
summable_unop
{α : Type u_1}
{β : Type u_2}
{L : SummationFilter β}
[AddCommMonoid α]
[TopologicalSpace α]
{f : β → αᵐᵒᵖ}
:
theorem
tsum_op
{α : Type u_1}
{β : Type u_2}
{L : SummationFilter β}
[AddCommMonoid α]
[TopologicalSpace α]
{f : β → α}
[T2Space α]
:
theorem
tsum_unop
{α : Type u_1}
{β : Type u_2}
{L : SummationFilter β}
[AddCommMonoid α]
[TopologicalSpace α]
[T2Space α]
{f : β → αᵐᵒᵖ}
:
Interaction with the star #
theorem
HasSum.star
{α : Type u_1}
{β : Type u_2}
{L : SummationFilter β}
[AddCommMonoid α]
[TopologicalSpace α]
[StarAddMonoid α]
[ContinuousStar α]
{f : β → α}
{a : α}
(h : HasSum f a L)
:
theorem
Summable.star
{α : Type u_1}
{β : Type u_2}
{L : SummationFilter β}
[AddCommMonoid α]
[TopologicalSpace α]
[StarAddMonoid α]
[ContinuousStar α]
{f : β → α}
(hf : Summable f L)
:
theorem
Summable.ofStar
{α : Type u_1}
{β : Type u_2}
{L : SummationFilter β}
[AddCommMonoid α]
[TopologicalSpace α]
[StarAddMonoid α]
[ContinuousStar α]
{f : β → α}
(hf : Summable (fun (b : β) => Star.star (f b)) L)
:
Summable f L
@[simp]
theorem
summable_star_iff
{α : Type u_1}
{β : Type u_2}
{L : SummationFilter β}
[AddCommMonoid α]
[TopologicalSpace α]
[StarAddMonoid α]
[ContinuousStar α]
{f : β → α}
:
@[simp]
theorem
summable_star_iff'
{α : Type u_1}
{β : Type u_2}
{L : SummationFilter β}
[AddCommMonoid α]
[TopologicalSpace α]
[StarAddMonoid α]
[ContinuousStar α]
{f : β → α}
:
theorem
tsum_star
{α : Type u_1}
{β : Type u_2}
{L : SummationFilter β}
[AddCommMonoid α]
[TopologicalSpace α]
[StarAddMonoid α]
[ContinuousStar α]
{f : β → α}
[T2Space α]
: