awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
α : Type u_5
inst : NormedDivisionRing α
inst_1 : NormedAlgebra ℝ α
a : α
h : ¬‖a‖₊ = 0
neg : ‖‖a‖‖₊ * ‖a⁻¹‖₊ = 1
neg₁ : ‖‖a‖‖₊ * ‖a‖₊⁻¹ = 1
neg₂ : ‖a‖₊ * ‖a‖₊⁻¹ = 1
neg₃ neg₄ : Eq (α := ℝ≥0) 1 1
⊢ ‖‖a‖ • a⁻¹‖₊ = 1

Tactic:
rw [nnnorm_smul, nnnorm_inv, nnnorm_norm, mul_inv_cancel₀ h]

Premises used: nnnorm_inv, mul_inv_cancel₀, nnnorm_smul, nnnorm_norm
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
α : Type u_5
inst : NormedDivisionRing α
inst_1 : NormedAlgebra ℝ α
a : α
simp : (a * if a = 0 then 1 else ‖a‖ • a⁻¹) = (algebraMap ℝ α : (a : ℝ) → α) ‖a‖
⊢ a * unitOf a = (algebraMap ℝ α : (a : ℝ) → α) (↑‖a‖₊ : ℝ)

Tactic:
simp only [unitOf, coe_nnnorm]

Premises used: _private.0.Matrix.unitOf, coe_nnnorm
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
α : Type u_5
inst : NormedDivisionRing α
inst_1 : NormedAlgebra ℝ α
a : α
pos : ∀ (h : a = 0), a * 1 = (algebraMap ℝ α : (a : ℝ) → α) ‖a‖
neg : ∀ (h : ¬a = 0), a * ‖a‖ • a⁻¹ = (algebraMap ℝ α : (a : ℝ) → α) ‖a‖
⊢ (a * if a = 0 then 1 else ‖a‖ • a⁻¹) = (algebraMap ℝ α : (a : ℝ) → α) ‖a‖

Tactic:
split_ifs with h
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
α : Type u_5
inst : NormedDivisionRing α
inst_1 : NormedAlgebra ℝ α
a : α
h : a = 0
⊢ a * 1 = (algebraMap ℝ α : (a : ℝ) → α) ‖a‖

Tactic:
simp [h]
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
α : Type u_5
inst : NormedDivisionRing α
inst_1 : NormedAlgebra ℝ α
a : α
h : ¬a = 0
neg : ‖a‖ • (a * a⁻¹) = (algebraMap ℝ α : (a : ℝ) → α) ‖a‖
neg₁ : HSMul.hSMul (β := α) ‖a‖ 1 = (algebraMap ℝ α : (a : ℝ) → α) ‖a‖
neg₂ neg₃ : HSMul.hSMul (β := α) ‖a‖ 1 = HSMul.hSMul (β := α) ‖a‖ 1
⊢ a * ‖a‖ • a⁻¹ = (algebraMap ℝ α : (a : ℝ) → α) ‖a‖

Tactic:
rw [mul_smul_comm, mul_inv_cancel₀ h, Algebra.algebraMap_eq_smul_one]

Premises used: mul_inv_cancel₀, Algebra.algebraMap_eq_smul_one, mul_smul_comm
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : NontriviallyNormedField α
inst_3 : NormedAlgebra ℝ α
A : Matrix m n α
rw :
  ∀ (N : ℝ≥0)
    (hN :
      ∀ (x : n → α),
        nnnorm (E := m → α)
            (({ toLinearMap := A.mulVecLin, cont := ⋯ : (n → α) →L[α] m → α } : (a : n → α) → m → α) x : m → α) ≤
          N * ‖x‖₊),
    ‖A‖₊ ≤ N
⊢ ‖A‖₊ = nnnorm (E := (n → α) →L[α] m → α) { toLinearMap := A.mulVecLin, cont := ⋯ }

Tactic:
rw [ContinuousLinearMap.opNNNorm_eq_of_bounds _ (linfty_opNNNorm_mulVec _) fun N hN => ?_]

Premises used: ContinuousLinearMap.opNNNorm_eq_of_bounds
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : NontriviallyNormedField α
inst_3 : NormedAlgebra ℝ α
A : Matrix m n α
N : ℝ≥0
hN :
  ∀ (x : n → α),
    nnnorm (E := m → α)
        (({ toLinearMap := A.mulVecLin, cont := ⋯ : (n → α) →L[α] m → α } : (a : n → α) → m → α) x : m → α) ≤
      N * ‖x‖₊
