QuantumInfo.lean

/-
Copyright (c) 2025 Alex Meiburg. All rights reserved.
Released under MIT license as described in the file LICENSE.
Authors: Alex Meiburg
-/
--Mathlib imports
import QuantumInfo.ForMathlib

--Code
import QuantumInfo.Finite.Channel.DegradableOrder
import QuantumInfo.Finite.CPTPMap
import QuantumInfo.Finite.Distance
import QuantumInfo.Finite.Qubit.Basic
import QuantumInfo.Finite.ResourceTheory.FreeState
-- import QuantumInfo.Finite.ResourceTheory.ResourceTheory --Commenting out for now -- pretty broken
import QuantumInfo.Finite.ResourceTheory.SteinsLemma
import QuantumInfo.Finite.Braket
import QuantumInfo.Finite.Capacity
import QuantumInfo.Finite.Ensemble
import QuantumInfo.Finite.Entanglement
import QuantumInfo.Finite.Entropy
-- import QuantumInfo.Finite.AxiomatizedEntropy.Defs --Experimental
-- import QuantumInfo.Finite.AxiomatizedEntropy.Renyi --Experimental
import QuantumInfo.Finite.MState
import QuantumInfo.Finite.Pinching
import QuantumInfo.Finite.POVM
import QuantumInfo.Finite.Unitary

--Documentation without code
import QuantumInfo.Finite.Capacity_doc

/-! # Quantum Information in Lean

What follows is a top-level index to some major definitions in this repository, in roughly their dependency order:
 * `Bra` and `Ket` for pure quantum states
 * `MState` for mixed quantum states
 * `𝐔[d]`, a notation for unitary matrices
 * `MEnsemble` and `PEnsemble`: Ensemble of mixed and pure states, respectively
 * `(mixed_)convex_roof` : (Mixed) convex roof extension
 * `CPTPMap` for quantum channels
 * `MState.fidelity`, the fidelity between quantum states
 * `Sᵥₙ`, `qConditionalEnt`, `qMutualInfo`, `coherentInfo`, etc. - different notions of entropy or information in quantum states
-/