theorem ENNReal.toReal_lt_toReal_if (p : ENNReal) (q : ENNReal) (hp : p ≠ ⊤) (hq : q ≠ ⊤) (h : p < q) : p.toReal < q.toReal

theorem ENNReal.ge_one_ne_zero (p : ENNReal) [Fact (1 ≤ p)] : p ≠ 0

theorem ENNReal.ge_one_toReal_ne_zero (p : ENNReal) [Fact (1 ≤ p)] (hp : p ≠ ⊤) : p.toReal ≠ 0

theorem Finset.single_le_row {α : Type u_5} {m : Type u_7} {n : Type u_8} [Fintype n] [OrderedAddCommMonoid α] (M : m → n → α) (h : ∀ (i : m) (j : n), 0 ≤ M i j) (i : m) (j : n) : M i j ≤ ∑ k : n, M i k

theorem Finset.row_le_sum {α : Type u_5} {m : Type u_7} {n : Type u_8} [Fintype m] [Fintype n] [OrderedAddCommMonoid α] (M : m → n → α) (h : ∀ (i : m) (j : n), 0 ≤ M i j) (i : m) : ∑ j : n, M i j ≤ ∑ k : m, ∑ l : n, M k l

theorem Finset.single_le_sum' {α : Type u_5} {m : Type u_7} {n : Type u_8} [Fintype m] [Fintype n] [OrderedAddCommMonoid α] (M : m → n → α) (h : ∀ (i : m) (j : n), 0 ≤ M i j) (i : m) (j : n) : M i j ≤ ∑ k : m, ∑ l : n, M k l

theorem Finset.sum_sum_le_sum_sum {α : Type u_5} {m : Type u_7} {n : Type u_8} [Fintype m] [Fintype n] [OrderedAddCommMonoid α] (f : m → n → α) (g : m → n → α) (h : ∀ (i : m) (j : n), f i j ≤ g i j) : ∑ i : m, ∑ j : n, f i j ≤ ∑ i : m, ∑ j : n, g i j

theorem Finset.sum_sum_nonneg {α : Type u_5} {m : Type u_7} {n : Type u_8} [Fintype m] [Fintype n] [OrderedAddCommMonoid α] (f : m → n → α) (h : ∀ (i : m) (j : n), 0 ≤ f i j) : 0 ≤ ∑ i : m, ∑ j : n, f i j

@[reducible, inline]

abbrev Matrix.MatrixP (m : Type u_10) (n : Type u_11) (α : Type u_12) (_p : ENNReal) : Type (max u_10 u_11 u_12)

synonym for matrix with lp norm

Equations

• Matrix.MatrixP m n α _p = Matrix m n α

def Matrix.LpNorm {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} [RCLike 𝕂] [Fintype m] [Fintype n] (p : ENNReal) (M : Matrix m n 𝕂) : ℝ

a function of lpnorm, of which LpNorm p M = ‖M‖ for p

Equations

• Matrix.LpNorm p M = if p = ⊤ then ⨆ (i : m), ⨆ (j : n), ‖M i j‖ else (∑ i : m, ∑ j : n, ‖M i j‖ ^ p.toReal) ^ (1 / p.toReal)

def Matrix.LpNNNorm {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} [RCLike 𝕂] [Fintype m] [Fintype n] (p : ENNReal) (M : Matrix m n 𝕂) : ℝ

a function of lpnorm, of which LpNorm p M = ‖M‖₊ for p

Equations

• Matrix.LpNNNorm p M = if p = ⊤ then ⨆ (i : m), ⨆ (j : n), ↑‖M i j‖₊ else ↑(∑ i : m, ∑ j : n, ‖M i j‖₊ ^ p.toReal) ^ (1 / p.toReal)

def Matrix.lpMatrixSeminormedAddCommGroup {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} (p : ENNReal) [Fintype m] [Fintype n] [Fact (1 ≤ p)] [SeminormedAddCommGroup 𝕂] : SeminormedAddCommGroup (Matrix.MatrixP m n 𝕂 p)

Seminormed group instance (using lp norm) for matrices over a seminormed group. Not declared as an instance because there are several natural choices for defining the norm of a matrix.

Equations

• Matrix.lpMatrixSeminormedAddCommGroup p = inferInstanceAs (SeminormedAddCommGroup (PiLp p fun (_i : m) => PiLp p fun (_j : n) => 𝕂))

def Matrix.lpMatrixNormedAddCommGroup {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} (p : ENNReal) [Fintype m] [Fintype n] [Fact (1 ≤ p)] [NormedAddCommGroup 𝕂] : NormedAddCommGroup (Matrix.MatrixP m n 𝕂 p)