rw : (Finset.sup Finset.univ fun (i : m) ↦ ∑ j : n, ‖A i j‖₊) ≤ N
⊢ ‖A‖₊ ≤ N

Tactic:
rw [linfty_opNNNorm_def]

Premises used: Matrix.linfty_opNNNorm_def
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : NontriviallyNormedField α
inst_3 : NormedAlgebra ℝ α
A : Matrix m n α
N : ℝ≥0
hN :
  ∀ (x : n → α),
    nnnorm (E := m → α)
        (({ toLinearMap := A.mulVecLin, cont := ⋯ : (n → α) →L[α] m → α } : (a : n → α) → m → α) x : m → α) ≤
      N * ‖x‖₊
⊢ (Finset.sup Finset.univ fun (i : m) ↦ ∑ j : n, ‖A i j‖₊) ≤ N

Tactic:
Finset.sup_le fun i _ => ?_

Premises used: Finset.sup_le
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : NontriviallyNormedField α
inst_3 : NormedAlgebra ℝ α
A : Matrix m n α
N : ℝ≥0
hN :
  ∀ (x : n → α),
    nnnorm (E := m → α)
        (({ toLinearMap := A.mulVecLin, cont := ⋯ : (n → α) →L[α] m → α } : (a : n → α) → m → α) x : m → α) ≤
      N * ‖x‖₊
refine : ∀ (i : m), Membership.mem (γ := Finset m) Finset.univ i → ∑ j : n, ‖A i j‖₊ ≤ N
⊢ (Finset.sup Finset.univ fun (i : m) ↦ ∑ j : n, ‖A i j‖₊) ≤ N

Tactic:
refine Finset.sup_le fun i _ => ?_

Premises used: Finset.sup_le
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : NontriviallyNormedField α
inst_3 : NormedAlgebra ℝ α
A : Matrix m n α
N : ℝ≥0
hN :
  ∀ (x : n → α),
    nnnorm (E := m → α)
        (({ toLinearMap := A.mulVecLin, cont := ⋯ : (n → α) →L[α] m → α } : (a : n → α) → m → α) x : m → α) ≤
      N * ‖x‖₊
i : m
h : Membership.mem (γ := Finset m) Finset.univ i
inl : IsEmpty n → ∑ j : n, ‖A i j‖₊ ≤ N
inr : Nonempty n → ∑ j : n, ‖A i j‖₊ ≤ N
⊢ ∑ j : n, ‖A i j‖₊ ≤ N

Tactic:
cases isEmpty_or_nonempty n

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : NontriviallyNormedField α
inst_3 : NormedAlgebra ℝ α
A : Matrix m n α
N : ℝ≥0
hN :
  ∀ (x : n → α),
    nnnorm (E := m → α)
        (({ toLinearMap := A.mulVecLin, cont := ⋯ : (n → α) →L[α] m → α } : (a : n → α) → m → α) x : m → α) ≤
      N * ‖x‖₊
i : m
h : Membership.mem (γ := Finset m) Finset.univ i
h_1 : IsEmpty n
⊢ ∑ j : n, ‖A i j‖₊ ≤ N

Tactic:
simp
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : NontriviallyNormedField α
inst_3 : NormedAlgebra ℝ α
A : Matrix m n α
N : ℝ≥0
hN :
  ∀ (x : n → α),
    nnnorm (E := m → α)
        (({ toLinearMap := A.mulVecLin, cont := ⋯ : (n → α) →L[α] m → α } : (a : n → α) → m → α) x : m → α) ≤
      N * ‖x‖₊
i : m
h : Membership.mem (γ := Finset m) Finset.univ i
h_1 : Nonempty n
x : n → α := fun (j : n) ↦ unitOf (A i j)
simp_rw : (nnnorm (E := n → α) fun (j : n) ↦ unitOf (A i j)) = 1
simp_rw₁ : Eq (α := ℝ≥0) (Finset.sup Finset.univ fun (b : n) ↦ ‖unitOf (A i b)‖₊) 1
simp_rw₂ : Eq (α := ℝ≥0) (Finset.sup Finset.univ fun (b : n) ↦ 1) 1
⊢ ‖x‖₊ = 1

