-
Notifications
You must be signed in to change notification settings - Fork 1
All issues
Issue creation is restricted in this repository
Issues
is:issue state:open
is:issue state:open
Search results
Add prescribed-rate spectral-radius power bounds
formalizationLean 4 formalization taskLean 4 formalization taskStatus: Open.#531 In LionSR/QICLean;- Status: Open.#525 In LionSR/QICLean;
Wolf Ch6: primitive positive-map equivalences (Theorem 6.7)
blueprint-syncBlueprint out of sync with Lean codeBlueprint out of sync with Lean codeformalizationLean 4 formalization taskLean 4 formalization taskwolf-ch6Wolf Lecture Notes — Chapter 6: Spectral PropertiesWolf Lecture Notes — Chapter 6: Spectral PropertiesStatus: Open.#479 In LionSR/QICLean;Wolf Ch6: covariance and peripheral eigensystem (Proposition 6.7)
blueprint-syncBlueprint out of sync with Lean codeBlueprint out of sync with Lean codeformalizationLean 4 formalization taskLean 4 formalization taskwolf-ch6Wolf Lecture Notes — Chapter 6: Spectral PropertiesWolf Lecture Notes — Chapter 6: Spectral PropertiesStatus: Open.#478 In LionSR/QICLean;Wolf Ch6: abstract Schwarz peripheral-spectrum theorem (Theorem 6.6)
blueprint-syncBlueprint out of sync with Lean codeBlueprint out of sync with Lean codeformalizationLean 4 formalization taskLean 4 formalization taskwolf-ch6Wolf Lecture Notes — Chapter 6: Spectral PropertiesWolf Lecture Notes — Chapter 6: Spectral PropertiesStatus: Open.#477 In LionSR/QICLean;Wolf Ch6: spectral-radius PSD eigenvector for arbitrary positive maps (Theorem 6.5)
blueprint-syncBlueprint out of sync with Lean codeBlueprint out of sync with Lean codeformalizationLean 4 formalization taskLean 4 formalization taskwolf-ch6Wolf Lecture Notes — Chapter 6: Spectral PropertiesWolf Lecture Notes — Chapter 6: Spectral PropertiesStatus: Open.#476 In LionSR/QICLean;Wolf Ch6: positive-map ergodic time average (Corollary 6.3)
blueprint-syncBlueprint out of sync with Lean codeBlueprint out of sync with Lean codeformalizationLean 4 formalization taskLean 4 formalization taskwolf-ch6Wolf Lecture Notes — Chapter 6: Spectral PropertiesWolf Lecture Notes — Chapter 6: Spectral PropertiesStatus: Open.#475 In LionSR/QICLean;Low-layer matrix reindex star equivalence and bipartite coefficient naturality
1703.09188arXiv:1703.09188 — Matrix Product UnitariesarXiv:1703.09188 — Matrix Product UnitariesformalizationLean 4 formalization taskLean 4 formalization taskmpuMatrix Product Unitaries: structure, index, symmetries, and QCAMatrix Product Unitaries: structure, index, symmetries, and QCAStatus: Open.#465 In LionSR/QICLean;Wolf Ch2: signed canonical pairs for four-dimensional Minkowski-selfadjoint matrices
blueprint-syncBlueprint out of sync with Lean codeBlueprint out of sync with Lean codeformalizationLean 4 formalization taskLean 4 formalization taskwolf-ch2Wolf Lecture Notes — Chapter 2: RepresentationsWolf Lecture Notes — Chapter 2: RepresentationsStatus: Open.#426 In LionSR/QICLean;Wolf Ch2: specialize the Lorentz SVD to qubit channels and canonical Kraus ranks
blueprint-syncBlueprint out of sync with Lean codeBlueprint out of sync with Lean codeformalizationLean 4 formalization taskLean 4 formalization taskwolf-ch2Wolf Lecture Notes — Chapter 2: RepresentationsWolf Lecture Notes — Chapter 2: RepresentationsStatus: Open.#379 In LionSR/QICLean;Wolf Ch2: Lorentz singular-value decomposition for positive two-qubit operators
blueprint-syncBlueprint out of sync with Lean codeBlueprint out of sync with Lean codeformalizationLean 4 formalization taskLean 4 formalization taskwolf-ch2Wolf Lecture Notes — Chapter 2: RepresentationsWolf Lecture Notes — Chapter 2: RepresentationsStatus: Open.#378 In LionSR/QICLean;Wolf Ch8: trace-norm convergence toward asymptotic states (Eqs. 8.112–8.117)
blueprint-syncBlueprint out of sync with Lean codeBlueprint out of sync with Lean codeformalizationLean 4 formalization taskLean 4 formalization taskwolf-ch8Wolf Lecture Notes — Chapter 8: Distance Measures and MixednessWolf Lecture Notes — Chapter 8: Distance Measures and MixednessStatus: Open.#301 In LionSR/QICLean;