Normed group instance (using lp norm) for matrices over a normed group. Not declared as an instance because there are several natural choices for defining the norm of a matrix.

Equations

• Matrix.lpMatrixNormedAddCommGroup p = inferInstanceAs (NormedAddCommGroup (PiLp p fun (_i : m) => PiLp p fun (_j : n) => 𝕂))

def Matrix.lpMatrixNormedSpace {𝕂 : Type u_1} {R : Type u_6} {m : Type u_7} {n : Type u_8} (p : ENNReal) [Fintype m] [Fintype n] [Fact (1 ≤ p)] [NormedField R] [SeminormedAddCommGroup 𝕂] [NormedSpace R 𝕂] : NormedSpace R (Matrix.MatrixP m n 𝕂 p)

Normed space instance (using lp norm) for matrices over a normed space. Not declared as an instance because there are several natural choices for defining the norm of a matrix.

Equations

• Matrix.lpMatrixNormedSpace p = inferInstance

@[simp]

theorem Matrix.lp_nnnorm_def {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} (p : ENNReal) [RCLike 𝕂] [Fintype m] [Fintype n] [Fact (1 ≤ p)] (M : Matrix.MatrixP m n 𝕂 p) (hp : p ≠ ⊤) : ‖M‖₊ = (∑ i : m, ∑ j : n, ‖M i j‖₊ ^ p.toReal) ^ (1 / p.toReal)

@[simp]

theorem Matrix.lp_norm_eq_ciSup {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} (p : ENNReal) [RCLike 𝕂] [Fintype m] [Fintype n] [Fact (1 ≤ p)] (M : Matrix.MatrixP m n 𝕂 p) (hp : p = ⊤) : ‖M‖ = ⨆ (i : m), ⨆ (j : n), ‖M i j‖

@[simp]

theorem Matrix.lpnorm_eq_ciSup {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} (p : ENNReal) [RCLike 𝕂] [Fintype m] [Fintype n] (M : Matrix m n 𝕂) (hp : p = ⊤) : Matrix.LpNorm p M = ⨆ (i : m), ⨆ (j : n), ‖M i j‖

@[simp]

theorem Matrix.lp_norm_def {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} (p : ENNReal) [RCLike 𝕂] [Fintype m] [Fintype n] [Fact (1 ≤ p)] (M : Matrix.MatrixP m n 𝕂 p) (hp : p ≠ ⊤) : ‖M‖ = (∑ i : m, ∑ j : n, ‖M i j‖ ^ p.toReal) ^ (1 / p.toReal)

@[simp]

theorem Matrix.lpnorm_def {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} (p : ENNReal) [RCLike 𝕂] [Fintype m] [Fintype n] (M : Matrix m n 𝕂) (hp : p ≠ ⊤) : Matrix.LpNorm p M = (∑ i : m, ∑ j : n, ‖M i j‖ ^ p.toReal) ^ (1 / p.toReal)

@[simp]

theorem Matrix.lp_nnnorm_eq_ciSup {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} (p : ENNReal) [RCLike 𝕂] [Fintype m] [Fintype n] [Fact (1 ≤ p)] (M : Matrix.MatrixP m n 𝕂 p) (hp : p = ⊤) : ‖M‖₊ = ⨆ (i : m), ⨆ (j : n), ‖M i j‖₊

theorem Matrix.lp_norm_eq_lpnorm {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} (p : ENNReal) [RCLike 𝕂] [Fintype m] [Fintype n] [Fact (1 ≤ p)] (M : Matrix m n 𝕂) : ‖M‖ = Matrix.LpNorm p M

theorem Matrix.lpnorm_triangle {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} (p : ENNReal) [RCLike 𝕂] [Fintype m] [Fintype n] [Fact (1 ≤ p)] (M : Matrix m n 𝕂) (N : Matrix m n 𝕂) : Matrix.LpNorm p (M + N) ≤ Matrix.LpNorm p M + Matrix.LpNorm p N

theorem Matrix.lpnorm_continuous_at_m {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} (p : ENNReal) [RCLike 𝕂] [Fintype m] [Fintype n] [Fact (1 ≤ p)] : Continuous (Matrix.LpNorm p)

theorem Matrix.lpnorm_tendsto_maxnorm {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} (p : ENNReal) [RCLike 𝕂] [Fintype m] [Fintype n] [Fact (1 ≤ p)] (h : p = ⊤) (M : Matrix m n 𝕂) : (∑ i : m, ∑ j : n, ‖M i j‖ ^ p.toReal) ^ (1 / p.toReal) = ⨆ (i : m), ⨆ (j : n), ‖M i j‖

