Skip to content

refactor: Reorganise the QuantumInfo directory #1124

Open
jstoobysmith wants to merge 4 commits into
leanprover-community:masterfrom
jstoobysmith:moveQuantumInfoFiles
Open

refactor: Reorganise the QuantumInfo directory #1124
jstoobysmith wants to merge 4 commits into
leanprover-community:masterfrom
jstoobysmith:moveQuantumInfoFiles

Conversation

@jstoobysmith
Copy link
Copy Markdown
Member

No changes to content, just a reorganisation. New directory structure is the following:

QuantumInfo
 ┣ Capacity
 ┃ ┣ Capacity.lean
 ┃ ┗ Capacity_doc.lean
 ┣ Channels
 ┃ ┣ Bundled.lean
 ┃ ┣ CPTP.lean
 ┃ ┣ DegradableOrder.lean
 ┃ ┣ Dual.lean
 ┃ ┣ MatrixMap.lean
 ┃ ┣ Pinching.lean
 ┃ ┗ Unbundled.lean
 ┣ ClassicalInfo
 ┃ ┣ ForMathlib
 ┃ ┃ ┗ Analysis
 ┃ ┃ ┃ ┗ SpecialFunctions
 ┃ ┃ ┃ ┃ ┗ Log
 ┃ ┃ ┃ ┃ ┃ ┗ NegMulLog.lean
 ┃ ┣ Capacity.lean
 ┃ ┣ Channel.lean
 ┃ ┣ Distribution.lean
 ┃ ┣ Entropy.lean
 ┃ ┗ Prob.lean
 ┣ Entropy
 ┃ ┣ Axiomatized
 ┃ ┃ ┣ Defs.lean
 ┃ ┃ ┗ Renyi.lean
 ┃ ┣ DPI.lean
 ┃ ┣ Relative.lean
 ┃ ┣ SSA.lean
 ┃ ┗ VonNeumann.lean
 ┣ ForMathlib
 ┃ ┣  ...
 ┣ Measurements
 ┃ ┗ POVM.lean
 ┣ Operators
 ┃ ┗ Unitary.lean
 ┣ ResourceTheory
 ┃ ┣ FreeState.lean
 ┃ ┣ HypothesisTesting.lean
 ┃ ┣ ResourceTheory.lean
 ┃ ┗ SteinsLemma.lean
 ┣ States
 ┃ ┣ Mixed
 ┃ ┃ ┣ Fidelity.lean
 ┃ ┃ ┣ MState.lean
 ┃ ┃ ┗ TraceDistance.lean
 ┃ ┣ Pure
 ┃ ┃ ┣ BargmannInvariant.lean
 ┃ ┃ ┣ Braket.lean
 ┃ ┃ ┗ Qubit.lean
 ┃ ┣ Ensemble.lean
 ┃ ┗ Entanglement.lean
 ┗ Regularized.lean

@jstoobysmith jstoobysmith added t-quantum-info Quantum information RFC Request for comment labels May 26, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

RFC Request for comment t-quantum-info Quantum information

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant