α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
f : α → E
hf : Summable f
⊢ Summable fun x => ‖f x‖
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
f : α → E
⊢ (Summable fun x => ‖f x‖) ↔ Summable f
refine' ⟨summable_of_summable_norm, fun hf => _⟩
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
f : α → E
hf : Summable f
⊢ ∀ {N : ℕ} {g : α → Fin N → ℝ}, Summable g → Summable fun x => ‖g x‖
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
f : α → E
hf : Summable f
⊢ Summable fun x => ‖f x‖
suffices ∀ {N : ℕ} {g : α → Fin N → ℝ}, Summable g → Summable fun x => ‖g x‖ by
  obtain v := finBasis ℝ E
  set e := v.equivFunL
  have : Summable fun x => ‖e (f x)‖ := this (e.summable.2 hf)
  refine'
    summable_of_norm_bounded _ (this.mul_left ↑‖(e.symm : (Fin (finrank ℝ E) → ℝ) →L[ℝ] E)‖₊)
      fun i => _
  simpa using (e.symm : (Fin (finrank ℝ E) → ℝ) →L[ℝ] E).le_op_norm (e <| f i)
α : Type u_1
⊢ ∀ {N : ℕ} {g : α → Fin N → ℝ}, Summable g → Summable fun x => ‖g x‖
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
f : α → E
hf : Summable f
⊢ ∀ {N : ℕ} {g : α → Fin N → ℝ}, Summable g → Summable fun x => ‖g x‖
clear! E
α : Type u_1
N : ℕ
g : α → Fin N → ℝ
hg : Summable g
⊢ Summable fun x => ‖g x‖
α : Type u_1
⊢ ∀ {N : ℕ} {g : α → Fin N → ℝ}, Summable g → Summable fun x => ‖g x‖
intro N g hg
α : Type u_1
N : ℕ
g : α → Fin N → ℝ
hg : Summable g
this : ∀ (i : Fin N), Summable fun x => ‖g x i‖
⊢ Summable fun x => ‖g x‖
α : Type u_1
N : ℕ
g : α → Fin N → ℝ
hg : Summable g
⊢ Summable fun x => ‖g x‖
have : ∀ i, Summable fun x => ‖g x i‖ := fun i => (Pi.summable.1 hg i).abs
α : Type u_1
N : ℕ
g : α → Fin N → ℝ
hg : Summable g
this : ∀ (i : Fin N), Summable fun x => ‖g x i‖
x : α
⊢ ‖‖g x‖‖ ≤ ∑ i : Fin N, ‖g x i‖
α : Type u_1
N : ℕ
g : α → Fin N → ℝ
hg : Summable g
this : ∀ (i : Fin N), Summable fun x => ‖g x i‖
⊢ Summable fun x => ‖g x‖
refine'
  summable_of_norm_bounded _ (summable_sum fun i (_ : i ∈ Finset.univ) => this i) fun x => _
α : Type u_1
N : ℕ
g : α → Fin N → ℝ
hg : Summable g
this : ∀ (i : Fin N), Summable fun x => ‖g x i‖
x : α
⊢ ∀ (i : Fin N), ‖g x i‖ ≤ ∑ i : Fin N, ‖g x i‖

