Matrix.frobenius_nnnorm_def
theorem Matrix.frobenius_nnnorm_def :
∀ {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‖₊ = (Finset.univ.sum fun i => Finset.univ.sum fun j => ‖A i j‖₊ ^ 2) ^ (1 / 2)
The theorem `Matrix.frobenius_nnnorm_def` states that for any matrix `A` with entries in a seminormed additive commutative group `α`, the nonnegative norm `‖A‖₊` of the matrix is equal to the square root of the sum of the squares of the nonnegative norms `‖A i j‖₊` of its elements, where the sum is taken over all indices `i` and `j` in the respective finite sets of row and column indices of `A`.
More concisely: The L1-norm of a matrix equals the square root of the sum of the squares of the L1-norms of its elements.
|
Matrix.boundedSMul
theorem Matrix.boundedSMul :
∀ {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 : BoundedSMul R α],
BoundedSMul R (Matrix m n α)
The theorem `Matrix.boundedSMul` states that for any types `R`, `m`, `n`, and `α`, if `m` and `n` are finite types, `R` is a semi-normed ring, `α` is a semi-normed additive commutative group, `α` is an `R`-module, and there is a bounded scalar multiplication from `R` to `α`, then there is a bounded scalar multiplication from `R` to the matrix whose entries are in `α` and whose rows are indexed by `m` and columns are indexed by `n`.
More concisely: If `R` is a semi-normed ring, `α` is a semi-normed additive commutative group and an `R`-module, `m` and `n` are finite types, and there is a bounded scalar multiplication from `R` to `α`, then there exists a bounded scalar multiplication from `R` to the `m x n` matrix over `α`.
|
Matrix.linfty_opNNNorm_col
theorem Matrix.linfty_opNNNorm_col :
∀ {m : Type u_3} {α : Type u_5} [inst : Fintype m] [inst_1 : SeminormedAddCommGroup α] (v : m → α),
‖Matrix.col v‖₊ = ‖v‖₊
The theorem `Matrix.linfty_opNNNorm_col` states that for any type `m` and any semi-normed add commutative group `α`, and for any function `v` from `m` to `α`, the non-negative norm (denoted by ‖‖₊) of the column matrix whose entries are given by `v` is equal to the non-negative norm of the function `v` itself. Essentially, it indicates that the non-negative norm remains unchanged when a function is transformed into a column matrix.
More concisely: For any semi-normed add commutative group α and type m, the non-negative norm of a function from m to α equals the non-negative norm of the column matrix formed by its values.
|
Matrix.frobeniusBoundedSMul
theorem Matrix.frobeniusBoundedSMul :
∀ {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 : BoundedSMul R α],
BoundedSMul R (Matrix m n α)
This theorem states that for any type `R` that forms a semi-normed ring, types `m` and `n` that are finite types, and a type `α` that forms a semi-normed additive commutative group and a module over `R`, if `α` has the bounded scalar multiplication property, then the type of matrices with rows indexed by `m` and columns indexed by `n` and entries in `α`, `Matrix m n α`, also has the bounded scalar multiplication property. This is related to the Frobenius norm, which is a way of measuring the size of a matrix.
More concisely: For any semi-normed ring `R`, finite types `m` and `n`, and a semi-normed additive commutative group and `R`-module `α` with the bounded scalar multiplication property, the type of `m x n` matrices with entries in `α` also has the bounded scalar multiplication property.
|
Matrix.linfty_opNNNorm_def
theorem Matrix.linfty_opNNNorm_def :
∀ {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‖₊ = Finset.univ.sup fun i => Finset.univ.sum fun j => ‖A i j‖₊
The theorem `Matrix.linfty_opNNNorm_def` states for any type `m`, `n`, and `α`, where `m` and `n` are finite types and `α` is a seminormed additively commutative group, for a matrix `A` of type `Matrix m n α`, the non-negative norm of `A` is equal to the supremum (maximum) over all rows `i` of the sum over all columns `j` of the non-negative norms of the elements of `A` at position `(i, j)`. In other words, the non-negative norm of a matrix is the maximum row sum of the non-negative norms of its elements.
More concisely: For any finite types `m` and `n` and seminormed additively commutative group `α`, the non-negative matrix norm of a matrix `A` of type `Matrix m n α` equals the maximum row sum of non-negative element norms in `A`.
|
Matrix.linfty_opNNNorm_mul
theorem Matrix.linfty_opNNNorm_mul :
∀ {l : Type u_2} {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype l] [inst_1 : Fintype m]
[inst_2 : Fintype n] [inst_3 : NonUnitalSeminormedRing α] (A : Matrix l m α) (B : Matrix m n α),
‖A * B‖₊ ≤ ‖A‖₊ * ‖B‖₊
The theorem `Matrix.linfty_opNNNorm_mul` states that for any two matrices `A` and `B` with entries in a non-unital semi-normed ring `α`, the `ℓ∞` (also known as the infinity or Chebyshev) norm of the product of `A` and `B` is less than or equal to the product of the `ℓ∞` norms of `A` and `B` individually. This theorem holds for matrices of any dimension, as indexed by arbitrary types `l`, `m`, `n`, where `l`, `m` index the rows and `n` indexes the columns of the matrices, respectively.
More concisely: For any matrices A and B with entries in a non-unital semi-normed ring, the ℓ∞ norm of their product is less than or equal to the product of their individual ℓ∞ norms.
|
Matrix.linftyOpBoundedSMul
theorem Matrix.linftyOpBoundedSMul :
∀ {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 : BoundedSMul R α],
BoundedSMul R (Matrix m n α)
This theorem, `Matrix.linftyOpBoundedSMul`, asserts that given any type `R` with a seminormed ring structure, any type `m` and `n` with a finite number of elements (Fintype), and a type `α` with a seminormed additive commutative group structure and a module structure over `R` that has bounded scalar multiplication, then a matrix with rows indexed by `m`, columns indexed by `n`, and entries in `α` also has bounded scalar multiplication. In mathematical terms, this is stating that the sup norm of the L1 norm is bounded for such matrices.
More concisely: Given a seminormed ring `R`, a finite type `m x n α` (where `α` is a seminormed additive commutative group with bounded scalar multiplication over `R`), the supremum of the L1 norms of the products of scalars and matrix entries is bounded.
|