case pos
X : Type u_5
α : Type ?u.110701
l : Type u_1
m : Type ?u.110707
n : Type ?u.110710
p : Type ?u.110713
S : Type ?u.110716
R : Type u_2
m' : l → Type u_3
n' : l → Type u_4
inst✝⁵ : Semiring α
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : Module α R
inst✝¹ : DecidableEq l
inst✝ : T2Space R
f : X → (i : l) → Matrix (m' i) (n' i) R
hf : Summable f
⊢ blockDiagonal' (∑' (x : X), f x) = ∑' (x : X), blockDiagonal' (f x)

case neg
X : Type u_5
α : Type ?u.110701
l : Type u_1
m : Type ?u.110707
n : Type ?u.110710
p : Type ?u.110713
S : Type ?u.110716
R : Type u_2
m' : l → Type u_3
n' : l → Type u_4
inst✝⁵ : Semiring α
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : Module α R
inst✝¹ : DecidableEq l
inst✝ : T2Space R
f : X → (i : l) → Matrix (m' i) (n' i) R
hf : ¬Summable f
⊢ blockDiagonal' (∑' (x : X), f x) = ∑' (x : X), blockDiagonal' (f x)
X : Type u_5
α : Type ?u.110701
l : Type u_1
m : Type ?u.110707
n : Type ?u.110710
p : Type ?u.110713
S : Type ?u.110716
R : Type u_2
m' : l → Type u_3
n' : l → Type u_4
inst✝⁵ : Semiring α
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : Module α R
inst✝¹ : DecidableEq l
inst✝ : T2Space R
f : X → (i : l) → Matrix (m' i) (n' i) R
⊢ blockDiagonal' (∑' (x : X), f x) = ∑' (x : X), blockDiagonal' (f x)
by_cases hf : Summable f
no goals
case pos
X : Type u_5
α : Type ?u.110701
l : Type u_1
m : Type ?u.110707
n : Type ?u.110710
p : Type ?u.110713
S : Type ?u.110716
R : Type u_2
m' : l → Type u_3
n' : l → Type u_4
inst✝⁵ : Semiring α
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : Module α R
inst✝¹ : DecidableEq l
inst✝ : T2Space R
f : X → (i : l) → Matrix (m' i) (n' i) R
hf : Summable f
⊢ blockDiagonal' (∑' (x : X), f x) = ∑' (x : X), blockDiagonal' (f x)
exact hf.hasSum.matrix_blockDiagonal'.tsum_eq.symm
case neg
X : Type u_5
α : Type ?u.110701
l : Type u_1
m : Type ?u.110707
n : Type ?u.110710
p : Type ?u.110713
S : Type ?u.110716
R : Type u_2
m' : l → Type u_3
n' : l → Type u_4
inst✝⁵ : Semiring α
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : Module α R
inst✝¹ : DecidableEq l
inst✝ : T2Space R
f : X → (i : l) → Matrix (m' i) (n' i) R
hf : ¬Summable f
hft : ¬Summable fun x => blockDiagonal' (f x)
⊢ blockDiagonal' (∑' (x : X), f x) = ∑' (x : X), blockDiagonal' (f x)
case neg
X : Type u_5
α : Type ?u.110701
l : Type u_1
m : Type ?u.110707
n : Type ?u.110710
p : Type ?u.110713
S : Type ?u.110716
R : Type u_2
m' : l → Type u_3
n' : l → Type u_4
inst✝⁵ : Semiring α
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : Module α R
inst✝¹ : DecidableEq l
inst✝ : T2Space R
f : X → (i : l) → Matrix (m' i) (n' i) R
hf : ¬Summable f
⊢ blockDiagonal' (∑' (x : X), f x) = ∑' (x : X), blockDiagonal' (f x)
have hft := summable_matrix_blockDiagonal'.not.mpr hf
case neg
X : Type u_5
α : Type ?u.110701
l : Type u_1
m : Type ?u.110707
n : Type ?u.110710
p : Type ?u.110713
S : Type ?u.110716
R : Type u_2
m' : l → Type u_3
n' : l → Type u_4
inst✝⁵ : Semiring α
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : Module α R
inst✝¹ : DecidableEq l
inst✝ : T2Space R
f : X → (i : l) → Matrix (m' i) (n' i) R
hf : ¬Summable f
hft : ¬Summable fun x => blockDiagonal' (f x)
⊢ blockDiagonal' 0 = 0
case neg
X : Type u_5
α : Type ?u.110701
l : Type u_1
m : Type ?u.110707
n : Type ?u.110710
p : Type ?u.110713
S : Type ?u.110716
R : Type u_2
m' : l → Type u_3
n' : l → Type u_4
inst✝⁵ : Semiring α
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : Module α R
inst✝¹ : DecidableEq l
inst✝ : T2Space R
f : X → (i : l) → Matrix (m' i) (n' i) R
hf : ¬Summable f
hft : ¬Summable fun x => blockDiagonal' (f x)
⊢ blockDiagonal' (∑' (x : X), f x) = ∑' (x : X), blockDiagonal' (f x)
rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable hft]
no goals
case neg
X : Type u_5
α : Type ?u.110701
l : Type u_1
m : Type ?u.110707
n : Type ?u.110710
p : Type ?u.110713
S : Type ?u.110716
R : Type u_2
m' : l → Type u_3
n' : l → Type u_4
inst✝⁵ : Semiring α
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : Module α R
inst✝¹ : DecidableEq l
inst✝ : T2Space R
f : X → (i : l) → Matrix (m' i) (n' i) R
hf : ¬Summable f
hft : ¬Summable fun x => blockDiagonal' (f x)
⊢ blockDiagonal' 0 = 0
exact blockDiagonal'_zero