Tactic:
simp_rw [x, Pi.nnnorm_def, norm_unitOf, Finset.sup_const Finset.univ_nonempty]

Premises used: Finset.univ_nonempty, Finset.sup_const, _private.0.Matrix.norm_unitOf, Pi.nnnorm_def
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : NontriviallyNormedField α
inst_3 : NormedAlgebra ℝ α
A : Matrix m n α
N : ℝ≥0
hN :
  ∀ (x : n → α),
    nnnorm (E := m → α)
        (({ toLinearMap := A.mulVecLin, cont := ⋯ : (n → α) →L[α] m → α } : (a : n → α) → m → α) x : m → α) ≤
      N * ‖x‖₊
i : m
h : Membership.mem (γ := Finset m) Finset.univ i
h_1 : Nonempty n
x : n → α := fun (j : n) ↦ unitOf (A i j)
⊢ ‖x‖₊ = 1

Tactic:
have hxn : ‖x‖₊ = 1 := by
    simp_rw [x, Pi.nnnorm_def, norm_unitOf, Finset.sup_const Finset.univ_nonempty]
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : NontriviallyNormedField α
inst_3 : NormedAlgebra ℝ α
A : Matrix m n α
N : ℝ≥0
hN :
  ∀ (x : n → α),
    nnnorm (E := m → α)
        (({ toLinearMap := A.mulVecLin, cont := ⋯ : (n → α) →L[α] m → α } : (a : n → α) → m → α) x : m → α) ≤
      N * ‖x‖₊
i : m
h : Membership.mem (γ := Finset m) Finset.univ i
h_1 : Nonempty n
x : n → α := fun (j : n) ↦ unitOf (A i j)
hxn : ‖x‖₊ = 1
⊢ nnnorm (E := m → α)
      (({ toLinearMap := A.mulVecLin, cont := ⋯ : (n → α) →L[α] m → α } : (a : n → α) → m → α) x : m → α) ≤
    N * ‖x‖₊

Tactic:
specialize hN x
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : NontriviallyNormedField α
inst_3 : NormedAlgebra ℝ α
A : Matrix m n α
N : ℝ≥0
i : m
h : Membership.mem (γ := Finset m) Finset.univ i
h_1 : Nonempty n
x : n → α := fun (j : n) ↦ unitOf (A i j)
hxn : ‖x‖₊ = 1
hN :
  nnnorm (E := m → α)
      (({ toLinearMap := A.mulVecLin, cont := ⋯ : (n → α) →L[α] m → α } : (a : n → α) → m → α) x : m → α) ≤
    N * ‖x‖₊
⊢ ∀ (b : m),
    Membership.mem (γ := Finset m) Finset.univ b →
      nnnorm.{u_5} (E := α)
          (({ toLinearMap := A.mulVecLin, cont := ⋯ : (n → α) →L[α] m → α } : (a : n → α) → m → α) x b : α) ≤
        N

Tactic:
rw [hxn, mul_one, Pi.nnnorm_def, Finset.sup_le_iff] at hN

Premises used: Pi.nnnorm_def, Finset.sup_le_iff, mul_one
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : NontriviallyNormedField α
inst_3 : NormedAlgebra ℝ α
A : Matrix m n α
N : ℝ≥0
i : m
h : Membership.mem (γ := Finset m) Finset.univ i
h_1 : Nonempty n
x : n → α := fun (j : n) ↦ unitOf (A i j)
hxn : ‖x‖₊ = 1
hN :
  ∀ (b : m),
    Membership.mem (γ := Finset m) Finset.univ b →
      nnnorm.{u_5} (E := α)
          (({ toLinearMap := A.mulVecLin, cont := ⋯ : (n → α) →L[α] m → α } : (a : n → α) → m → α) x b : α) ≤
        N
⊢ nnnorm.{u_5} (E := α)
      (({ toLinearMap := A.mulVecLin, cont := ⋯ : (n → α) →L[α] m → α } : (a : n → α) → m → α) x i : α) ≤
    N

