awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
l : Type u_4
inst : RCLike 𝕜
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq n
inst_4 : Fintype l
inst_5 : DecidableEq l
A : Matrix m n 𝕜
B : Matrix n l 𝕜
this :
  norm (E := EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 m)
      (ContinuousLinearMap.comp (R₂ := 𝕜) (σ₁₂ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) (M₂ := EuclideanSpace 𝕜 n)
        ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix m n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)
          A)
        ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix n l 𝕜) → EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 n)
          B)) ≤
    norm (E := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)
        ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix m n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)
            A :
          EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m) *
      norm (E := EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 n)
        ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix n l 𝕜) → EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 n)
            B :
          EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 n)
x : EuclideanSpace 𝕜 l
⊢ Eq (α := EuclideanSpace 𝕜 m)
    ((((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix m l 𝕜) → EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 m)
              (A * B) :
            EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 m) :
          (a : EuclideanSpace 𝕜 l) → EuclideanSpace 𝕜 m)
        x :
      EuclideanSpace 𝕜 m)
    ((ContinuousLinearMap.comp (R₂ := 𝕜) (σ₁₂ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) (M₂ := EuclideanSpace 𝕜 n)
            ((toEuclideanLin ≪≫ₗ toContinuousLinearMap :
                (a : Matrix m n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)
              A)
            ((toEuclideanLin ≪≫ₗ toContinuousLinearMap :
                (a : Matrix n l 𝕜) → EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 n)
              B) :
          (a : EuclideanSpace 𝕜 l) → EuclideanSpace 𝕜 m)
        x :
      EuclideanSpace 𝕜 m)

Tactic:
congr(toLp 2 ($(Matrix.toLin'_mul A B) x))

Premises used: congrArg, WithLp.toLp, Matrix.toLin'_mul, id, OfNat.ofNat, WithLp.ofLp, DFunLike.coe
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
l : Type u_4
inst : RCLike 𝕜
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq n
inst_4 : Fintype l
inst_5 : DecidableEq l
A : Matrix m n 𝕜
B : Matrix n l 𝕜
this :
  norm (E := EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 m)
      (ContinuousLinearMap.comp (R₂ := 𝕜) (σ₁₂ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) (M₂ := EuclideanSpace 𝕜 n)
        ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix m n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)
          A)
        ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix n l 𝕜) → EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 n)
          B)) ≤
    norm (E := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)
        ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix m n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)
            A :
          EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m) *
      norm (E := EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 n)
        ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix n l 𝕜) → EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 n)
            B :
          EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 n)
