[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSemiring α
f g : ι → α
a a₁ a₂✝ a₂ : α
h : HasSum f a₁
⊢ HasSum (fun i => a₂ * f i) (a₂ * a₁)
[PROOFSTEP]
simpa only using h.map (AddMonoidHom.mulLeft a₂) (continuous_const.mul continuous_id)
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSemiring α
f g : ι → α
a a₁ a₂✝ a₂ : α
hf : HasSum f a₁
⊢ HasSum (fun i => f i * a₂) (a₁ * a₂)
[PROOFSTEP]
simpa only using hf.map (AddMonoidHom.mulRight a₂) (continuous_id.mul continuous_const)
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝² : DivisionSemiring α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSemiring α
f g : ι → α
a a₁ a₂ : α
h : HasSum f a
b : α
⊢ HasSum (fun i => f i / b) (a / b)
[PROOFSTEP]
simp only [div_eq_mul_inv, h.mul_right b⁻¹]
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝² : DivisionSemiring α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSemiring α
f g : ι → α
a a₁ a₂ : α
h : a₂ ≠ 0
H : HasSum (fun i => a₂ * f i) (a₂ * a₁)
⊢ HasSum f a₁
[PROOFSTEP]
simpa only [inv_mul_cancel_left₀ h] using H.mul_left a₂⁻¹
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝² : DivisionSemiring α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSemiring α
f g : ι → α
a a₁ a₂ : α
h : a₂ ≠ 0
H : HasSum (fun i => f i * a₂) (a₁ * a₂)
⊢ HasSum f a₁
[PROOFSTEP]
simpa only [mul_inv_cancel_right₀ h] using H.mul_right a₂⁻¹
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝² : DivisionSemiring α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSemiring α
f g : ι → α
a a₁ a₂ : α
h : a₂ ≠ 0
⊢ HasSum (fun i => f i / a₂) (a₁ / a₂) ↔ HasSum f a₁
[PROOFSTEP]
simpa only [div_eq_mul_inv] using hasSum_mul_right_iff (inv_ne_zero h)
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝² : DivisionSemiring α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSemiring α
f g : ι → α
a a₁ a₂ : α
h : a ≠ 0
H : Summable fun i => a * f i
⊢ Summable f
[PROOFSTEP]
simpa only [inv_mul_cancel_left₀ h] using H.mul_left a⁻¹
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝² : DivisionSemiring α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSemiring α
f g : ι → α
a a₁ a₂ : α
h : a ≠ 0
H : Summable fun i => f i * a
⊢ Summable f
[PROOFSTEP]
simpa only [mul_inv_cancel_right₀ h] using H.mul_right a⁻¹
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝² : DivisionSemiring α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSemiring α
f g : ι → α
a a₁ a₂ : α
h : a ≠ 0
⊢ (Summable fun i => f i / a) ↔ Summable f
[PROOFSTEP]
simpa only [div_eq_mul_inv] using summable_mul_right_iff (inv_ne_zero h)
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : DivisionSemiring α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSemiring α
f g : ι → α
a a₁ a₂ : α
inst✝ : T2Space α
hf : ¬Summable f
ha : a = 0
⊢ ∑' (x : ι), a * f x = a * ∑' (x : ι), f x
[PROOFSTEP]
simp [ha]
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : DivisionSemiring α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSemiring α
f g : ι → α
a a₁ a₂ : α
inst✝ : T2Space α
hf : ¬Summable f
ha : ¬a = 0
⊢ ∑' (x : ι), a * f x = a * ∑' (x : ι), f x
[PROOFSTEP]
rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable (mt (summable_mul_left_iff ha).mp hf), mul_zero]
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : DivisionSemiring α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSemiring α
f g : ι → α
a a₁ a₂ : α
inst✝ : T2Space α
hf : ¬Summable f
ha : a = 0
⊢ ∑' (x : ι), f x * a = (∑' (x : ι), f x) * a
[PROOFSTEP]
simp [ha]
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : DivisionSemiring α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSemiring α
f g : ι → α
a a₁ a₂ : α
inst✝ : T2Space α
hf : ¬Summable f
ha : ¬a = 0
⊢ ∑' (x : ι), f x * a = (∑' (x : ι), f x) * a
[PROOFSTEP]
rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable (mt (summable_mul_right_iff ha).mp hf), zero_mul]
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : DivisionSemiring α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSemiring α
f g : ι → α
a a₁ a₂ : α
inst✝ : T2Space α
⊢ ∑' (x : ι), f x / a = (∑' (x : ι), f x) / a
[PROOFSTEP]
simpa only [div_eq_mul_inv] using tsum_mul_right
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
h : Summable fun x => f x.fst * g x.snd
⊢ Summable fun n => ∑ kl in Nat.antidiagonal n, f kl.fst * g kl.snd
[PROOFSTEP]
rw [summable_mul_prod_iff_summable_mul_sigma_antidiagonal] at h 
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
h : Summable fun x => f (↑x.snd).fst * g (↑x.snd).snd
⊢ Summable fun n => ∑ kl in Nat.antidiagonal n, f kl.fst * g kl.snd
[PROOFSTEP]
conv => congr; ext; rw [← Finset.sum_finset_coe, ← tsum_fintype]
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
h : Summable fun x => f (↑x.snd).fst * g (↑x.snd).snd
| Summable fun n => ∑ kl in Nat.antidiagonal n, f kl.fst * g kl.snd
[PROOFSTEP]
congr; ext; rw [← Finset.sum_finset_coe, ← tsum_fintype]
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
h : Summable fun x => f (↑x.snd).fst * g (↑x.snd).snd
| Summable fun n => ∑ kl in Nat.antidiagonal n, f kl.fst * g kl.snd
[PROOFSTEP]
congr; ext; rw [← Finset.sum_finset_coe, ← tsum_fintype]
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
h : Summable fun x => f (↑x.snd).fst * g (↑x.snd).snd
| Summable fun n => ∑ kl in Nat.antidiagonal n, f kl.fst * g kl.snd
[PROOFSTEP]
congr
[GOAL]
case f
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
h : Summable fun x => f (↑x.snd).fst * g (↑x.snd).snd
| fun n => ∑ kl in Nat.antidiagonal n, f kl.fst * g kl.snd
[PROOFSTEP]
ext
[GOAL]
case f.h
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
h : Summable fun x => f (↑x.snd).fst * g (↑x.snd).snd
x✝ : ℕ
| ∑ kl in Nat.antidiagonal x✝, f kl.fst * g kl.snd
[PROOFSTEP]
rw [← Finset.sum_finset_coe, ← tsum_fintype]
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
h : Summable fun x => f (↑x.snd).fst * g (↑x.snd).snd
⊢ Summable fun x => ∑' (b : ↑↑(Nat.antidiagonal x)), f (↑b).fst * g (↑b).snd
[PROOFSTEP]
exact h.sigma' fun n => (hasSum_fintype _).summable
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x => f x.fst * g x.snd
⊢ (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ kl in Nat.antidiagonal n, f kl.fst * g kl.snd
[PROOFSTEP]
conv_rhs => congr; ext; rw [← Finset.sum_finset_coe, ← tsum_fintype]
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x => f x.fst * g x.snd
| ∑' (n : ℕ), ∑ kl in Nat.antidiagonal n, f kl.fst * g kl.snd
[PROOFSTEP]
congr; ext; rw [← Finset.sum_finset_coe, ← tsum_fintype]
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x => f x.fst * g x.snd
| ∑' (n : ℕ), ∑ kl in Nat.antidiagonal n, f kl.fst * g kl.snd
[PROOFSTEP]
congr; ext; rw [← Finset.sum_finset_coe, ← tsum_fintype]
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x => f x.fst * g x.snd
| ∑' (n : ℕ), ∑ kl in Nat.antidiagonal n, f kl.fst * g kl.snd
[PROOFSTEP]
congr
[GOAL]
case f
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x => f x.fst * g x.snd
| fun n => ∑ kl in Nat.antidiagonal n, f kl.fst * g kl.snd
[PROOFSTEP]
ext
[GOAL]
case f.h
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x => f x.fst * g x.snd
x✝ : ℕ
| ∑ kl in Nat.antidiagonal x✝, f kl.fst * g kl.snd
[PROOFSTEP]
rw [← Finset.sum_finset_coe, ← tsum_fintype]
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x => f x.fst * g x.snd
⊢ (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (x : ℕ) (b : ↑↑(Nat.antidiagonal x)), f (↑b).fst * g (↑b).snd
[PROOFSTEP]
rw [tsum_mul_tsum hf hg hfg, ← Nat.sigmaAntidiagonalEquivProd.tsum_eq (_ : ℕ × ℕ → α)]
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x => f x.fst * g x.snd
⊢ ∑' (c : (n : ℕ) × { x // x ∈ Nat.antidiagonal n }),
      f (↑Nat.sigmaAntidiagonalEquivProd c).fst * g (↑Nat.sigmaAntidiagonalEquivProd c).snd =
    ∑' (x : ℕ) (b : ↑↑(Nat.antidiagonal x)), f (↑b).fst * g (↑b).snd
[PROOFSTEP]
exact tsum_sigma' (fun n => (hasSum_fintype _).summable) (summable_mul_prod_iff_summable_mul_sigma_antidiagonal.mp hfg)
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
h : Summable fun x => f x.fst * g x.snd
⊢ Summable fun n => ∑ k in range (n + 1), f k * g (n - k)
[PROOFSTEP]
simp_rw [← Nat.sum_antidiagonal_eq_sum_range_succ fun k l => f k * g l]
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
h : Summable fun x => f x.fst * g x.snd
⊢ Summable fun n => ∑ ij in Nat.antidiagonal n, f ij.fst * g ij.snd
[PROOFSTEP]
exact summable_sum_mul_antidiagonal_of_summable_mul h
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x => f x.fst * g x.snd
⊢ (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ k in range (n + 1), f k * g (n - k)
[PROOFSTEP]
simp_rw [← Nat.sum_antidiagonal_eq_sum_range_succ fun k l => f k * g l]
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x => f x.fst * g x.snd
⊢ (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ ij in Nat.antidiagonal n, f ij.fst * g ij.snd
[PROOFSTEP]
exact tsum_mul_tsum_eq_tsum_sum_antidiagonal hf hg hfg