theorem Matrix.le_iSup {m : Type u_7} {n : Type u_8} [Fintype m] (f : m → n → ℝ) (i : m) : f i ≤ ⨆ (i : m), f i

theorem Matrix.le_iSup' {m : Type u_7} {n : Type u_8} [Fintype n] (f : m → n → ℝ) (j : n) : (fun (x : m) => f x j) ≤ ⨆ (j : n), fun (x : m) => f x j

theorem Matrix.le_iSup_iSup {m : Type u_7} {n : Type u_8} [Fintype m] [Fintype n] (f : m → n → ℝ) (i : m) (j : n) : f i j ≤ ⨆ (i : m), ⨆ (j : n), f i j

theorem Matrix.le_iSup_iSup' {m : Type u_7} {n : Type u_8} [Fintype m] [Fintype n] (f : m → n → ℝ) (i : m) (j : n) : f i j ≤ ⨆ (j : n), ⨆ (i : m), f i j

theorem Matrix.iSup_iSup_nonneg {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} [RCLike 𝕂] (M : Matrix m n 𝕂) : 0 ≤ ⨆ (i : m), ⨆ (j : n), ‖M i j‖

theorem Matrix.elem_le_iSup_iSup {m : Type u_7} {n : Type u_8} [Fintype m] [Fintype n] (f : m → n → ℝ) (i : m) (j : n) : f i j ≤ ⨆ (i : m), ⨆ (j : n), f i j

theorem Matrix.elem_le_iSup_iSup' {m : Type u_7} {n : Type u_8} [Fintype m] [Fintype n] (f : m → n → ℝ) (i : m) (j : n) : f i j ≤ ⨆ (j : n), ⨆ (i : m), f i j

theorem Matrix.iSup_comm' {m : Type u_7} {n : Type u_8} [Fintype m] [Fintype n] (f : m → n → ℝ) (h : ∀ (i : m) (j : n), 0 ≤ f i j) : ⨆ (i : m), ⨆ (j : n), f i j = ⨆ (j : n), ⨆ (i : m), f i j

theorem Matrix.lpnorm_eq0_iff {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} (p : ENNReal) [RCLike 𝕂] [Fintype m] [Fintype n] [Fact (1 ≤ p)] (M : Matrix m n 𝕂) : Matrix.LpNorm p M = 0 ↔ M = 0

theorem Matrix.lpnorm_nonneg {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} (p : ENNReal) [RCLike 𝕂] [Fintype m] [Fintype n] [Fact (1 ≤ p)] (M : Matrix m n 𝕂) : 0 ≤ Matrix.LpNorm p M

theorem Matrix.lpnorm_rpow_nonneg {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} (p : ENNReal) [RCLike 𝕂] [Fintype m] [Fintype n] (M : Matrix m n 𝕂) : 0 ≤ ∑ i : m, ∑ j : n, ‖M i j‖ ^ p.toReal