α : Type u_1
N : ℕ
g : α → Fin N → ℝ
hg : Summable g
this : ∀ (i : Fin N), Summable fun x => ‖g x i‖
x : α
⊢ 0 ≤ ∑ i : Fin N, ‖g x i‖
α : Type u_1
N : ℕ
g : α → Fin N → ℝ
hg : Summable g
this : ∀ (i : Fin N), Summable fun x => ‖g x i‖
x : α
⊢ ‖‖g x‖‖ ≤ ∑ i : Fin N, ‖g x i‖
rw [norm_norm, pi_norm_le_iff_of_nonneg]
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
f : α → E
hf : Summable f
this : ∀ {N : ℕ} {g : α → Fin N → ℝ}, Summable g → Summable fun x => ‖g x‖
v : Basis (Fin (finrank ℝ E)) ℝ E
⊢ Summable fun x => ‖f x‖
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
f : α → E
hf : Summable f
this : ∀ {N : ℕ} {g : α → Fin N → ℝ}, Summable g → Summable fun x => ‖g x‖
⊢ Summable fun x => ‖f x‖
obtain v := finBasis ℝ E
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
f : α → E
hf : Summable f
this : ∀ {N : ℕ} {g : α → Fin N → ℝ}, Summable g → Summable fun x => ‖g x‖
v : Basis (Fin (finrank ℝ E)) ℝ E
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := Basis.equivFunL v
⊢ Summable fun x => ‖f x‖
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
f : α → E
hf : Summable f
this : ∀ {N : ℕ} {g : α → Fin N → ℝ}, Summable g → Summable fun x => ‖g x‖
v : Basis (Fin (finrank ℝ E)) ℝ E
⊢ Summable fun x => ‖f x‖
set e := v.equivFunL
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
f : α → E
hf : Summable f
this✝ : ∀ {N : ℕ} {g : α → Fin N → ℝ}, Summable g → Summable fun x => ‖g x‖
v : Basis (Fin (finrank ℝ E)) ℝ E
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := Basis.equivFunL v
this : Summable fun x => ‖↑e (f x)‖
⊢ Summable fun x => ‖f x‖
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
f : α → E
hf : Summable f
this : ∀ {N : ℕ} {g : α → Fin N → ℝ}, Summable g → Summable fun x => ‖g x‖
v : Basis (Fin (finrank ℝ E)) ℝ E
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := Basis.equivFunL v
⊢ Summable fun x => ‖f x‖
have : Summable fun x => ‖e (f x)‖ := this (e.summable.2 hf)
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
f : α → E
hf : Summable f
this✝ : ∀ {N : ℕ} {g : α → Fin N → ℝ}, Summable g → Summable fun x => ‖g x‖
v : Basis (Fin (finrank ℝ E)) ℝ E
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := Basis.equivFunL v
this : Summable fun x => ‖↑e (f x)‖
i : α
⊢ ‖‖f i‖‖ ≤ ↑‖↑(ContinuousLinearEquiv.symm e)‖₊ * ‖↑e (f i)‖
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
f : α → E
hf : Summable f
this✝ : ∀ {N : ℕ} {g : α → Fin N → ℝ}, Summable g → Summable fun x => ‖g x‖
v : Basis (Fin (finrank ℝ E)) ℝ E
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := Basis.equivFunL v
this : Summable fun x => ‖↑e (f x)‖
⊢ Summable fun x => ‖f x‖
refine'
  summable_of_norm_bounded _ (this.mul_left ↑‖(e.symm : (Fin (finrank ℝ E) → ℝ) →L[ℝ] E)‖₊)
    fun i => _
no goals
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
f : α → E
hf : Summable f
this✝ : ∀ {N : ℕ} {g : α → Fin N → ℝ}, Summable g → Summable fun x => ‖g x‖
v : Basis (Fin (finrank ℝ E)) ℝ E
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := Basis.equivFunL v
this : Summable fun x => ‖↑e (f x)‖
i : α
⊢ ‖‖f i‖‖ ≤ ↑‖↑(ContinuousLinearEquiv.symm e)‖₊ * ‖↑e (f i)‖
simpa using (e.symm : (Fin (finrank ℝ E) → ℝ) →L[ℝ] E).le_op_norm (e <| f i)
α : Type u_1
N : ℕ
g : α → Fin N → ℝ
hg : Summable g
this : ∀ (i : Fin N), Summable fun x => ‖g x i‖
x : α
i✝ i : Fin N
x✝ : i ∈ Finset.univ
⊢ 0 ≤ (fun i => ‖g x i‖) i
α : Type u_1
N : ℕ
g : α → Fin N → ℝ
hg : Summable g
this : ∀ (i : Fin N), Summable fun x => ‖g x i‖
x : α
⊢ ∀ (i : Fin N), ‖g x i‖ ≤ ∑ i : Fin N, ‖g x i‖
refine' fun i => Finset.single_le_sum (f := fun i => ‖g x i‖) (fun i _ => _) (Finset.mem_univ i)
no goals
α : Type u_1
N : ℕ
g : α → Fin N → ℝ
hg : Summable g
this : ∀ (i : Fin N), Summable fun x => ‖g x i‖
x : α
i✝ i : Fin N
x✝ : i ∈ Finset.univ
⊢ 0 ≤ (fun i => ‖g x i‖) i
exact norm_nonneg (g x i)
no goals
α : Type u_1
N : ℕ
g : α → Fin N → ℝ
hg : Summable g
this : ∀ (i : Fin N), Summable fun x => ‖g x i‖
x : α
⊢ 0 ≤ ∑ i : Fin N, ‖g x i‖
exact Finset.sum_nonneg fun _ _ => norm_nonneg _