Project-declaredLean 4.28.0 · mathlib@8f9d9cff6bd7

Matrix op Norm mul le

Matrix.opNorm_mul_le

quantum information entropy quantum channels ssa

Plain-language statement

The operator norm of a matrix product is at most the product of the operator norms.

Exact Lean statement

theorem Matrix.opNorm_mul_le {l m n 𝕜 : Type*} [Fintype l] [Fintype m] [Fintype n]
    [DecidableEq l] [DecidableEq m] [DecidableEq n] [RCLike 𝕜]
    (A : Matrix l m 𝕜) (B : Matrix m n 𝕜) :
    Matrix.opNorm (A * B) ≤ Matrix.opNorm A * Matrix.opNorm B

Formal artifact

Lean source

Canonical source

Full Lean sourceLean 4

theorem Matrix.opNorm_mul_le {l m n 𝕜 : Type*} [Fintype l] [Fintype m] [Fintype n]    [DecidableEq l] [DecidableEq m] [DecidableEq n] [RCLike 𝕜]    (A : Matrix l m 𝕜) (B : Matrix m n 𝕜) :    Matrix.opNorm (A * B) ≤ Matrix.opNorm A * Matrix.opNorm B := by  have h_opNorm_mul_le : ∀ (A : Matrix l m 𝕜) (B : Matrix m n 𝕜), Matrix.opNorm (A * B) ≤ Matrix.opNorm A * Matrix.opNorm B := by    intro A B    have h_comp : Matrix.toEuclideanLin (A * B) = Matrix.toEuclideanLin A ∘ₗ Matrix.toEuclideanLin B := by      ext; simp [toEuclideanLin]    convert ContinuousLinearMap.opNorm_comp_le ( Matrix.toEuclideanLin A |> LinearMap.toContinuousLinearMap ) ( Matrix.toEuclideanLin B |> LinearMap.toContinuousLinearMap ) using 1;    unfold Matrix.opNorm;    exact congr_arg _ ( by aesop );  exact h_opNorm_mul_le A B

Project: quantumInfo
License: MIT
Commit: 56e83a9288a3
Source: QuantumInfo/Finite/Entropy/SSA.lean:237-248

Reuse this declaration

Bring the exact result into your workflow

The import identifies the source module. Your project still needs the pinned package dependency shown on this page.

What this badge means

This completion status comes from the project or community source. It has not yet been represented here as an independent rebuild and axiom audit.

Continue in this project

Related declarations

Project-declaredLean 4.28.0

Conj Transpose isometry mul isometry le one

conjTranspose_isometry_mul_isometry_le_one

Project documentation

The operator norm of the conjugate transpose is equal to the operator norm. -/ theorem Matrix.opNorm_conjTranspose_eq_opNorm {m n : Type*} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (A : Matrix m n 𝕜) : Matrix.opNorm Aᴴ = Matrix.opNorm A := by unfold Matrix.opNorm rw [← ContinuousLinearMap.adjoint.norm_map (toEuclideanLin A).toContinuousLine...

quantum informationentropyquantum channels

Source project: quantumInfo

Person-level attribution pending.

View proof record

Project-declaredLean 4.28.0

Convex roof of pure

convex_roof_of_pure

Plain-language statement

The convex roof extension of g : KetUpToPhase d → ℝ≥0 applied to a pure state ψ is g (KetUpToPhase.mk ψ).

quantum informationentropyquantum channels

Source project: quantumInfo

Person-level attribution pending.

View proof record

Project-declaredLean 4.28.0

Id achieves Rate log dim

CPTPMap.id_achievesRate_log_dim

Plain-language statement

The identity channel on D dimensional space achieves a rate of log2(D).

quantum informationentropyquantum channels

Source project: quantumInfo

Person-level attribution pending.

View proof record