[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
r : ℝ
hr : 0 ≤ r
A : Matrix m n α
⊢ ‖A‖ ≤ r ↔ ∀ (i : m) (j : n), ‖A i j‖ ≤ r
[PROOFSTEP]
simp_rw [norm_def, pi_norm_le_iff_of_nonneg hr]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
r : ℝ≥0
A : Matrix m n α
⊢ ‖A‖₊ ≤ r ↔ ∀ (i : m) (j : n), ‖A i j‖₊ ≤ r
[PROOFSTEP]
simp_rw [nnnorm_def, pi_nnnorm_le_iff]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
r : ℝ
hr : 0 < r
A : Matrix m n α
⊢ ‖A‖ < r ↔ ∀ (i : m) (j : n), ‖A i j‖ < r
[PROOFSTEP]
simp_rw [norm_def, pi_norm_lt_iff hr]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
r : ℝ≥0
hr : 0 < r
A : Matrix m n α
⊢ ‖A‖₊ < r ↔ ∀ (i : m) (j : n), ‖A i j‖₊ < r
[PROOFSTEP]
simp_rw [nnnorm_def, pi_nnnorm_lt_iff hr]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
A : Matrix m n α
f : α → β
hf : ∀ (a : α), ‖f a‖₊ = ‖a‖₊
⊢ ‖map A f‖₊ = ‖A‖₊
[PROOFSTEP]
simp only [nnnorm_def, Pi.nnnorm_def, Matrix.map_apply, hf]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
v : m → α
⊢ ‖col v‖₊ = ‖v‖₊
[PROOFSTEP]
simp [nnnorm_def, Pi.nnnorm_def]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
v : n → α
⊢ ‖row v‖₊ = ‖v‖₊
[PROOFSTEP]
simp [nnnorm_def, Pi.nnnorm_def]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : SeminormedAddCommGroup α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : DecidableEq n
v : n → α
⊢ ‖diagonal v‖₊ = ‖v‖₊
[PROOFSTEP]
simp_rw [nnnorm_def, Pi.nnnorm_def]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : SeminormedAddCommGroup α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : DecidableEq n
v : n → α
⊢ (Finset.sup Finset.univ fun b => Finset.sup Finset.univ fun b_1 => ‖diagonal v b b_1‖₊) =
    Finset.sup Finset.univ fun b => ‖v b‖₊
[PROOFSTEP]
congr 1 with i : 1
[GOAL]
case e_f.h
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : SeminormedAddCommGroup α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : DecidableEq n
v : n → α
i : n
⊢ (Finset.sup Finset.univ fun b => ‖diagonal v i b‖₊) = ‖v i‖₊
[PROOFSTEP]
refine' le_antisymm (Finset.sup_le fun j hj => _) _
[GOAL]
case e_f.h.refine'_1
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : SeminormedAddCommGroup α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : DecidableEq n
v : n → α
i j : n
hj : j ∈ Finset.univ
⊢ ‖diagonal v i j‖₊ ≤ ‖v i‖₊
[PROOFSTEP]
obtain rfl | hij := eq_or_ne i j
[GOAL]
case e_f.h.refine'_1.inl
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : SeminormedAddCommGroup α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : DecidableEq n
v : n → α
i : n
hj : i ∈ Finset.univ
⊢ ‖diagonal v i i‖₊ ≤ ‖v i‖₊
[PROOFSTEP]
rw [diagonal_apply_eq]
[GOAL]
case e_f.h.refine'_1.inr
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : SeminormedAddCommGroup α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : DecidableEq n
v : n → α
i j : n
hj : j ∈ Finset.univ
hij : i ≠ j
⊢ ‖diagonal v i j‖₊ ≤ ‖v i‖₊
[PROOFSTEP]
rw [diagonal_apply_ne _ hij, nnnorm_zero]
[GOAL]
case e_f.h.refine'_1.inr
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : SeminormedAddCommGroup α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : DecidableEq n
v : n → α
i j : n
hj : j ∈ Finset.univ
hij : i ≠ j
⊢ 0 ≤ ‖v i‖₊
[PROOFSTEP]
exact zero_le _
[GOAL]
case e_f.h.refine'_2
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : SeminormedAddCommGroup α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : DecidableEq n
v : n → α
i : n
⊢ ‖v i‖₊ ≤ Finset.sup Finset.univ fun b => ‖diagonal v i b‖₊
[PROOFSTEP]
refine' Eq.trans_le _ (Finset.le_sup (Finset.mem_univ i))
[GOAL]
case e_f.h.refine'_2
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : SeminormedAddCommGroup α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : DecidableEq n
v : n → α
i : n
⊢ ‖v i‖₊ = ‖diagonal v i i‖₊
[PROOFSTEP]
rw [diagonal_apply_eq]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
⊢ SeminormedAddCommGroup (m → PiLp 1 fun j => α)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NormedAddCommGroup α
⊢ NormedAddCommGroup (m → PiLp 1 fun j => α)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NormedField R
inst✝¹ : SeminormedAddCommGroup α
inst✝ : NormedSpace R α
⊢ NormedSpace R (m → PiLp 1 fun j => α)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
A : Matrix m n α
⊢ ‖A‖ = ↑(Finset.sup Finset.univ fun i => ∑ j : n, ‖A i j‖₊)
[PROOFSTEP]
change ‖fun i => (PiLp.equiv 1 _).symm (A i)‖ = _
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
A : Matrix m n α
⊢ ‖fun i => ↑(PiLp.equiv 1 fun i => α).symm (A i)‖ = ↑(Finset.sup Finset.univ fun i => ∑ j : n, ‖A i j‖₊)
[PROOFSTEP]
simp [Pi.norm_def, PiLp.nnnorm_eq_sum ENNReal.one_ne_top]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
v : m → α
⊢ ‖col v‖₊ = ‖v‖₊
[PROOFSTEP]
rw [linfty_op_nnnorm_def, Pi.nnnorm_def]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
v : m → α
⊢ (Finset.sup Finset.univ fun i => ∑ j : Unit, ‖col v i j‖₊) = Finset.sup Finset.univ fun b => ‖v b‖₊
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
v : n → α
⊢ ‖row v‖₊ = ∑ i : n, ‖v i‖₊
[PROOFSTEP]
simp [linfty_op_nnnorm_def]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
v : n → α
⊢ ↑(∑ i : n, ‖v i‖₊) = ∑ i : n, ‖v i‖
[PROOFSTEP]
simp [NNReal.coe_sum]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq m
v : m → α
⊢ ‖diagonal v‖₊ = ‖v‖₊
[PROOFSTEP]
rw [linfty_op_nnnorm_def, Pi.nnnorm_def]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq m
v : m → α
⊢ (Finset.sup Finset.univ fun i => ∑ j : m, ‖diagonal v i j‖₊) = Finset.sup Finset.univ fun b => ‖v b‖₊
[PROOFSTEP]
congr 1 with i : 1
[GOAL]
case e_f.h
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq m
v : m → α
i : m
⊢ ∑ j : m, ‖diagonal v i j‖₊ = ‖v i‖₊
[PROOFSTEP]
refine' (Finset.sum_eq_single_of_mem _ (Finset.mem_univ i) fun j _hj hij => _).trans _
[GOAL]
case e_f.h.refine'_1
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq m
v : m → α
i j : m
_hj : j ∈ Finset.univ
hij : j ≠ i
⊢ ‖diagonal v i j‖₊ = 0
[PROOFSTEP]
rw [diagonal_apply_ne' _ hij, nnnorm_zero]
[GOAL]
case e_f.h.refine'_2
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq m
v : m → α
i : m
⊢ ‖diagonal v i i‖₊ = ‖v i‖₊
[PROOFSTEP]
rw [diagonal_apply_eq]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
⊢ ‖A * B‖₊ ≤ ‖A‖₊ * ‖B‖₊
[PROOFSTEP]
simp_rw [linfty_op_nnnorm_def, Matrix.mul_apply]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
⊢ (Finset.sup Finset.univ fun i => ∑ x : n, ‖∑ j : m, A i j * B j x‖₊) ≤
    (Finset.sup Finset.univ fun i => ∑ j : m, ‖A i j‖₊) * Finset.sup Finset.univ fun i => ∑ j : n, ‖B i j‖₊
[PROOFSTEP]
calc
  (Finset.univ.sup fun i => ∑ k, ‖∑ j, A i j * B j k‖₊) ≤ Finset.univ.sup fun i => ∑ k, ∑ j, ‖A i j‖₊ * ‖B j k‖₊ :=
    Finset.sup_mono_fun fun i _hi => Finset.sum_le_sum fun k _hk => nnnorm_sum_le_of_le _ fun j _hj => nnnorm_mul_le _ _
  _ = Finset.univ.sup fun i => ∑ j, ‖A i j‖₊ * ∑ k, ‖B j k‖₊ := by simp_rw [@Finset.sum_comm _ m n, Finset.mul_sum]
  _ ≤ Finset.univ.sup fun i => ∑ j, ‖A i j‖₊ * Finset.univ.sup fun i => ∑ j, ‖B i j‖₊ :=
    by
    refine Finset.sup_mono_fun fun i _hi => ?_
    gcongr with j hj
    exact Finset.le_sup (f := fun i ↦ ∑ k : n, ‖B i k‖₊) hj
  _ ≤ (Finset.univ.sup fun i => ∑ j, ‖A i j‖₊) * Finset.univ.sup fun i => ∑ j, ‖B i j‖₊ :=
    by
    simp_rw [← Finset.sum_mul, ← NNReal.finset_sup_mul]
    rfl
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
⊢ (Finset.sup Finset.univ fun i => ∑ k : n, ∑ j : m, ‖A i j‖₊ * ‖B j k‖₊) =
    Finset.sup Finset.univ fun i => ∑ j : m, ‖A i j‖₊ * ∑ k : n, ‖B j k‖₊
[PROOFSTEP]
simp_rw [@Finset.sum_comm _ m n, Finset.mul_sum]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
⊢ (Finset.sup Finset.univ fun i => ∑ j : m, ‖A i j‖₊ * ∑ k : n, ‖B j k‖₊) ≤
    Finset.sup Finset.univ fun i => ∑ j : m, ‖A i j‖₊ * Finset.sup Finset.univ fun i => ∑ j : n, ‖B i j‖₊
[PROOFSTEP]
refine Finset.sup_mono_fun fun i _hi => ?_
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
i : l
_hi : i ∈ Finset.univ
⊢ ∑ j : m, ‖A i j‖₊ * ∑ k : n, ‖B j k‖₊ ≤ ∑ j : m, ‖A i j‖₊ * Finset.sup Finset.univ fun i => ∑ j : n, ‖B i j‖₊
[PROOFSTEP]
gcongr with j hj
[GOAL]
case h.bc
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
i : l
_hi : i ∈ Finset.univ
j : m
hj : j ∈ Finset.univ
⊢ ∑ k : n, ‖B j k‖₊ ≤ Finset.sup Finset.univ fun i => ∑ j : n, ‖B i j‖₊
[PROOFSTEP]
exact Finset.le_sup (f := fun i ↦ ∑ k : n, ‖B i k‖₊) hj
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
⊢ (Finset.sup Finset.univ fun i => ∑ j : m, ‖A i j‖₊ * Finset.sup Finset.univ fun i => ∑ j : n, ‖B i j‖₊) ≤
    (Finset.sup Finset.univ fun i => ∑ j : m, ‖A i j‖₊) * Finset.sup Finset.univ fun i => ∑ j : n, ‖B i j‖₊
[PROOFSTEP]
simp_rw [← Finset.sum_mul, ← NNReal.finset_sup_mul]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
⊢ ((Finset.sup Finset.univ fun a => ∑ x : m, ‖A a x‖₊) * Finset.sup Finset.univ fun i => ∑ j : n, ‖B i j‖₊) ≤
    (Finset.sup Finset.univ fun i => ∑ j : m, ‖A i j‖₊) * Finset.sup Finset.univ fun i => ∑ j : n, ‖B i j‖₊
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalSeminormedRing α
A : Matrix l m α
v : m → α
⊢ ‖mulVec A v‖₊ ≤ ‖A‖₊ * ‖v‖₊
[PROOFSTEP]
rw [← linfty_op_nnnorm_col (A.mulVec v), ← linfty_op_nnnorm_col v]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalSeminormedRing α
A : Matrix l m α
v : m → α
⊢ ‖col (mulVec A v)‖₊ ≤ ‖A‖₊ * ‖col v‖₊
[PROOFSTEP]
exact linfty_op_nnnorm_mul A (col v)
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NormedAddCommGroup α
⊢ NormedAddCommGroup (PiLp 2 fun i => PiLp 2 fun j => α)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NormedField R
inst✝¹ : SeminormedAddCommGroup α
inst✝ : NormedSpace R α
⊢ NormedSpace R (PiLp 2 fun i => PiLp 2 fun j => α)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
A : Matrix m n α
⊢ ‖A‖₊ = (∑ i : m, ∑ j : n, ‖A i j‖₊ ^ 2) ^ (1 / 2)
[PROOFSTEP]
change ‖(PiLp.equiv 2 _).symm <| fun i => (PiLp.equiv 2 _).symm <| fun j => A i j‖₊ = _
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
A : Matrix m n α
⊢ ‖↑(PiLp.equiv 2 fun i => (fun x => PiLp 2 fun j => α) fun j => A i j).symm fun i =>
        ↑(PiLp.equiv 2 fun j => α).symm fun j => A i j‖₊ =
    (∑ i : m, ∑ j : n, ‖A i j‖₊ ^ 2) ^ (1 / 2)
[PROOFSTEP]
simp_rw [PiLp.nnnorm_eq_of_L2, NNReal.sq_sqrt, NNReal.sqrt_eq_rpow, NNReal.rpow_two, PiLp.equiv_symm_apply]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
A : Matrix m n α
⊢ ↑((∑ i : m, ∑ j : n, ‖A i j‖₊ ^ 2) ^ (1 / 2)) = (∑ i : m, ∑ j : n, ‖A i j‖ ^ 2) ^ (1 / 2)
[PROOFSTEP]
simp [NNReal.coe_sum]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
A : Matrix m n α
f : α → β
hf : ∀ (a : α), ‖f a‖₊ = ‖a‖₊
⊢ ‖map A f‖₊ = ‖A‖₊
[PROOFSTEP]
simp_rw [frobenius_nnnorm_def, Matrix.map_apply, hf]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
A : Matrix m n α
⊢ ‖Aᵀ‖₊ = ‖A‖₊
[PROOFSTEP]
rw [frobenius_nnnorm_def, frobenius_nnnorm_def, Finset.sum_comm]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
A : Matrix m n α
⊢ (∑ y : m, ∑ x : n, ‖Aᵀ x y‖₊ ^ 2) ^ (1 / 2) = (∑ i : m, ∑ j : n, ‖A i j‖₊ ^ 2) ^ (1 / 2)
[PROOFSTEP]
simp_rw [Matrix.transpose_apply]
  -- porting note: added
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
v : m → α
⊢ ‖row v‖ = ‖↑(PiLp.equiv 2 fun i => α).symm v‖
[PROOFSTEP]
rw [frobenius_norm_def, Fintype.sum_unique, PiLp.norm_eq_of_L2, Real.sqrt_eq_rpow]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
v : m → α
⊢ (∑ j : m, ‖row v default j‖ ^ 2) ^ (1 / 2) = (∑ i : m, ‖↑(PiLp.equiv 2 fun i => α).symm v i‖ ^ 2) ^ (1 / 2)
[PROOFSTEP]
simp only [row_apply, Real.rpow_two, PiLp.equiv_symm_apply]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
v : n → α
⊢ ‖col v‖ = ‖↑(PiLp.equiv 2 fun i => α).symm v‖
[PROOFSTEP]
simp_rw [frobenius_norm_def, Fintype.sum_unique, PiLp.norm_eq_of_L2, Real.sqrt_eq_rpow]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
v : n → α
⊢ (∑ x : n, ‖col v x default‖ ^ 2) ^ (1 / 2) = (∑ i : n, ‖↑(PiLp.equiv 2 fun i => α).symm v i‖ ^ 2) ^ (1 / 2)
[PROOFSTEP]
simp only [col_apply, Real.rpow_two, PiLp.equiv_symm_apply]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : SeminormedAddCommGroup α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : DecidableEq n
v : n → α
⊢ ‖diagonal v‖₊ = ‖↑(PiLp.equiv 2 fun i => α).symm v‖₊
[PROOFSTEP]
simp_rw [frobenius_nnnorm_def, ← Finset.sum_product', Finset.univ_product_univ, PiLp.nnnorm_eq_of_L2]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : SeminormedAddCommGroup α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : DecidableEq n
v : n → α
⊢ (∑ x : n × n, ‖diagonal v x.fst x.snd‖₊ ^ 2) ^ (1 / 2) =
    ↑NNReal.sqrt (∑ i : n, ‖↑(PiLp.equiv 2 fun i => α).symm v i‖₊ ^ 2)
[PROOFSTEP]
let s := (Finset.univ : Finset n).map ⟨fun i : n => (i, i), fun i j h => congr_arg Prod.fst h⟩
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : SeminormedAddCommGroup α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : DecidableEq n
v : n → α
s : Finset (n × n) :=
  Finset.map
    { toFun := fun i => (i, i),
      inj' :=
        (_ :
          ∀ (i j : n),
            (fun i => (i, i)) i = (fun i => (i, i)) j → ((fun i => (i, i)) i).fst = ((fun i => (i, i)) j).fst) }
    Finset.univ
⊢ (∑ x : n × n, ‖diagonal v x.fst x.snd‖₊ ^ 2) ^ (1 / 2) =
    ↑NNReal.sqrt (∑ i : n, ‖↑(PiLp.equiv 2 fun i => α).symm v i‖₊ ^ 2)
[PROOFSTEP]
rw [← Finset.sum_subset (Finset.subset_univ s) fun i _hi his => ?_]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : SeminormedAddCommGroup α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : DecidableEq n
v : n → α
s : Finset (n × n) :=
  Finset.map
    { toFun := fun i => (i, i),
      inj' :=
        (_ :
          ∀ (i j : n),
            (fun i => (i, i)) i = (fun i => (i, i)) j → ((fun i => (i, i)) i).fst = ((fun i => (i, i)) j).fst) }
    Finset.univ
⊢ (∑ x in s, ‖diagonal v x.fst x.snd‖₊ ^ 2) ^ (1 / 2) =
    ↑NNReal.sqrt (∑ i : n, ‖↑(PiLp.equiv 2 fun i => α).symm v i‖₊ ^ 2)
[PROOFSTEP]
rw [Finset.sum_map, NNReal.sqrt_eq_rpow]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : SeminormedAddCommGroup α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : DecidableEq n
v : n → α
s : Finset (n × n) :=
  Finset.map
    { toFun := fun i => (i, i),
      inj' :=
        (_ :
          ∀ (i j : n),
            (fun i => (i, i)) i = (fun i => (i, i)) j → ((fun i => (i, i)) i).fst = ((fun i => (i, i)) j).fst) }
    Finset.univ
⊢ (∑ x : n,
        ‖diagonal v
              (↑{ toFun := fun i => (i, i),
                      inj' :=
                        (_ :
                          ∀ (i j : n),
                            (fun i => (i, i)) i = (fun i => (i, i)) j →
                              ((fun i => (i, i)) i).fst = ((fun i => (i, i)) j).fst) }
                  x).fst
              (↑{ toFun := fun i => (i, i),
                      inj' :=
                        (_ :
                          ∀ (i j : n),
                            (fun i => (i, i)) i = (fun i => (i, i)) j →
                              ((fun i => (i, i)) i).fst = ((fun i => (i, i)) j).fst) }
                  x).snd‖₊ ^
          2) ^
      (1 / 2) =
    (∑ i : n, ‖↑(PiLp.equiv 2 fun i => α).symm v i‖₊ ^ 2) ^ (1 / 2)
[PROOFSTEP]
dsimp
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : SeminormedAddCommGroup α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : DecidableEq n
v : n → α
s : Finset (n × n) :=
  Finset.map
    { toFun := fun i => (i, i),
      inj' :=
        (_ :
          ∀ (i j : n),
            (fun i => (i, i)) i = (fun i => (i, i)) j → ((fun i => (i, i)) i).fst = ((fun i => (i, i)) j).fst) }
    Finset.univ
⊢ (∑ x : n, ‖diagonal v x x‖₊ ^ 2) ^ (1 / 2) = (∑ i : n, ‖v i‖₊ ^ 2) ^ (1 / 2)
[PROOFSTEP]
simp_rw [diagonal_apply_eq, NNReal.rpow_two]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : SeminormedAddCommGroup α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : DecidableEq n
v : n → α
s : Finset (n × n) :=
  Finset.map
    { toFun := fun i => (i, i),
      inj' :=
        (_ :
          ∀ (i j : n),
            (fun i => (i, i)) i = (fun i => (i, i)) j → ((fun i => (i, i)) i).fst = ((fun i => (i, i)) j).fst) }
    Finset.univ
i : n × n
_hi : i ∈ Finset.univ
his : ¬i ∈ s
⊢ ‖diagonal v i.fst i.snd‖₊ ^ 2 = 0
[PROOFSTEP]
suffices i.1 ≠ i.2 by rw [diagonal_apply_ne _ this, nnnorm_zero, NNReal.zero_rpow two_ne_zero]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : SeminormedAddCommGroup α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : DecidableEq n
v : n → α
s : Finset (n × n) :=
  Finset.map
    { toFun := fun i => (i, i),
      inj' :=
        (_ :
          ∀ (i j : n),
            (fun i => (i, i)) i = (fun i => (i, i)) j → ((fun i => (i, i)) i).fst = ((fun i => (i, i)) j).fst) }
    Finset.univ
i : n × n
_hi : i ∈ Finset.univ
his : ¬i ∈ s
this : i.fst ≠ i.snd
⊢ ‖diagonal v i.fst i.snd‖₊ ^ 2 = 0
[PROOFSTEP]
rw [diagonal_apply_ne _ this, nnnorm_zero, NNReal.zero_rpow two_ne_zero]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : SeminormedAddCommGroup α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : DecidableEq n
v : n → α
s : Finset (n × n) :=
  Finset.map
    { toFun := fun i => (i, i),
      inj' :=
        (_ :
          ∀ (i j : n),
            (fun i => (i, i)) i = (fun i => (i, i)) j → ((fun i => (i, i)) i).fst = ((fun i => (i, i)) j).fst) }
    Finset.univ
i : n × n
_hi : i ∈ Finset.univ
his : ¬i ∈ s
⊢ i.fst ≠ i.snd
[PROOFSTEP]
intro h
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : SeminormedAddCommGroup α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : DecidableEq n
v : n → α
s : Finset (n × n) :=
  Finset.map
    { toFun := fun i => (i, i),
      inj' :=
        (_ :
          ∀ (i j : n),
            (fun i => (i, i)) i = (fun i => (i, i)) j → ((fun i => (i, i)) i).fst = ((fun i => (i, i)) j).fst) }
    Finset.univ
i : n × n
_hi : i ∈ Finset.univ
his : ¬i ∈ s
h : i.fst = i.snd
⊢ False
[PROOFSTEP]
exact Finset.mem_map.not.mp his ⟨i.1, Finset.mem_univ _, Prod.ext rfl h⟩
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : One α
⊢ ‖1‖₊ = ↑NNReal.sqrt ↑(Fintype.card n) * ‖1‖₊
[PROOFSTEP]
refine'
  (frobenius_nnnorm_diagonal _).trans
    _
      -- porting note: change to erw, since `fun x => 1` no longer matches `Function.const`
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : One α
⊢ ‖↑(PiLp.equiv 2 fun i => α).symm fun x => 1‖₊ = ↑NNReal.sqrt ↑(Fintype.card n) * ‖1‖₊
[PROOFSTEP]
erw [PiLp.nnnorm_equiv_symm_const ENNReal.two_ne_top]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : One α
⊢ ↑(Fintype.card n) ^ ENNReal.toReal (1 / 2) * ‖1‖₊ = ↑NNReal.sqrt ↑(Fintype.card n) * ‖1‖₊
[PROOFSTEP]
simp_rw [NNReal.sqrt_eq_rpow]
  -- porting note: added `ENNReal.toReal_ofNat`
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : One α
⊢ ↑(Fintype.card n) ^ ENNReal.toReal (1 / 2) * ‖1‖₊ = ↑(Fintype.card n) ^ (1 / 2) * ‖1‖₊
[PROOFSTEP]
simp only [ENNReal.toReal_div, ENNReal.one_toReal, ENNReal.toReal_ofNat]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : IsROrC α
A : Matrix l m α
B : Matrix m n α
⊢ ‖A * B‖₊ ≤ ‖A‖₊ * ‖B‖₊
[PROOFSTEP]
simp_rw [frobenius_nnnorm_def, Matrix.mul_apply]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : IsROrC α
A : Matrix l m α
B : Matrix m n α
⊢ (∑ x : l, ∑ x_1 : n, ‖∑ j : m, A x j * B j x_1‖₊ ^ 2) ^ (1 / 2) ≤
    (∑ i : l, ∑ j : m, ‖A i j‖₊ ^ 2) ^ (1 / 2) * (∑ i : m, ∑ j : n, ‖B i j‖₊ ^ 2) ^ (1 / 2)
[PROOFSTEP]
rw [← NNReal.mul_rpow, @Finset.sum_comm _ n m, Finset.sum_mul_sum, Finset.sum_product]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : IsROrC α
A : Matrix l m α
B : Matrix m n α
⊢ (∑ x : l, ∑ x_1 : n, ‖∑ j : m, A x j * B j x_1‖₊ ^ 2) ^ (1 / 2) ≤
    (∑ x : l, ∑ y : n, (∑ j : m, ‖A (x, y).fst j‖₊ ^ 2) * ∑ x_1 : m, ‖B x_1 (x, y).snd‖₊ ^ 2) ^ (1 / 2)
[PROOFSTEP]
refine' NNReal.rpow_le_rpow _ one_half_pos.le
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : IsROrC α
A : Matrix l m α
B : Matrix m n α
⊢ ∑ x : l, ∑ x_1 : n, ‖∑ j : m, A x j * B j x_1‖₊ ^ 2 ≤
    ∑ x : l, ∑ y : n, (∑ j : m, ‖A (x, y).fst j‖₊ ^ 2) * ∑ x_1 : m, ‖B x_1 (x, y).snd‖₊ ^ 2
[PROOFSTEP]
refine' Finset.sum_le_sum fun i _ => Finset.sum_le_sum fun j _ => _
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : IsROrC α
A : Matrix l m α
B : Matrix m n α
i : l
x✝¹ : i ∈ Finset.univ
j : n
x✝ : j ∈ Finset.univ
⊢ ‖∑ j_1 : m, A i j_1 * B j_1 j‖₊ ^ 2 ≤ (∑ j_1 : m, ‖A (i, j).fst j_1‖₊ ^ 2) * ∑ x : m, ‖B x (i, j).snd‖₊ ^ 2
[PROOFSTEP]
rw [← NNReal.rpow_le_rpow_iff one_half_pos, ← NNReal.rpow_mul, mul_div_cancel' (1 : ℝ) two_ne_zero, NNReal.rpow_one,
  NNReal.mul_rpow]
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : IsROrC α
A : Matrix l m α
B : Matrix m n α
i : l
x✝¹ : i ∈ Finset.univ
j : n
x✝ : j ∈ Finset.univ
⊢ ‖∑ j_1 : m, A i j_1 * B j_1 j‖₊ ≤
    (∑ j_1 : m, ‖A (i, j).fst j_1‖₊ ^ 2) ^ (1 / 2) * (∑ x : m, ‖B x (i, j).snd‖₊ ^ 2) ^ (1 / 2)
[PROOFSTEP]
dsimp only
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : IsROrC α
A : Matrix l m α
B : Matrix m n α
i : l
x✝¹ : i ∈ Finset.univ
j : n
x✝ : j ∈ Finset.univ
⊢ ‖∑ j_1 : m, A i j_1 * B j_1 j‖₊ ≤ (∑ j : m, ‖A i j‖₊ ^ 2) ^ (1 / 2) * (∑ x : m, ‖B x j‖₊ ^ 2) ^ (1 / 2)
[PROOFSTEP]
have :=
  @nnnorm_inner_le_nnnorm α _ _ _ _ ((PiLp.equiv 2 fun _ => α).symm fun j => star (A i j))
    ((PiLp.equiv 2 fun _ => α).symm fun k => B k j)
[GOAL]
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : IsROrC α
A : Matrix l m α
B : Matrix m n α
i : l
x✝¹ : i ∈ Finset.univ
j : n
x✝ : j ∈ Finset.univ
this :
  ‖inner (↑(PiLp.equiv 2 fun x => α).symm fun j => star (A i j)) (↑(PiLp.equiv 2 fun x => α).symm fun k => B k j)‖₊ ≤
    ‖↑(PiLp.equiv 2 fun x => α).symm fun j => star (A i j)‖₊ * ‖↑(PiLp.equiv 2 fun x => α).symm fun k => B k j‖₊
⊢ ‖∑ j_1 : m, A i j_1 * B j_1 j‖₊ ≤ (∑ j : m, ‖A i j‖₊ ^ 2) ^ (1 / 2) * (∑ x : m, ‖B x j‖₊ ^ 2) ^ (1 / 2)
[PROOFSTEP]
simpa only [PiLp.equiv_symm_apply, PiLp.inner_apply, IsROrC.inner_apply, starRingEnd_apply, Pi.nnnorm_def,
  PiLp.nnnorm_eq_of_L2, star_star, nnnorm_star, NNReal.sqrt_eq_rpow, NNReal.rpow_two] using this