Tactic:
replace hN := hN i (Finset.mem_univ _)
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : NontriviallyNormedField α
inst_3 : NormedAlgebra ℝ α
A : Matrix m n α
N : ℝ≥0
i : m
h : Membership.mem (γ := Finset m) Finset.univ i
h_1 : Nonempty n
x : n → α := fun (j : n) ↦ unitOf (A i j)
hxn : ‖x‖₊ = 1
hN : nnnorm.{u_5} (E := α) (∑ i_1 : n, A i i_1 * x i_1) ≤ N
⊢ ∑ i_1 : n, ‖A i i_1‖₊ ≤ N

Tactic:
simp_rw [x, mul_unitOf, ← map_sum, nnnorm_algebraMap, ← NNReal.coe_sum, NNReal.nnnorm_eq,
    nnnorm_one, mul_one] at hN

Premises used: nnnorm_one, nnnorm_algebraMap, map_sum, NNReal.coe_sum, _private.0.Matrix.mul_unitOf, NNReal.nnnorm_eq, mul_one
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : NontriviallyNormedField α
inst_3 : NormedAlgebra ℝ α
A : Matrix m n α
N : ℝ≥0
i : m
h : Membership.mem (γ := Finset m) Finset.univ i
h_1 : Nonempty n
x : n → α := fun (j : n) ↦ unitOf (A i j)
hxn : ‖x‖₊ = 1
hN : ∑ i_1 : n, ‖A i i_1‖₊ ≤ N
⊢ ∑ j : n, ‖A i j‖₊ ≤ N

Tactic:
hN
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : NontriviallyNormedField α
inst_3 : NormedAlgebra ℝ α
A : Matrix m n α
N : ℝ≥0
i : m
h : Membership.mem (γ := Finset m) Finset.univ i
h_1 : Nonempty n
x : n → α := fun (j : n) ↦ unitOf (A i j)
hxn : ‖x‖₊ = 1
hN : ∑ i_1 : n, ‖A i i_1‖₊ ≤ N
⊢ ∑ j : n, ‖A i j‖₊ ≤ N

Tactic:
exact hN
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : NontriviallyNormedField α
inst_3 : NormedAlgebra ℝ α
A : Matrix m n α
N : ℝ≥0
hN :
  ∀ (x : n → α),
    nnnorm (E := m → α)
        (({ toLinearMap := A.mulVecLin, cont := ⋯ : (n → α) →L[α] m → α } : (a : n → α) → m → α) x : m → α) ≤
      N * ‖x‖₊
i : m
h : Membership.mem (γ := Finset m) Finset.univ i
h_1 : Nonempty n
inr inr₁ inr₂ : ∑ j : n, ‖A i j‖₊ ≤ N
inr₃ :
  let x : n → α := fun (j : n) ↦ unitOf (A i j);
  ∀ (hxn : ‖x‖₊ = 1), ∑ j : n, ‖A i j‖₊ ≤ N
inr₄ :
  let x : n → α := fun (j : n) ↦ unitOf (A i j);
  ∀ (hxn : ‖x‖₊ = 1)
    (hN :
      nnnorm (E := m → α)
          (({ toLinearMap := A.mulVecLin, cont := ⋯ : (n → α) →L[α] m → α } : (a : n → α) → m → α) x : m → α) ≤
        N * ‖x‖₊),
    ∑ j : n, ‖A i j‖₊ ≤ N
inr₅ :
  let x : n → α := fun (j : n) ↦ unitOf (A i j);
  ∀ (hxn : ‖x‖₊ = 1)
    (hN :
      ∀ (b : m),
        Membership.mem (γ := Finset m) Finset.univ b →
          nnnorm.{u_5} (E := α)
              (({ toLinearMap := A.mulVecLin, cont := ⋯ : (n → α) →L[α] m → α } : (a : n → α) → m → α) x b : α) ≤
            N),
    ∑ j : n, ‖A i j‖₊ ≤ N
inr₆ :
  let x : n → α := fun (j : n) ↦ unitOf (A i j);
  ∀ (hxn : ‖x‖₊ = 1)
    (hN :
      nnnorm.{u_5} (E := α)
          (({ toLinearMap := A.mulVecLin, cont := ⋯ : (n → α) →L[α] m → α } : (a : n → α) → m → α) x i : α) ≤
        N),
    ∑ j : n, ‖A i j‖₊ ≤ N