x : EuclideanSpace 𝕜 l
⊢ Eq (α := EuclideanSpace 𝕜 m)
    ((((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix m l 𝕜) → EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 m)
              (A * B) :
            EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 m) :
          (a : EuclideanSpace 𝕜 l) → EuclideanSpace 𝕜 m)
        x :
      EuclideanSpace 𝕜 m)
    ((ContinuousLinearMap.comp (R₂ := 𝕜) (σ₁₂ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) (M₂ := EuclideanSpace 𝕜 n)
            ((toEuclideanLin ≪≫ₗ toContinuousLinearMap :
                (a : Matrix m n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)
              A)
            ((toEuclideanLin ≪≫ₗ toContinuousLinearMap :
                (a : Matrix n l 𝕜) → EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 n)
              B) :
          (a : EuclideanSpace 𝕜 l) → EuclideanSpace 𝕜 m)
        x :
      EuclideanSpace 𝕜 m)

Tactic:
exact congr(toLp 2 ($(Matrix.toLin'_mul A B) x))
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
l : Type u_4
inst : RCLike 𝕜
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq n
inst_4 : Fintype l
inst_5 : DecidableEq l
A : Matrix m n 𝕜
B : Matrix n l 𝕜
⊢ ‖A * B‖₊ ≤ ‖A‖₊ * ‖B‖₊

Tactic:
l2_opNorm_mul A B

Premises used: Matrix.l2_opNorm_mul
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
⊢ norm (E := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
      ((toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) A :
        EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) =
    ‖A‖

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Matrix.mulVec, Finset.sum, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n :=
  (toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v)
rw :
  norm (E := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
      ((toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v) :
        EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) =
    ‖v‖
⊢ ‖diagonal v‖ = ‖v‖

Tactic:
rw [← l2_opNorm_toEuclideanCLM]

Premises used: Matrix.l2_opNorm_toEuclideanCLM
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n :=
  (toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v)
⊢ norm (E := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
      ((toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v) :
        EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) =
    ‖v‖

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n :=
  (toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v)
refine_1 :
  norm (E := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
      ((toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v) :
        EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) ≤
    ‖v‖
refine_2 :
  ‖v‖ ≤
    norm (E := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
      ((toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v) :
        EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
⊢ norm (E := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
      ((toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v) :
        EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) =
    ‖v‖

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n :=
  (toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v)
⊢ norm (E := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
      ((toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v) :
        EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) ≤
    ‖v‖

Tactic:
T.opNorm_le_bound (norm_nonneg _) fun x ↦ ?_

Premises used: ContinuousLinearMap.opNorm_le_bound, norm_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n :=
  (toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v)
refine_1 :
  ∀ (x : EuclideanSpace 𝕜 n),
    norm (E := EuclideanSpace 𝕜 n) ((T : (a : EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n) x : EuclideanSpace 𝕜 n) ≤
      ‖v‖ * ‖x‖
⊢ norm (E := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
      ((toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v) :
        EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) ≤
    ‖v‖

Tactic:
refine T.opNorm_le_bound (norm_nonneg _) fun x ↦ ?_

Premises used: ContinuousLinearMap.opNorm_le_bound, norm_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n :=
  (toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v)
x : EuclideanSpace 𝕜 n
⊢ 0 ≤ norm (E := EuclideanSpace 𝕜 n) ((T : (a : EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n) x : EuclideanSpace 𝕜 n)

Tactic:
positivity
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n :=
  (toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v)
x : EuclideanSpace 𝕜 n
⊢ 0 ≤ ‖v‖ * ‖x‖

Tactic:
positivity
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n :=
  (toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v)
x : EuclideanSpace 𝕜 n
refine_1 :
  HPow.hPow (β := ℕ)
      (norm (E := EuclideanSpace 𝕜 n) ((T : (a : EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n) x : EuclideanSpace 𝕜 n)) 2 ≤
    HPow.hPow (β := ℕ) (‖v‖ * ‖x‖) 2
⊢ norm (E := EuclideanSpace 𝕜 n) ((T : (a : EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n) x : EuclideanSpace 𝕜 n) ≤
    ‖v‖ * ‖x‖

Tactic:
refine (sq_le_sq₀ (by positivity) (by positivity)).mp ?_

Premises used: sq_le_sq₀, Iff.mp
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n :=
  (toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v)
x : EuclideanSpace 𝕜 n
refine_1 : ∑ x_1 : n, HPow.hPow (β := ℕ) (‖v x_1‖ * ‖x.ofLp x_1‖) 2 ≤ HPow.hPow (β := ℕ) (‖v‖ * ‖x‖) 2
⊢ HPow.hPow (β := ℕ)
      (norm (E := EuclideanSpace 𝕜 n) ((T : (a : EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n) x : EuclideanSpace 𝕜 n)) 2 ≤
    HPow.hPow (β := ℕ) (‖v‖ * ‖x‖) 2

Tactic:
simp only [(T x).norm_sq_eq, ofLp_toEuclideanCLM, mulVec_diagonal, norm_mul, T]

Premises used: EuclideanSpace.norm_sq_eq, norm_mul, Matrix.ofLp_toEuclideanCLM, Matrix.mulVec_diagonal, DFunLike.coe
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n :=
  (toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v)
x : EuclideanSpace 𝕜 n
i : n
h : Membership.mem (γ := Finset n) Finset.univ i
grw :
  HPow.hPow (β := ℕ) ‖v i‖ 2 * HPow.hPow (β := ℕ) ‖x.ofLp i‖ 2 ≤
    HPow.hPow (β := ℕ) ‖v‖ 2 * HPow.hPow (β := ℕ) ‖x.ofLp i‖ 2
grw₁ grw₂ :
  HPow.hPow (β := ℕ) ‖v‖ 2 * HPow.hPow (β := ℕ) ‖x.ofLp i‖ 2 ≤
    HPow.hPow (β := ℕ) ‖v‖ 2 * HPow.hPow (β := ℕ) ‖x.ofLp i‖ 2
⊢ HPow.hPow (β := ℕ) (‖v i‖ * ‖x.ofLp i‖) 2 ≤ HPow.hPow (β := ℕ) ‖v‖ 2 * HPow.hPow (β := ℕ) ‖x.ofLp i‖ 2

Tactic:
grw [mul_pow, norm_le_pi_norm v i]

Premises used: norm_le_pi_norm, mul_pow
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n :=
  (toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v)
x : EuclideanSpace 𝕜 n
⊢ ∑ i : n, HPow.hPow (β := ℕ) ‖v‖ 2 * HPow.hPow (β := ℕ) ‖x.ofLp i‖ 2 = HPow.hPow (β := ℕ) (‖v‖ * ‖x‖) 2

Tactic:
simp [mul_pow, EuclideanSpace.norm_sq_eq x, Finset.mul_sum]

Premises used: Finset.mul_sum, EuclideanSpace.norm_sq_eq, mul_pow
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n :=
  (toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v)
x : EuclideanSpace 𝕜 n
calc : ∑ i : n, HPow.hPow (β := ℕ) ‖v‖ 2 * HPow.hPow (β := ℕ) ‖x.ofLp i‖ 2 = HPow.hPow (β := ℕ) (‖v‖ * ‖x‖) 2
⊢ ∑ x_1 : n, HPow.hPow (β := ℕ) (‖v x_1‖ * ‖x.ofLp x_1‖) 2 ≤ HPow.hPow (β := ℕ) (‖v‖ * ‖x‖) 2

Tactic:
calc _ ≤ _ := Finset.sum_le_sum fun i _ ↦ by grw [mul_pow, norm_le_pi_norm v i]
      _ = _ := by simp [mul_pow, EuclideanSpace.norm_sq_eq x, Finset.mul_sum]

Premises used: Finset.sum_le_sum
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n :=
  (toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v)
⊢ ‖v‖ ≤
    norm (E := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
      ((toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v) :
        EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)

Tactic:
(pi_norm_le_iff_of_nonneg (norm_nonneg T)).mpr fun i ↦ ?_

Premises used: Iff.mpr, pi_norm_le_iff_of_nonneg, norm_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n :=
  (toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v)
refine_2 : ∀ (i : n), ‖v i‖ ≤ ‖T‖
⊢ ‖v‖ ≤
    norm (E := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
      ((toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v) :
        EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)

Tactic:
refine (pi_norm_le_iff_of_nonneg (norm_nonneg T)).mpr fun i ↦ ?_

Premises used: Iff.mpr, pi_norm_le_iff_of_nonneg, norm_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n :=
  (toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v)
i : n
rw : ‖v i‖ = norm (E := EuclideanSpace 𝕜 n) (toLp 2 (diagonal v *ᵥ Pi.single (M := fun (a : n) ↦ 𝕜) i 1))
⊢ ‖v i‖ =
    norm (E := EuclideanSpace 𝕜 n)
      ((T : (a : EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n) (toLp 2 (Pi.single (M := fun (x : n) ↦ 𝕜) i 1)) :
        EuclideanSpace 𝕜 n)

Tactic:
rw [toEuclideanCLM_toLp (diagonal v) (Pi.single i (1 : 𝕜))]

Premises used: Matrix.toEuclideanCLM_toLp, Pi.single, OfNat.ofNat, Matrix.diagonal
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n :=
  (toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v)
i : n
⊢ ‖v i‖ = norm (E := EuclideanSpace 𝕜 n) (toLp 2 (diagonal v *ᵥ Pi.single (M := fun (a : n) ↦ 𝕜) i 1))

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n :=
  (toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v)
i : n
grw : ‖T‖ * norm (E := EuclideanSpace 𝕜 n) (toLp 2 (Pi.single (M := fun (x : n) ↦ 𝕜) i 1)) ≤ ‖T‖
⊢ norm (E := EuclideanSpace 𝕜 n)
      ((T : (a : EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n) (toLp 2 (Pi.single (M := fun (x : n) ↦ 𝕜) i 1)) :
        EuclideanSpace 𝕜 n) ≤
    ‖T‖

Tactic:
grw [T.le_opNorm]

Premises used: ContinuousLinearMap.le_opNorm
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n :=
  (toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v)
i : n
⊢ ‖T‖ * norm (E := EuclideanSpace 𝕜 n) (toLp 2 (Pi.single (M := fun (x : n) ↦ 𝕜) i 1)) ≤ ‖T‖

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n :=
  (toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v)
i : n
calc :
  ‖v i‖ =
    norm (E := EuclideanSpace 𝕜 n)
      ((T : (a : EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n) (toLp 2 (Pi.single (M := fun (x : n) ↦ 𝕜) i 1)) :
        EuclideanSpace 𝕜 n)
calc₁ :
  norm (E := EuclideanSpace 𝕜 n)
      ((T : (a : EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n) (toLp 2 (Pi.single (M := fun (x : n) ↦ 𝕜) i 1)) :
        EuclideanSpace 𝕜 n) ≤
    ‖T‖
⊢ ‖v i‖ ≤ ‖T‖

Tactic:
calc _ = ‖T (toLp 2 (Pi.single i (1 : 𝕜)))‖ := by
          rw [toEuclideanCLM_toLp (diagonal v) (Pi.single i (1 : 𝕜))]
          simp
      _ ≤ _ := by grw [T.le_opNorm]; simp

Premises used: WithLp.toLp, Pi.single, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
v : n → 𝕜
⊢ ‖diagonal v‖₊ = ‖v‖₊

Tactic:
Subtype.ext <| l2_opNorm_diagonal (n := n) (𝕜 := 𝕜) v

Premises used: Matrix.l2_opNorm_diagonal, NNReal, Subtype.ext
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
l : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq n
inst_4 : Fintype l
inst_5 : DecidableEq l
r : 𝕜
x : Matrix m n 𝕜
rw :
  ‖HSMul.hSMul (β := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m) r
        ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix m n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)
            x :
          EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)‖ ≤
    ‖r‖ * ‖x‖
⊢ ‖r • x‖ ≤ ‖r‖ * ‖x‖

Tactic:
rw [l2_opNorm_def, map_smul]

Premises used: Matrix.l2_opNorm_def, map_smul
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
l : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq n
inst_4 : Fintype l
inst_5 : DecidableEq l
r : 𝕜
x : Matrix m n 𝕜
⊢ ‖HSMul.hSMul (β := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m) r
        ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix m n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)
            x :
          EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)‖ ≤
    ‖r‖ * ‖x‖

Tactic:
norm_smul_le r ((toEuclideanLin (𝕜 := 𝕜) (m := m) (n := n)).trans toContinuousLinearMap x)

Premises used: norm_smul_le, Matrix.toEuclideanLin, LinearEquiv.trans, DFunLike.coe, LinearMap.toContinuousLinearMap
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
l : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq n
inst_4 : Fintype l
inst_5 : DecidableEq l
r : 𝕜
x : Matrix m n 𝕜
⊢ ‖HSMul.hSMul (β := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m) r
        ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix m n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)
            x :
          EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)‖ ≤
    ‖r‖ * ‖x‖

Tactic:
exact norm_smul_le r ((toEuclideanLin (𝕜 := 𝕜) (m := m) (n := n)).trans toContinuousLinearMap x)

Premises used: norm_smul_le, Matrix.toEuclideanLin, LinearEquiv.trans, DFunLike.coe, LinearMap.toContinuousLinearMap
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
⊢ ‖A‖ =
    norm (E := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
      ((toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) A :
        EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Matrix.mulVec, Finset.sum, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
⊢ ‖A‖₊ =
    nnnorm (E := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
      ((toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) A :
        EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Matrix.mulVec, Finset.sum, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x y : A
⊢ star (y * star x) = x * star y

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
⊢ 0 ≤ √‖x * star x‖

Tactic:
positivity
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
rw : HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) (√‖x * star x‖) 2
⊢ ‖x‖ = √‖x * star x‖

Tactic:
rw [← sq_eq_sq₀ (norm_nonneg _) (by positivity)]

Premises used: sq_eq_sq₀, norm_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) (√‖x * star x‖) 2

Tactic:
simpa [sq] using Eq.symm <| CStarRing.norm_self_mul_star

Premises used: sq, CStarRing.norm_self_mul_star, Eq.symm
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x y : A
⊢ ⟪x, y⟫_A = y * star x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ ‖x‖ = √‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 = ‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖

Tactic:
simp [prod_norm]

Premises used: WithCStarModule.prod_norm
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ 0 ≤ ‖x.1‖ + ‖x.2‖

Tactic:
positivity