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 : α) : HasSum (Pi.single b a) a

@[simp]

theorem tprod_pi_single {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] [DecidableEq β] (b : β) (a : α) : ∏' (b' : β), Pi.mulSingle b a 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 tprod_setProd_singleton_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] (b : β) (t : Set γ) (f : β × γ → α) : ∏' (x : ↑({b} ×ˢ t)), f ↑x = ∏' (c : ↑t), f (b, ↑c)

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 tprod_setProd_singleton_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] (s : Set β) (c : γ) (f : β × γ → α) : ∏' (x : ↑(s ×ˢ {c})), f ↑x = ∏' (b : ↑s), 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 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) : Summable fun (p : γ × β) => f p.swap

theorem HasProd.prod_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] [CommMonoid γ] [TopologicalSpace γ] {f : β → α} {g : β → γ} {a : α} {b : γ} (hf : HasProd f a) (hg : HasProd g b) : HasProd (fun (x : β) => (f x, g x)) (a, b)

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 HasProd.sigma {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] [ContinuousMul α] [RegularSpace α] {γ : β → Type u_5} {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_5} {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_5} {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_5} {f : (b : β) × γ b → α} (ha : Summable f) (hf : ∀ (b : β), Summable fun (c : γ b) => f ⟨b, c⟩) : Summable fun (b : β) => ∑' (c : γ b), f ⟨b, c⟩

theorem HasProd.sigma_of_hasProd {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] [ContinuousMul α] [T3Space α] {γ : β → Type u_5} {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_5} {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 tprod_sigma' {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] [ContinuousMul α] [T3Space α] {γ : β → Type u_5} {f : (b : β) × γ b → α} (h₁ : ∀ (b : β), Multipliable fun (c : γ b) => f ⟨b, c⟩) (h₂ : Multipliable f) : ∏' (p : (b : β) × γ b), f p = ∏' (b : β) (c : γ b), f ⟨b, c⟩

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 ⟨b, c⟩) (h₂ : Summable f) : ∑' (p : (b : β) × γ b), f p = ∑' (b : β) (c : γ b), f ⟨b, c⟩

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)) : ∏' (p : β × γ), f p = ∏' (b : β) (c : γ), f (b, 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 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) : ∏' (c : γ) (b : β), f b c = ∏' (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 HasProd.of_sigma {α : Type u_1} {β : Type u_2} [CommGroup α] [UniformSpace α] [UniformGroup α] {γ : β → Type u_5} {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 α] [UniformAddGroup α] {γ : β → Type u_5} {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 α] [UniformGroup α] [CompleteSpace α] {γ : β → Type u_5} {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 α] [UniformAddGroup α] [CompleteSpace α] {γ : β → Type u_5} {f : (b : β) × γ b → α} (ha : Summable f) (b : β) : Summable fun (c : γ b) => f ⟨b, c⟩

theorem Multipliable.sigma {α : Type u_1} {β : Type u_2} [CommGroup α] [UniformSpace α] [UniformGroup α] [CompleteSpace α] {γ : β → Type u_5} {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 α] [UniformAddGroup α] [CompleteSpace α] {γ : β → Type u_5} {f : (b : β) × γ b → α} (ha : Summable f) : Summable fun (b : β) => ∑' (c : γ b), f ⟨b, c⟩

theorem Multipliable.prod_factor {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommGroup α] [UniformSpace α] [UniformGroup α] [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 α] [UniformAddGroup α] [CompleteSpace α] {f : β × γ → α} (h : Summable f) (b : β) : Summable fun (c : γ) => f (b, c)

theorem HasProd.tprod_fiberwise {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommGroup α] [UniformSpace α] [UniformGroup α] [CompleteSpace α] [T2Space α] {f : β → α} {a : α} (hf : HasProd f a) (g : β → γ) : HasProd (fun (c : γ) => ∏' (b : ↑(g ⁻¹' {c})), f ↑b) a

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 tprod_sigma {α : Type u_1} {β : Type u_2} [CommGroup α] [UniformSpace α] [UniformGroup α] [CompleteSpace α] [T0Space α] {γ : β → Type u_5} {f : (b : β) × γ b → α} (ha : Multipliable f) : ∏' (p : (b : β) × γ b), f p = ∏' (b : β) (c : γ b), f ⟨b, c⟩

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 ⟨b, c⟩

theorem tprod_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommGroup α] [UniformSpace α] [UniformGroup α] [CompleteSpace α] [T0Space α] {f : β × γ → α} (h : Multipliable f) : ∏' (p : β × γ), f p = ∏' (b : β) (c : γ), f (b, 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 tprod_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommGroup α] [UniformSpace α] [UniformGroup α] [CompleteSpace α] [T0Space α] {f : β → γ → α} (h : Multipliable (Function.uncurry f)) : ∏' (c : γ) (b : β), f b c = ∏' (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.hasProd {α : Type u_1} {ι : Type u_5} {π : α → Type u_6} [(x : α) → CommMonoid (π x)] [(x : α) → TopologicalSpace (π x)] {f : ι → (x : α) → π x} {g : (x : α) → π x} : HasProd f g ↔ ∀ (x : α), HasProd (fun (i : ι) => f i x) (g x)

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.multipliable {α : Type u_1} {ι : Type u_5} {π : α → Type u_6} [(x : α) → CommMonoid (π x)] [(x : α) → TopologicalSpace (π x)] {f : ι → (x : α) → π x} : Multipliable f ↔ ∀ (x : α), Multipliable fun (i : ι) => f i 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 tprod_apply {α : Type u_1} {ι : Type u_5} {π : α → Type u_6} [(x : α) → CommMonoid (π x)] [(x : α) → TopologicalSpace (π x)] [∀ (x : α), T2Space (π x)] {f : ι → (x : α) → π x} {x : α} (hf : Multipliable f) : tprod (fun (i : ι) => f i) x = ∏' (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)) : Summable f

@[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 : β → α} : Summable (star f) ↔ Summable f

theorem tsum_star {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [StarAddMonoid α] [ContinuousStar α] {f : β → α} [T2Space α] : star (∑' (b : β), f b) = ∑' (b : β), star (f b)