theorem Matrix.lpnorm_rpow_ne0 {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} (p : ENNReal) [RCLike 𝕂] [Fintype m] [Fintype n] [Fact (1 ≤ p)] (M : Matrix m n 𝕂) (h : Matrix.LpNorm p M ≠ 0) (h' : p ≠ ⊤) : ∑ i : m, ∑ j : n, ‖M i j‖ ^ p.toReal ≠ 0

theorem Matrix.lpnorm_rpow_pos {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} (p : ENNReal) [RCLike 𝕂] [Fintype m] [Fintype n] [Fact (1 ≤ p)] (M : Matrix m n 𝕂) (h : Matrix.LpNorm p M ≠ 0) (h' : p ≠ ⊤) : 0 < ∑ i : m, ∑ j : n, ‖M i j‖ ^ p.toReal

theorem Matrix.lpnorm_p_one_nonneg {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} [RCLike 𝕂] [Fintype m] [Fintype n] (M : Matrix m n 𝕂) : 0 ≤ ∑ i : m, ∑ j : n, ‖M i j‖

theorem Matrix.lpnorm_p_one_ne0 {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} [RCLike 𝕂] [Fintype m] [Fintype n] (M : Matrix m n 𝕂) (h : M ≠ 0) : ∑ i : m, ∑ j : n, ‖M i j‖ ≠ 0

theorem Matrix.lpnorm_p_one_pos {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} [RCLike 𝕂] [Fintype m] [Fintype n] (M : Matrix m n 𝕂) (h : M ≠ 0) : 0 < ∑ i : m, ∑ j : n, ‖M i j‖

theorem Matrix.norm_rpow_rpow_inv {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} (p : ENNReal) [RCLike 𝕂] [Fact (1 ≤ p)] (M : Matrix m n 𝕂) (i : m) (j : n) (h : ¬p = ⊤) : ‖M i j‖ = (‖M i j‖ ^ p.toReal) ^ p.toReal⁻¹

theorem Matrix.lpnorm_elem_le_norm {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} (p : ENNReal) [RCLike 𝕂] [Fintype m] [Fintype n] [Fact (1 ≤ p)] (M : Matrix m n 𝕂) (i : m) (j : n) : ‖M i j‖ ≤ Matrix.LpNorm p M

theorem Matrix.lpnorm_elem_div_norm {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} (p : ENNReal) [RCLike 𝕂] [Fintype m] [Fintype n] [Fact (1 ≤ p)] (M : Matrix m n 𝕂) (i : m) (j : n) : 0 ≤ ‖M i j‖ / Matrix.LpNorm p M ∧ ‖M i j‖ / Matrix.LpNorm p M ≤ 1

theorem Matrix.lpnorm_antimono {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} [RCLike 𝕂] [Fintype m] [Fintype n] (M : Matrix m n 𝕂) (p₁ : ENNReal) (p₂ : ENNReal) [Fact (1 ≤ p₁)] [Fact (1 ≤ p₂)] (h₁ : p₁ ≠ ⊤) (h₂ : p₂ ≠ ⊤) (ple : p₁ ≤ p₂) : Matrix.LpNorm p₂ M ≤ Matrix.LpNorm p₁ M

theorem Matrix.lpnorm_antimono' {m : Type u_7} [Fintype m] (p₁ : ℝ) (p₂ : ℝ) (hp₁ : 1 ≤ p₁) (hp₂ : 1 ≤ p₂) (ple : p₁ ≤ p₂) (f : m → ℝ) (hf : ∀ (i : m), 0 ≤ f i) : (∑ i : m, f i ^ p₂) ^ p₂⁻¹ ≤ (∑ i : m, f i ^ p₁) ^ p₁⁻¹

@[simp]

theorem Matrix.lpnorm_transpose {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} (p : ENNReal) [RCLike 𝕂] [Fintype m] [Fintype n] [Fact (1 ≤ p)] (M : Matrix.MatrixP m n 𝕂 p) : ‖Matrix.transpose M‖ = ‖M‖

theorem Matrix.lpnorm_diag {𝕂 : Type u_1} {m : Type u_7} (p : ENNReal) [RCLike 𝕂] [Fintype m] [Fact (1 ≤ p)] [DecidableEq m] (d : m → 𝕂) (h : p ≠ ⊤) : Matrix.LpNorm p (Matrix.diagonal d) = (∑ i : m, ‖d i‖ ^ p.toReal) ^ (1 / p.toReal)

@[simp]

theorem Matrix.lpnorm_conjugate {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} (p : ENNReal) [RCLike 𝕂] [Fintype m] [Fintype n] [Fact (1 ≤ p)] (M : Matrix.MatrixP m n 𝕂 p) : ‖M^*‖ = ‖M‖

@[simp]

theorem Matrix.lpnorm_conjTranspose {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} (p : ENNReal) [RCLike 𝕂] [Fintype m] [Fintype n] [Fact (1 ≤ p)] [DecidableEq m] [DecidableEq n] (M : Matrix.MatrixP m n 𝕂 p) : ‖Matrix.conjTranspose M‖ = ‖M‖

theorem Matrix.lpnorm_continuous_at_p {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} [RCLike 𝕂] [Fintype m] [Fintype n] (A : Matrix m n 𝕂) : ContinuousOn (fun (p : ENNReal) => Matrix.LpNorm p A) {p : ENNReal | 1 ≤ p ∧ p ≠ ⊤}

theorem Matrix.lpnorm_mul_le {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} {l : Type u_9} (p : ENNReal) [RCLike 𝕂] [Fintype m] [Fintype n] [Fintype l] [Fact (1 ≤ p)] (A : Matrix m n 𝕂) (B : Matrix n l 𝕂) (ple2 : p ≤ 2) (h : p ≠ ⊤) : Matrix.LpNorm p (A * B) ≤ Matrix.LpNorm p A * Matrix.LpNorm p B

theorem Matrix.lpnorm_mul_le_lpnorm_pq {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} {l : Type u_9} [RCLike 𝕂] [Fintype m] [Fintype n] [Fintype l] (A : Matrix m n 𝕂) (B : Matrix n l 𝕂) (p : ENNReal) (q : ENNReal) [Fact (1 ≤ p)] [Fact (1 ≤ q)] (pge2 : 2 ≤ p) (h : p.toReal.IsConjExponent q.toReal) (hp : p ≠ ⊤) (hq : q ≠ ⊤) : Matrix.LpNorm p (A * B) ≤ Matrix.LpNorm p A * Matrix.LpNorm q B

theorem Matrix.lpnorm_mul_le_lpnorm_qp {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} {l : Type u_9} [RCLike 𝕂] [Fintype m] [Fintype n] [Fintype l] (A : Matrix m n 𝕂) (B : Matrix n l 𝕂) (p : ENNReal) (q : ENNReal) [Fact (1 ≤ p)] [Fact (1 ≤ q)] (pge2 : 2 ≤ p) (h : q.toReal.IsConjExponent p.toReal) (hp : p ≠ ⊤) (hq : q ≠ ⊤) : Matrix.LpNorm p (A * B) ≤ Matrix.LpNorm q A * Matrix.LpNorm p B

theorem Matrix.lpnorm_hoelder {𝕂 : Type u_1} {m : Type u_7} [RCLike 𝕂] [Fintype m] (p : ENNReal) (q : ENNReal) [Fact (1 ≤ p)] [Fact (1 ≤ q)] (h : q.toReal.IsConjExponent p.toReal) (M : Matrix Unit m 𝕂) (N : Matrix m Unit 𝕂) (hp : p ≠ ⊤) (hq : q ≠ ⊤) : Matrix.LpNorm 1 (M * N) ≤ Matrix.LpNorm p M * Matrix.LpNorm q N

theorem Matrix.lpnorm_cauchy {𝕂 : Type u_1} {m : Type u_7} [RCLike 𝕂] [Fintype m] (M : Matrix Unit m 𝕂) (N : Matrix m Unit 𝕂) : ‖(M * N).trace‖ ≤ Matrix.LpNorm 2 M * Matrix.LpNorm 2 N

@[simp]

theorem Matrix.trace_eq_l2norm {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} [RCLike 𝕂] [Fintype m] [Fintype n] (M : Matrix m n 𝕂) : (M.conjTranspose * M).trace = ↑(Matrix.LpNorm 2 M ^ 2)

@[simp]

theorem Matrix.trace_eq_l2norm' {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} [RCLike 𝕂] [Fintype m] [Fintype n] (M : Matrix m n 𝕂) : (M * M.conjTranspose).trace = ↑(Matrix.LpNorm 2 M ^ 2)

@[simp]

theorem Matrix.left_unitary_l2norm_preserve {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} [RCLike 𝕂] [Fintype m] [Fintype n] [PartialOrder 𝕂] [StarOrderedRing 𝕂] [DecidableEq m] (U : Matrix m m 𝕂) (h : U.IsUnitary) (N : Matrix m n 𝕂) : Matrix.LpNorm 2 (U * N) = Matrix.LpNorm 2 N

@[simp]

theorem Matrix.right_unitary_l2norm_preserve {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} [RCLike 𝕂] [Fintype m] [Fintype n] [PartialOrder 𝕂] [StarOrderedRing 𝕂] [DecidableEq n] (U : Matrix n n 𝕂) (h : U.IsUnitary) (N : Matrix m n 𝕂) : Matrix.LpNorm 2 (N * U) = Matrix.LpNorm 2 N

@[simp]

theorem Matrix.l2norm_unitary {𝕂 : Type u_1} {m : Type u_7} [RCLike 𝕂] [Fintype m] [DecidableEq m] (U : Matrix m m 𝕂) (h : U.IsUnitary) : Matrix.LpNorm 2 U = ↑(Fintype.card m) ^ (1 / 2)

theorem Matrix.lpnorm_unit_default_eq1 {𝕂 : Type u_1} {n : Type u_8} (p : ENNReal) [RCLike 𝕂] [Fintype n] [Fact (1 ≤ p)] [Inhabited n] [DecidableEq n] (v : Matrix n Unit 𝕂) : (v = fun (i : n) (x : Unit) => if i = default then 1 else 0) → Matrix.LpNorm p v = 1

theorem Matrix.unit_nonempty {𝕂 : Type u_1} {n : Type u_8} (p : ENNReal) [RCLike 𝕂] [Fintype n] [Fact (1 ≤ p)] [Inhabited n] [DecidableEq n] : {v : Matrix n Unit 𝕂 | Matrix.LpNorm p v = 1}.Nonempty

theorem Matrix.unit_bdd {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} (p : ENNReal) [RCLike 𝕂] [Fintype m] [Fintype n] [Fact (1 ≤ p)] : Bornology.IsBounded {v : Matrix m n 𝕂 | Matrix.LpNorm p v = 1}

theorem Matrix.unit_closed {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} (p : ENNReal) [RCLike 𝕂] [Fintype m] [Fintype n] [Fact (1 ≤ p)] : IsClosed {v : Matrix m n 𝕂 | Matrix.LpNorm p v = 1}

theorem Matrix.unit_compact {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} (p : ENNReal) [RCLike 𝕂] [Fintype m] [Fintype n] [Fact (1 ≤ p)] : IsCompact {v : Matrix m n 𝕂 | Matrix.LpNorm p v = 1}

theorem Matrix.div_norm_self_norm_unit {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} (p : ENNReal) [RCLike 𝕂] [Fintype m] [Fintype n] [Fact (1 ≤ p)] (M : Matrix m n 𝕂) (hM : M ≠ 0) : Matrix.LpNorm p ((1 / Matrix.LpNorm p M) • M) = 1

theorem Matrix.lpnorm_smul {𝕂 : Type u_1} {R : Type u_6} {m : Type u_7} {n : Type u_8} (p : ENNReal) [RCLike 𝕂] [Fintype m] [Fintype n] [Fact (1 ≤ p)] (M : Matrix m n 𝕂) [NormedDivisionRing R] [MulActionWithZero R 𝕂] [BoundedSMul R 𝕂] (r : R) : Matrix.LpNorm p (r • M) = ‖r‖ * Matrix.LpNorm p M

def Matrix.IpqNorm {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} [RCLike 𝕂] [Fintype m] [Fintype n] (p : ENNReal) (q : ENNReal) (M : Matrix m n 𝕂) : ℝ

Equations

• Matrix.IpqNorm p q M = sSup ((fun (v : Matrix n Unit 𝕂) => Matrix.LpNorm q (M * v)) '' {v : Matrix n Unit 𝕂 | Matrix.LpNorm p v = 1})

theorem Matrix.range_on_unit_eq_range_div {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} (p : ENNReal) (q : ENNReal) [RCLike 𝕂] [Fintype m] [Fintype n] [Fact (1 ≤ p)] [Fact (1 ≤ q)] (M : Matrix m n 𝕂) : (fun (v : Matrix n Unit 𝕂) => Matrix.LpNorm q (M * v)) '' {v : Matrix n Unit 𝕂 | Matrix.LpNorm p v = 1} ∪ {0} = Set.range fun (v : Matrix n Unit 𝕂) => Matrix.LpNorm q (M * v) / Matrix.LpNorm p v

theorem Matrix.range_on_unit_eq_range_div' {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} (p : ENNReal) (q : ENNReal) [RCLike 𝕂] [Fintype m] [Fintype n] [Fact (1 ≤ p)] [Fact (1 ≤ q)] (M : Matrix m n 𝕂) : (fun (v : Matrix n Unit 𝕂) => Matrix.LpNorm q (M * v) / Matrix.LpNorm p v * Matrix.LpNorm p v) '' {v : Matrix n Unit 𝕂 | Matrix.LpNorm p v = 1} ∪ {0} = Set.range fun (v : Matrix n Unit 𝕂) => Matrix.LpNorm q (M * v) / Matrix.LpNorm p v

theorem Matrix.sup_on_unit_eq_sup_div {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} (p : ENNReal) (q : ENNReal) [RCLike 𝕂] [Fintype m] [Fintype n] [Fact (1 ≤ p)] [Fact (1 ≤ q)] (M : Matrix m n 𝕂) [DecidableEq n] [Inhabited n] : sSup ((fun (v : Matrix n Unit 𝕂) => Matrix.LpNorm q (M * v)) '' {v : Matrix n Unit 𝕂 | Matrix.LpNorm p v = 1}) = ⨆ (v : Matrix n Unit 𝕂), Matrix.LpNorm q (M * v) / Matrix.LpNorm p v

theorem Matrix.ipqnorm_def {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} (p : ENNReal) (q : ENNReal) [RCLike 𝕂] [Fintype m] [Fintype n] [Fact (1 ≤ p)] [Fact (1 ≤ q)] (M : Matrix m n 𝕂) [DecidableEq n] [Inhabited n] : Matrix.IpqNorm p q M = ⨆ (v : Matrix n Unit 𝕂), Matrix.LpNorm q (M * v) / Matrix.LpNorm p v

theorem Matrix.ipqnorm_nonneg {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} (p : ENNReal) (q : ENNReal) [RCLike 𝕂] [Fintype m] [Fintype n] [Fact (1 ≤ q)] (M : Matrix m n 𝕂) : 0 ≤ Matrix.IpqNorm p q M

theorem Matrix.ipqnorm_bddabove {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} (p : ENNReal) (q : ENNReal) [RCLike 𝕂] [Fintype m] [Fintype n] [Fact (1 ≤ p)] [Fact (1 ≤ q)] (M : Matrix m n 𝕂) : BddAbove ((fun (v : Matrix n Unit 𝕂) => Matrix.LpNorm q (M * v)) '' {v : Matrix n Unit 𝕂 | Matrix.LpNorm p v = 1})

theorem Matrix.ipqnorm_bddabove' {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} (p : ENNReal) (q : ENNReal) [RCLike 𝕂] [Fintype m] [Fintype n] [Fact (1 ≤ p)] [Fact (1 ≤ q)] (M : Matrix m n 𝕂) : BddAbove (Set.range fun (v : Matrix n Unit 𝕂) => Matrix.LpNorm q (M * v) / Matrix.LpNorm p v)

theorem Matrix.lqnorm_le_ipq_lp {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} (p : ENNReal) (q : ENNReal) [RCLike 𝕂] [Fintype m] [Fintype n] [Fact (1 ≤ p)] [Fact (1 ≤ q)] (M : Matrix m n 𝕂) [DecidableEq n] [Inhabited n] (v : Matrix n Unit 𝕂) : Matrix.LpNorm q (M * v) ≤ Matrix.IpqNorm p q M * Matrix.LpNorm p v

theorem Matrix.lpnorm_le_ipp_lp {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} (p : ENNReal) [RCLike 𝕂] [Fintype m] [Fintype n] [Fact (1 ≤ p)] (M : Matrix m n 𝕂) [DecidableEq n] [Inhabited n] (v : Matrix n Unit 𝕂) : Matrix.LpNorm p (M * v) ≤ Matrix.IpqNorm p p M * Matrix.LpNorm p v

theorem Matrix.lpnorm_le_ipq_lp {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} (p : ENNReal) [RCLike 𝕂] [Fintype m] [Fintype n] [Fact (1 ≤ p)] (M : Matrix m n 𝕂) [DecidableEq n] [Inhabited n] (v : Matrix n Unit 𝕂) : Matrix.LpNorm p (M * v) ≤ Matrix.IpqNorm p p M * Matrix.LpNorm p v

theorem Matrix.lqnorm_div_lp_le_ipq {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} (p : ENNReal) (q : ENNReal) [RCLike 𝕂] [Fintype m] [Fintype n] [Fact (1 ≤ p)] [Fact (1 ≤ q)] (M : Matrix m n 𝕂) [DecidableEq n] [Inhabited n] (v : Matrix n Unit 𝕂) : Matrix.LpNorm q (M * v) / Matrix.LpNorm p v ≤ Matrix.IpqNorm p q M

theorem Matrix.lpnorm_div_lp_le_ipq {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} (p : ENNReal) (q : ENNReal) [RCLike 𝕂] [Fintype m] [Fintype n] [Fact (1 ≤ p)] [Fact (1 ≤ q)] (M : Matrix m n 𝕂) [DecidableEq n] [Inhabited n] (v : Matrix n Unit 𝕂) : Matrix.LpNorm q (M * v) / Matrix.LpNorm p v ≤ Matrix.IpqNorm p q M

theorem Matrix.ipqnorm_exists {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} (p : ENNReal) (q : ENNReal) [RCLike 𝕂] [Fintype m] [Fintype n] [Fact (1 ≤ p)] [Fact (1 ≤ q)] (M : Matrix m n 𝕂) [Inhabited n] [DecidableEq n] : ∃ v ∈ {v : Matrix n Unit 𝕂 | Matrix.LpNorm p v = 1}, Matrix.IpqNorm p q M = Matrix.LpNorm q (M * v)

theorem Matrix.ipq_triangle {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} (p : ENNReal) (q : ENNReal) [RCLike 𝕂] [Fintype m] [Fintype n] [Fact (1 ≤ p)] [Fact (1 ≤ q)] (M : Matrix m n 𝕂) (N : Matrix m n 𝕂) [DecidableEq n] [Inhabited n] : Matrix.IpqNorm p q (M + N) ≤ Matrix.IpqNorm p q M + Matrix.IpqNorm p q N

theorem Matrix.ipqnorm_eq0_iff {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} (p : ENNReal) (q : ENNReal) [RCLike 𝕂] [Fintype m] [Fintype n] [Fact (1 ≤ p)] [Fact (1 ≤ q)] (M : Matrix m n 𝕂) [DecidableEq n] [Inhabited n] : Matrix.IpqNorm p q M = 0 ↔ M = 0

theorem Matrix.ipqnorm_smul {𝕂 : Type u_1} {R : Type u_6} {m : Type u_7} {n : Type u_8} (p : ENNReal) (q : ENNReal) [RCLike 𝕂] [Fintype m] [Fintype n] [Fact (1 ≤ p)] [Fact (1 ≤ q)] (M : Matrix m n 𝕂) [DecidableEq n] [Inhabited n] (r : 𝕂) [SMul R (Matrix m n 𝕂)] [SMul R (Matrix m Unit 𝕂)] [Norm R] : Matrix.IpqNorm p q (r • M) = ‖r‖ * Matrix.IpqNorm p q M

theorem Matrix.ipq_mul_le_ipr_mul_irq {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} {l : Type u_9} (p : ENNReal) (q : ENNReal) (r : ENNReal) [RCLike 𝕂] [Fintype m] [Fintype n] [Fintype l] [Fact (1 ≤ p)] [Fact (1 ≤ q)] [Fact (1 ≤ r)] [DecidableEq l] [Inhabited l] [DecidableEq n] [Inhabited n] (M : Matrix m n 𝕂) (N : Matrix n l 𝕂) : Matrix.IpqNorm p q (M * N) ≤ Matrix.IpqNorm p r N * Matrix.IpqNorm r q M

@[reducible, inline]

abbrev Matrix.IpNorm {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} [RCLike 𝕂] [Fintype m] [Fintype n] (p : ENNReal) (M : Matrix m n 𝕂) : ℝ

Equations

• Matrix.IpNorm p M = Matrix.IpqNorm p p M

@[reducible, inline]

abbrev Matrix.I1Norm {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} [RCLike 𝕂] [Fintype m] [Fintype n] (M : Matrix m n 𝕂) : ℝ

Equations

• M.I1Norm = Matrix.IpNorm 1 M

@[reducible, inline]

abbrev Matrix.ItNorm {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} [RCLike 𝕂] [Fintype m] [Fintype n] (M : Matrix m n 𝕂) : ℝ

Equations

• M.ItNorm = Matrix.IpNorm ⊤ M

theorem Matrix.i1norm_eq_max_col {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} [RCLike 𝕂] [Fintype m] [Fintype n] (M : Matrix m n 𝕂) [Nonempty n] [DecidableEq n] : M.I1Norm = ⨆ (j : n), Matrix.LpNorm 1 (Matrix.col Unit fun (x : m) => M x j)

theorem Matrix.sum_norm_eq_norm_sum_ofreal {𝕂 : Type u_1} {n : Type u_8} [RCLike 𝕂] [Fintype n] (f : n → 𝕂) : ∑ x : n, ‖f x‖ = ‖∑ x : n, ↑‖f x‖‖

theorem Matrix.itnorm_eq_max_row {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} [RCLike 𝕂] [Fintype m] [Fintype n] (M : Matrix m n 𝕂) [DecidableEq n] [Inhabited n] [Nonempty m] [LE 𝕂] : M.ItNorm = ⨆ (i : m), Matrix.LpNorm 1 (Matrix.row Unit (M i))

theorem Matrix.i2tnorm_eq_max_l2norm_row {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} [RCLike 𝕂] [Fintype m] [Fintype n] (M : Matrix m n 𝕂) [DecidableEq n] [Inhabited n] [LE 𝕂] [Nonempty m] : Matrix.IpqNorm 2 ⊤ M = ⨆ (i : m), Matrix.LpNorm 2 (Matrix.row Unit (M i))

theorem Matrix.i12norm_eq_max_l2norm_col {𝕂 : Type u_1} {m : Type u_7} {n : Type u_8} [RCLike 𝕂] [Fintype m] [Fintype n] (M : Matrix m n 𝕂) [DecidableEq n] [Inhabited n] : Matrix.IpqNorm 1 2 M = ⨆ (j : n), Matrix.LpNorm 2 (Matrix.col Unit fun (x : m) => M x j)