inr₇ :
  let x : n → α := fun (j : n) ↦ unitOf (A i j);
  ∀ (hxn : ‖x‖₊ = 1) (hN : nnnorm.{u_5} (E := α) (∑ i_1 : n, A i i_1 * x i_1) ≤ N), ∑ j : n, ‖A i j‖₊ ≤ N
inr₈ :
  let x : n → α := fun (j : n) ↦ unitOf (A i j);
  ∀ (hxn : ‖x‖₊ = 1) (hN : ∑ i_1 : n, ‖A i i_1‖₊ ≤ N), ∑ j : n, ‖A i j‖₊ ≤ N
⊢ ∑ j : n, ‖A i j‖₊ ≤ N

Tactic:
classical
  let x : n → α := fun j => unitOf (A i j)
  have hxn : ‖x‖₊ = 1 := by
    simp_rw [x, Pi.nnnorm_def, norm_unitOf, Finset.sup_const Finset.univ_nonempty]
  specialize hN x
  rw [hxn, mul_one, Pi.nnnorm_def, Finset.sup_le_iff] at hN
  replace hN := hN i (Finset.mem_univ _)
  dsimp [mulVec, dotProduct] at hN
  simp_rw [x, mul_unitOf, ← map_sum, nnnorm_algebraMap, ← NNReal.coe_sum, NNReal.nnnorm_eq,
    nnnorm_one, mul_one] at hN
  exact hN

Premises used: dotProduct, nnnorm_one, nnnorm_algebraMap, map_sum, NNReal.coe_sum, _private.0.Matrix.mul_unitOf, Pi.nnnorm_def, NNReal.nnnorm_eq, Finset.sup_le_iff, mul_one, Matrix.mulVec
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : NontriviallyNormedField α
inst_3 : NormedAlgebra ℝ α
A : Matrix m n α
⊢ ‖A‖ = norm (E := (n → α) →L[α] m → α) { toLinearMap := A.mulVecLin, cont := ⋯ }

Tactic:
congr_arg NNReal.toReal (linfty_opNNNorm_eq_opNNNorm A)

