LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Analysis.NormedSpace.Star.Matrix

`Matrix.cstar_norm_def` theorem Matrix.cstar_norm_def : ∀ {𝕜 : Type u_1} {n : Type u_3} [inst : RCLike 𝕜] [inst_1 : Fintype n] [inst_2 : DecidableEq n] (A : Matrix n n 𝕜), ‖A‖ = ‖Matrix.toEuclideanCLM A‖ The theorem `Matrix.cstar_norm_def` states that for any type `𝕜`, any type `n` that is a Fintype and has Decidable Equality, and a square matrix `A` of type `Matrix n n 𝕜`, the norm of `A`, represented as `‖A‖`, is equal to the norm of the Euclidean column-major linear map of `A`, represented as `‖Matrix.toEuclideanCLM A‖`. Here, `𝕜` is likely a number field (e.g., the real or complex numbers), `n` denotes the indices of the rows and columns of the matrix, `Fintype` ensures that `n` is a finite type, and `DecidableEq` ensures that equality within `n` is a decidable property. More concisely: For any number field `𝕜`, finite type `n` with decidable equality, and square matrix `A` of size `n x n` over `𝕜`, the matrix norm of `A` equals the Euclidean norm of the column-major linear map of `A`.
`entrywise_sup_norm_bound_of_unitary` theorem entrywise_sup_norm_bound_of_unitary : ∀ {𝕜 : Type u_1} {n : Type u_3} [inst : RCLike 𝕜] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {U : Matrix n n 𝕜}, U ∈ Matrix.unitaryGroup n 𝕜 → ‖U‖ ≤ 1 The theorem `entrywise_sup_norm_bound_of_unitary` states that for any type `𝕜` that behaves like a real or complex number (denoted by `[inst : RCLike 𝕜]`), and any finite type `n`, such that we can decide equality on elements of type `n` (`[inst_2 : DecidableEq n]`), if `U` is a `n` by `n` matrix over `𝕜` that belongs to the unitary group of `n` by `n` matrices over `𝕜` (i.e., `U` is a unitary matrix), then the sup norm (or maximum absolute value of its entries) of `U` is less than or equal to `1`. In mathematical terms, this is saying that if `U` is a unitary matrix, then the maximum absolute value of the entries of `U` is at most `1`. This result is fundamental in several areas of linear algebra and quantum computing, where unitary matrices play a crucial role. More concisely: For any type `𝕜` that behaves like the real or complex numbers, and for finite type `n` with decidable equality, if `U` is a `n` by `n` unitary matrix over `𝕜`, then the sup norm of `U` is bounded by 1.
`Matrix.l2_opNorm_conjTranspose_mul_self` theorem Matrix.l2_opNorm_conjTranspose_mul_self : ∀ {𝕜 : Type u_1} {m : Type u_2} {n : Type u_3} [inst : RCLike 𝕜] [inst_1 : Fintype m] [inst_2 : Fintype n] [inst_3 : DecidableEq n] (A : Matrix m n 𝕜), ‖A.conjTranspose * A‖ = ‖A‖ * ‖A‖ The theorem `Matrix.l2_opNorm_conjTranspose_mul_self` states that for any type `𝕜` that behaves like a ring or a field (indicated by `RCLike 𝕜`), types `m` and `n` which are finite (indicated by `Fintype m` and `Fintype n`) and have decidable equality (indicated by `DecidableEq n`), and a matrix `A` with entries in `𝕜` and dimensions indexed by `m` and `n`, the L2 operator norm (the square root of the largest eigenvalue of `A* A`) of the product of the conjugate transpose of `A` and `A` is equal to the product of the L2 operator norm of `A` and itself. Here, `Matrix.conjTranspose` is a function that computes the conjugate transpose of a matrix, `‖A‖` denotes the L2 operator norm of `A`, and '' denotes matrix multiplication. More concisely: For any ring or field `𝕜`, finite types `m` and `n` with decidable equality, and matrix `A` of dimension `m x n` over `𝕜`, the L2 norm of `A` multiplied by the L2 norm of its conjugate transpose equals the L2 norm of `A` multiplied by itself. In Lean notation: `∀ 𝕜: Type u \| RCLike 𝕜, (∀ m n: Nat, Fintype m → Fintype n → DecidableEq n → Matrix 𝕜 m n → Real = ‖A⟩.‖ ‖Matrix.conjTranspose A⟩.‖ = ‖A⟩.‖ * ‖A⟩.‖`.`
`Matrix.instCstarRing` theorem Matrix.instCstarRing : ∀ {𝕜 : Type u_1} {n : Type u_3} [inst : RCLike 𝕜] [inst_1 : Fintype n] [inst_2 : DecidableEq n], CstarRing (Matrix n n 𝕜) This theorem states that for any type `𝕜` and `n` where `𝕜` behaves like real or complex numbers (has a structure `RCLike 𝕜`), `n` is a finite type (`Fintype n`), and equality on `n` is decidable (`DecidableEq n`), then the matrix with rows and columns indexed by `n` and entries in `𝕜` (i.e., `Matrix n n 𝕜`) forms a `CstarRing`. This is a special mathematical construct related to the operator norm on the matrix given by its identification with the continuous linear endomorphisms of the n-dimensional Euclidean space over `𝕜`. A `CstarRing` captures some properties of complex numbers and linear operators, which are useful in quantum mechanics and other areas of mathematics. More concisely: For any type `𝕜` behaving like the real or complex numbers and having decidable equality, and `n` a finite type with decidable equality, the `Matrix n n 𝕜` forms a `CstarRing`.
`Matrix.cstar_nnnorm_def` theorem Matrix.cstar_nnnorm_def : ∀ {𝕜 : Type u_1} {n : Type u_3} [inst : RCLike 𝕜] [inst_1 : Fintype n] [inst_2 : DecidableEq n] (A : Matrix n n 𝕜), ‖A‖₊ = ‖Matrix.toEuclideanCLM A‖₊ The theorem `Matrix.cstar_nnnorm_def` states that for any type `𝕜`, any type `n`, under the conditions that `𝕜` behaves like a real closed field, `n` is a finite type, and `n` has decidable equality, for any square matrix `A` with entries in `𝕜` and indices in `n`, the non-negative norm of `A` (`‖A‖₊`) is equal to the non-negative norm of the result of applying the function `Matrix.toEuclideanCLM` to `A` (`‖Matrix.toEuclideanCLM A‖₊`). This theorem is a variant of `Matrix.l2_opNNNorm_def`, but it expresses the result in a more bundled form for square matrices. More concisely: For any square matrix A with entries in a real closed field and indices in a finite type with decidable equality, the non-negative norm of A is equal to the non-negative norm of Matrix.toEuclideanCLM(A).