Premises used: Multiset.foldr, Finset.fold, Matrix.linfty_opNNNorm_eq_opNNNorm, setOf, NNReal.mk, NNReal, congr_arg, Finset.sup, NNReal.toReal, Multiset.fold
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : NontriviallyNormedField α
inst_3 : NormedAlgebra ℝ α
inst_4 : DecidableEq n
f : (n → α) →L[α] m → α
rw :
  nnnorm (E := (n → α) →L[α] m → α)
      {
        toLinearMap :=
          mulVecLin ((LinearMap.toMatrix' : (a : (n → α) →ₗ[α] m → α) → Matrix m n α) (↑f : (n → α) →ₗ[α] m → α)),
        cont := ⋯ : (n → α) →L[α] m → α } =
    ‖f‖₊
⊢ nnnorm (E := Matrix m n α)
      ((LinearMap.toMatrix' : (a : (n → α) →ₗ[α] m → α) → Matrix m n α) (↑f : (n → α) →ₗ[α] m → α) : Matrix m n α) =
    ‖f‖₊

Tactic:
rw [linfty_opNNNorm_eq_opNNNorm]

Premises used: Matrix.linfty_opNNNorm_eq_opNNNorm
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : NontriviallyNormedField α
inst_3 : NormedAlgebra ℝ α
inst_4 : DecidableEq n
f : (n → α) →L[α] m → α
⊢ nnnorm (E := (n → α) →L[α] m → α)
      {
        toLinearMap :=
          mulVecLin ((LinearMap.toMatrix' : (a : (n → α) →ₗ[α] m → α) → Matrix m n α) (↑f : (n → α) →ₗ[α] m → α)),
        cont := ⋯ : (n → α) →L[α] m → α } =
    ‖f‖₊

Tactic:
simp only [← toLin'_apply', toLin'_toMatrix']

Premises used: Matrix.toLin'_apply', Matrix.toLin'_toMatrix'
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : NontriviallyNormedField α
inst_3 : NormedAlgebra ℝ α
inst_4 : DecidableEq n
f : (n → α) →L[α] m → α
⊢ norm (E := Matrix m n α)
      ((LinearMap.toMatrix' : (a : (n → α) →ₗ[α] m → α) → Matrix m n α) (↑f : (n → α) →ₗ[α] m → α) : Matrix m n α) =
    ‖f‖

Tactic:
congr_arg NNReal.toReal (linfty_opNNNorm_toMatrix f)

Premises used: Multiset.foldr, Finset.fold, setOf, Matrix.linfty_opNNNorm_toMatrix, NNReal.mk, NNReal, congr_arg, Finset.sup, NNReal.toReal, Multiset.fold
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
R : Type u_1
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : SeminormedRing R
inst_3 : SeminormedAddCommGroup α
inst_4 : Module R α
inst_5 : IsBoundedSMul R α
⊢ IsBoundedSMul R (Matrix m n α)

Tactic:
letI := PiLp.seminormedAddCommGroupToPi 2 (fun _ : n ↦ α)
  letI := PiLp.isBoundedSMulSeminormedAddCommGroupToPi (R := R) 2 (fun _ : n ↦ α)
  PiLp.isBoundedSMulSeminormedAddCommGroupToPi 2 _

Premises used: PiLp.isBoundedSMulSeminormedAddCommGroupToPi, Matrix, setOf, OfNat.ofNat
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
R : Type u_1
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : SeminormedRing R
inst_3 : SeminormedAddCommGroup α
inst_4 : Module R α
inst_5 : NormSMulClass R α
⊢ NormSMulClass R (Matrix m n α)

Tactic:
letI := PiLp.seminormedAddCommGroupToPi 2 (fun _ : n ↦ α)
  letI := PiLp.normSMulClassSeminormedAddCommGroupToPi (R := R) 2 (fun _ : n ↦ α)
  PiLp.normSMulClassSeminormedAddCommGroupToPi 2 _

Premises used: Matrix, setOf, PiLp.normSMulClassSeminormedAddCommGroupToPi, OfNat.ofNat
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : SeminormedAddCommGroup α
A : Matrix m n α
change :
  nnnorm (E := WithLp 2 ((i : m) → WithLp 2 ((j : n) → α))) (toLp 2 fun (i : m) ↦ toLp 2 fun (j : n) ↦ A i j) =
    HPow.hPow (α := ℝ≥0) (∑ i : m, ∑ j : n, HPow.hPow (β := ℝ) ‖A i j‖₊ 2) (1 / 2)
⊢ ‖A‖₊ = HPow.hPow (α := ℝ≥0) (∑ i : m, ∑ j : n, HPow.hPow (β := ℝ) ‖A i j‖₊ 2) (1 / 2)

Tactic:
change ‖toLp 2 fun i => toLp 2 fun j => A i j‖₊ = _

Premises used: WithLp.toLp, OfNat.ofNat
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : SeminormedAddCommGroup α
A : Matrix m n α
simp_rw :
  (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0)
      (∑ x : m,
        HPow.hPow (α := ℝ≥0) (β := ℕ) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (∑ x_1 : n, HPow.hPow (β := ℕ) ‖A x x_1‖₊ 2))
          2) =
    HPow.hPow (α := ℝ≥0) (∑ i : m, ∑ j : n, HPow.hPow (β := ℝ) ‖A i j‖₊ 2) (1 / 2)
simp_rw₁ :
  (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (∑ x : m, ∑ x_1 : n, HPow.hPow (β := ℕ) ‖A x x_1‖₊ 2) =
    HPow.hPow (α := ℝ≥0) (∑ i : m, ∑ j : n, HPow.hPow (β := ℝ) ‖A i j‖₊ 2) (1 / 2)
simp_rw₂ :
  HPow.hPow (α := ℝ≥0) (∑ x : m, ∑ x_1 : n, HPow.hPow (β := ℕ) ‖A x x_1‖₊ 2) (1 / 2) =
    HPow.hPow (α := ℝ≥0) (∑ i : m, ∑ j : n, HPow.hPow (β := ℝ) ‖A i j‖₊ 2) (1 / 2)
⊢ nnnorm (E := WithLp 2 ((i : m) → WithLp 2 ((j : n) → α))) (toLp 2 fun (i : m) ↦ toLp 2 fun (j : n) ↦ A i j) =
    HPow.hPow (α := ℝ≥0) (∑ i : m, ∑ j : n, HPow.hPow (β := ℝ) ‖A i j‖₊ 2) (1 / 2)

Tactic:
simp_rw [PiLp.nnnorm_eq_of_L2, NNReal.sq_sqrt, NNReal.sqrt_eq_rpow, NNReal.rpow_two]

Premises used: NNReal.sqrt_eq_rpow, PiLp.nnnorm_eq_of_L2, NNReal.rpow_two, NNReal.sq_sqrt
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : SeminormedAddCommGroup α
A : Matrix m n α
⊢ (↑(HPow.hPow (α := ℝ≥0) (∑ i : m, ∑ j : n, HPow.hPow (β := ℝ) ‖A i j‖₊ 2) (1 / 2)) : ℝ) =
    HPow.hPow (α := ℝ) (∑ i : m, ∑ j : n, HPow.hPow (β := ℝ) ‖A i j‖ 2) (1 / 2)

Tactic:
simp [NNReal.coe_sum]

Premises used: NNReal.coe_sum
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst : Fintype m
inst_1 : Fintype n
inst_2 : SeminormedAddCommGroup α
inst_3 : SeminormedAddCommGroup β
A : Matrix m n α
f : α → β
hf : ∀ (a : α), ‖f a‖₊ = ‖a‖₊
simp_rw :
  HPow.hPow (α := ℝ≥0) (∑ i : m, ∑ j : n, HPow.hPow (β := ℝ) ‖A.map f i j‖₊ 2) (1 / 2) =
    HPow.hPow (α := ℝ≥0) (∑ i : m, ∑ j : n, HPow.hPow (β := ℝ) ‖A i j‖₊ 2) (1 / 2)
simp_rw₁ :
  HPow.hPow (α := ℝ≥0) (∑ x : m, ∑ x_1 : n, HPow.hPow (β := ℝ) ‖f (A x x_1)‖₊ 2) (1 / 2) =
    HPow.hPow (α := ℝ≥0) (∑ i : m, ∑ j : n, HPow.hPow (β := ℝ) ‖A i j‖₊ 2) (1 / 2)
⊢ ‖A.map f‖₊ = ‖A‖₊

Tactic:
simp_rw [frobenius_nnnorm_def, Matrix.map_apply, hf]

Premises used: Matrix.map_apply, Matrix.frobenius_nnnorm_def
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst : Fintype m
inst_1 : Fintype n
inst_2 : SeminormedAddCommGroup α
inst_3 : SeminormedAddCommGroup β
A : Matrix m n α
f : α → β
hf : ∀ (a : α), ‖f a‖ = ‖a‖
⊢ ‖A.map f‖ = ‖A‖

Tactic:
(congr_arg ((↑) : ℝ≥0 → ℝ) <| frobenius_nnnorm_map_eq A f fun a => Subtype.ext <| hf a :)

Premises used: Matrix.frobenius_nnnorm_map_eq, congr_arg, NNReal.toReal, Subtype.ext
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : SeminormedAddCommGroup α
A : Matrix m n α
rw :
  HPow.hPow (α := ℝ≥0) (∑ y : m, ∑ x : n, HPow.hPow (β := ℝ) ‖Aᵀ x y‖₊ 2) (1 / 2) =
    HPow.hPow (α := ℝ≥0) (∑ i : m, ∑ j : n, HPow.hPow (β := ℝ) ‖A i j‖₊ 2) (1 / 2)
⊢ ‖Aᵀ‖₊ = ‖A‖₊

Tactic:
rw [frobenius_nnnorm_def, frobenius_nnnorm_def, Finset.sum_comm]

Premises used: Matrix.frobenius_nnnorm_def, Finset.sum_comm
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : SeminormedAddCommGroup α
A : Matrix m n α
⊢ HPow.hPow (α := ℝ≥0) (∑ y : m, ∑ x : n, HPow.hPow (β := ℝ) ‖Aᵀ x y‖₊ 2) (1 / 2) =
    HPow.hPow (α := ℝ≥0) (∑ i : m, ∑ j : n, HPow.hPow (β := ℝ) ‖A i j‖₊ 2) (1 / 2)

Tactic:
simp_rw [Matrix.transpose_apply]

Premises used: Matrix.transpose_apply
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : SeminormedAddCommGroup α
A : Matrix m n α
⊢ ‖Aᵀ‖ = ‖A‖

Tactic:
congr_arg ((↑) : ℝ≥0 → ℝ) <| frobenius_nnnorm_transpose A

Premises used: congr_arg, Matrix.frobenius_nnnorm_transpose, NNReal.toReal
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : SeminormedAddCommGroup α
inst_3 : StarAddMonoid α
inst_4 : NormedStarGroup α
A : Matrix m n α
⊢ ‖Aᴴ‖₊ = ‖A‖₊

Tactic:
(frobenius_nnnorm_map_eq _ _ nnnorm_star).trans A.frobenius_nnnorm_transpose

Premises used: Matrix.frobenius_nnnorm_map_eq, nnnorm_star, setOf, Matrix.conjTranspose, Matrix.frobenius_nnnorm_transpose, Eq.trans
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : SeminormedAddCommGroup α
inst_3 : StarAddMonoid α
inst_4 : NormedStarGroup α
A : Matrix m n α
⊢ ‖Aᴴ‖ = ‖A‖

Tactic:
congr_arg ((↑) : ℝ≥0 → ℝ) <| frobenius_nnnorm_conjTranspose A

Premises used: congr_arg, NNReal.toReal, Matrix.frobenius_nnnorm_conjTranspose
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
ι : Type u_7
inst : Fintype l
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : Unique ι
inst_4 : SeminormedAddCommGroup α
inst_5 : SeminormedAddCommGroup β
inst_6 : StarAddMonoid α
inst_7 : NormedStarGroup α
⊢ NormedStarGroup (Matrix m m α)

Tactic:
⟨(le_of_eq <| frobenius_norm_conjTranspose ·)⟩

Premises used: NormedStarGroup.mk, Matrix.frobenius_norm_conjTranspose, le_of_eq
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
α : Type u_5
ι : Type u_7
inst : Fintype m
inst_1 : Unique ι
inst_2 : SeminormedAddCommGroup α
v : m → α
rw :
  HPow.hPow (α := ℝ) (∑ j : m, HPow.hPow (β := ℝ) ‖replicateRow ι v default j‖ 2) (1 / 2) =
    HPow.hPow (α := ℝ) (∑ i : m, HPow.hPow (β := ℕ) ‖ofLp (p := 2) (toLp 2 v) i‖ 2) (1 / 2)
⊢ ‖replicateRow ι v‖ = norm (E := WithLp 2 (m → α)) (toLp 2 v)

Tactic:
rw [frobenius_norm_def, Fintype.sum_unique, PiLp.norm_eq_of_L2, Real.sqrt_eq_rpow]

Premises used: Fintype.sum_unique, Matrix.frobenius_norm_def, PiLp.norm_eq_of_L2, Real.sqrt_eq_rpow
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
α : Type u_5
ι : Type u_7
inst : Fintype m
inst_1 : Unique ι
inst_2 : SeminormedAddCommGroup α
v : m → α
⊢ HPow.hPow (α := ℝ) (∑ j : m, HPow.hPow (β := ℝ) ‖replicateRow ι v default j‖ 2) (1 / 2) =
    HPow.hPow (α := ℝ) (∑ i : m, HPow.hPow (β := ℕ) ‖ofLp (p := 2) (toLp 2 v) i‖ 2) (1 / 2)

Tactic:
simp only [replicateRow_apply, Real.rpow_two]

Premises used: Real.rpow_two, Matrix.replicateRow_apply
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
α : Type u_5
ι : Type u_7
inst : Fintype m
inst_1 : Unique ι
inst_2 : SeminormedAddCommGroup α
v : m → α
⊢ ‖replicateRow ι v‖₊ = nnnorm (E := WithLp 2 (m → α)) (toLp 2 v)

Tactic:
Subtype.ext <| frobenius_norm_replicateRow v

Premises used: NNReal, Matrix.frobenius_norm_replicateRow, Subtype.ext
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
n : Type u_4
α : Type u_5
ι : Type u_7
inst : Fintype n
inst_1 : Unique ι
inst_2 : SeminormedAddCommGroup α
v : n → α
⊢ ‖replicateCol ι v‖ = norm (E := WithLp 2 (n → α)) (toLp 2 v)

Tactic:
simp [frobenius_norm_def, PiLp.norm_eq_of_L2, Real.sqrt_eq_rpow]

Premises used: Matrix.frobenius_norm_def, PiLp.norm_eq_of_L2, Real.sqrt_eq_rpow