Skip to content

refactor: Reorganise the QuantumInfo directory #1124

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
jstoobysmith wants to merge 5 commits into
base: master
Choose a base branch
from
Open

refactor: Reorganise the QuantumInfo directory #1124

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
27722a7
refactor: File moves
jstoobysmith May 26, 2026
4cc42bd
fix: Build by renaming imports
jstoobysmith May 26, 2026
870b473
refactor: Lint
jstoobysmith May 26, 2026
0b7377b
fix: Lint
jstoobysmith May 26, 2026
086032a
feat: Line length
jstoobysmith May 26, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
56 changes: 36 additions & 20 deletions QuantumInfo.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,30 +6,46 @@ Authors: Alex Meiburg
--Mathlib imports
module

public import QuantumInfo.ForMathlib
public import QuantumInfo.ForMathlib.ContinuousLinearMap
public import QuantumInfo.ForMathlib.ComplexLaplaceTransform
public import QuantumInfo.ForMathlib.ContinuousSup
public import QuantumInfo.ForMathlib.Filter
public import QuantumInfo.ForMathlib.HermitianMat
public import QuantumInfo.ForMathlib.Isometry
public import QuantumInfo.ForMathlib.LinearEquiv
public import QuantumInfo.ForMathlib.MatrixNorm.TraceNorm
public import QuantumInfo.ForMathlib.Matrix
public import QuantumInfo.ForMathlib.Minimax
public import QuantumInfo.ForMathlib.Misc
public import QuantumInfo.ForMathlib.Unitary

--Code
public import QuantumInfo.Finite.Channel.DegradableOrder
public import QuantumInfo.Finite.CPTPMap
public import QuantumInfo.Finite.Distance
public import QuantumInfo.Finite.Qubit.Basic
public import QuantumInfo.Finite.ResourceTheory.FreeState
-- import QuantumInfo.Finite.ResourceTheory.ResourceTheory --Commenting out for now -- pretty broken
public import QuantumInfo.Finite.ResourceTheory.SteinsLemma
public import QuantumInfo.Finite.Braket
public import QuantumInfo.Finite.Capacity
public import QuantumInfo.Finite.Ensemble
public import QuantumInfo.Finite.Entanglement
public import QuantumInfo.Finite.Entropy
-- import QuantumInfo.Finite.AxiomatizedEntropy.Defs --Experimental
-- import QuantumInfo.Finite.AxiomatizedEntropy.Renyi --Experimental
public import QuantumInfo.Finite.MState
public import QuantumInfo.Finite.Pinching
public import QuantumInfo.Finite.POVM
public import QuantumInfo.Finite.Unitary
public import QuantumInfo.Channels.DegradableOrder
public import QuantumInfo.Channels.Bundled
public import QuantumInfo.Channels.CPTP
public import QuantumInfo.Channels.Dual
public import QuantumInfo.Channels.MatrixMap
public import QuantumInfo.Channels.Unbundled
public import QuantumInfo.States.Mixed.Fidelity
public import QuantumInfo.States.Mixed.TraceDistance
public import QuantumInfo.States.Pure.Qubit
public import QuantumInfo.ResourceTheory.FreeState
public import QuantumInfo.ResourceTheory.SteinsLemma
public import QuantumInfo.States.Pure.Braket
public import QuantumInfo.Capacity.Capacity
public import QuantumInfo.States.Ensemble
public import QuantumInfo.States.Entanglement
public import QuantumInfo.Entropy.VonNeumann
public import QuantumInfo.Entropy.SSA
public import QuantumInfo.Entropy.Relative
public import QuantumInfo.Entropy.DPI
public import QuantumInfo.States.Mixed.MState
public import QuantumInfo.Channels.Pinching
public import QuantumInfo.Measurements.POVM
public import QuantumInfo.Operators.Unitary

--Documentation without code
public import QuantumInfo.Finite.Capacity_doc
public import QuantumInfo.Capacity.Capacity_doc

--Classical information theory
-- import QuantumInfo.ClassicalInfo.Capacity
Expand Down
14 changes: 11 additions & 3 deletions QuantumInfo/Finite/Capacity.lean → QuantumInfo/Capacity/Capacity.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,9 +7,17 @@ module

public import Mathlib.Analysis.SpecialFunctions.Log.Base

public import QuantumInfo.Finite.Entropy
public import QuantumInfo.Finite.CPTPMap
public import QuantumInfo.Finite.Distance
public import QuantumInfo.Entropy.VonNeumann
public import QuantumInfo.Entropy.SSA
public import QuantumInfo.Entropy.Relative
public import QuantumInfo.Entropy.DPI
public import QuantumInfo.Channels.Bundled
public import QuantumInfo.Channels.CPTP
public import QuantumInfo.Channels.Dual
public import QuantumInfo.Channels.MatrixMap
public import QuantumInfo.Channels.Unbundled
public import QuantumInfo.States.Mixed.Fidelity
public import QuantumInfo.States.Mixed.TraceDistance
public import Physlib.Meta.Sorry

/-! # Quantum Capacity
Expand Down
0 QuantumInfo/Finite/Capacity_doc.lean → QuantumInfo/Capacity/Capacity_doc.lean
View file
Open in desktop
File renamed without changes.
4 changes: 2 additions & 2 deletions QuantumInfo/Finite/CPTPMap/Bundled.lean → QuantumInfo/Channels/Bundled.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,8 @@ Authors: Alex Meiburg
-/
module

public import QuantumInfo.Finite.CPTPMap.Unbundled
public import QuantumInfo.Finite.MState
public import QuantumInfo.Channels.Unbundled
public import QuantumInfo.States.Mixed.MState

public import Mathlib.Topology.Order.Hom.Basic

Expand Down
4 changes: 2 additions & 2 deletions QuantumInfo/Finite/CPTPMap/CPTP.lean → QuantumInfo/Channels/CPTP.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,8 @@ Authors: Alex Meiburg
-/
module

public import QuantumInfo.Finite.CPTPMap.Bundled
public import QuantumInfo.Finite.Unitary
public import QuantumInfo.Channels.Bundled
public import QuantumInfo.Operators.Unitary

/-! # Completely Positive Trace Preserving maps

Expand Down
6 changes: 5 additions & 1 deletion ...mInfo/Finite/Channel/DegradableOrder.lean → QuantumInfo/Channels/DegradableOrder.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,11 @@ Authors: Alex Meiburg
-/
module

public import QuantumInfo.Finite.CPTPMap
public import QuantumInfo.Channels.Bundled
public import QuantumInfo.Channels.CPTP
public import QuantumInfo.Channels.Dual
public import QuantumInfo.Channels.MatrixMap
public import QuantumInfo.Channels.Unbundled

/-! # The Degradable Order

Expand Down
2 changes: 1 addition & 1 deletion QuantumInfo/Finite/CPTPMap/Dual.lean → QuantumInfo/Channels/Dual.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ Authors: Alex Meiburg, Dennj Osele
-/
module

public import QuantumInfo.Finite.CPTPMap.Bundled
public import QuantumInfo.Channels.Bundled
public import Mathlib.LinearAlgebra.Matrix.FiniteDimensional

/-! # Duals of matrix map
Expand Down
17 changes: 14 additions & 3 deletions QuantumInfo/Finite/CPTPMap/MatrixMap.lean → QuantumInfo/Channels/MatrixMap.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,9 +10,20 @@ public import Mathlib.LinearAlgebra.PiTensorProduct
public import Mathlib.LinearAlgebra.PiTensorProduct.Basis
public import Mathlib.Data.Set.Card
public import Mathlib.Algebra.Module.LinearMap.Basic
public import QuantumInfo.ForMathlib
public import QuantumInfo.Finite.Braket
public import QuantumInfo.Finite.MState
public import QuantumInfo.ForMathlib.ContinuousLinearMap
public import QuantumInfo.ForMathlib.ComplexLaplaceTransform
public import QuantumInfo.ForMathlib.ContinuousSup
public import QuantumInfo.ForMathlib.Filter
public import QuantumInfo.ForMathlib.HermitianMat
public import QuantumInfo.ForMathlib.Isometry
public import QuantumInfo.ForMathlib.LinearEquiv
public import QuantumInfo.ForMathlib.MatrixNorm.TraceNorm
public import QuantumInfo.ForMathlib.Matrix
public import QuantumInfo.ForMathlib.Minimax
public import QuantumInfo.ForMathlib.Misc
public import QuantumInfo.ForMathlib.Unitary
public import QuantumInfo.States.Pure.Braket
public import QuantumInfo.States.Mixed.MState

/-! # Linear maps of matrices

Expand Down
13 changes: 10 additions & 3 deletions QuantumInfo/Finite/Pinching.lean → QuantumInfo/Channels/Pinching.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,9 +5,16 @@ Authors: Leonardo A Lessa, Alex Meiburg
-/
module

public import QuantumInfo.Finite.CPTPMap
public import QuantumInfo.Finite.MState
public import QuantumInfo.Finite.Entropy
public import QuantumInfo.Channels.Bundled
public import QuantumInfo.Channels.CPTP
public import QuantumInfo.Channels.Dual
public import QuantumInfo.Channels.MatrixMap
public import QuantumInfo.Channels.Unbundled
public import QuantumInfo.States.Mixed.MState
public import QuantumInfo.Entropy.VonNeumann
public import QuantumInfo.Entropy.SSA
public import QuantumInfo.Entropy.Relative
public import QuantumInfo.Entropy.DPI
public import QuantumInfo.ForMathlib.HermitianMat.CFC

/-! # Pinching channels
Expand Down
2 changes: 1 addition & 1 deletion QuantumInfo/Finite/CPTPMap/Unbundled.lean → QuantumInfo/Channels/Unbundled.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ Authors: Alex Meiburg
-/
module

public import QuantumInfo.Finite.CPTPMap.MatrixMap
public import QuantumInfo.Channels.MatrixMap
public import QuantumInfo.ForMathlib.MatrixNorm.TraceNorm

/-! # Properties of Matrix Maps
Expand Down
2 changes: 1 addition & 1 deletion QuantumInfo/ClassicalInfo/Prob.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -231,7 +231,7 @@ end Prob
multiplication, and a bijection between the `T` and a convex set of `U`.
For instance, in `Mixable (Distribution (Fin n))`, `U` is `n`-element vectors
(which form the probability simplex, degenerate in one dimension). For
`QuantumInfo.Finite.MState` density matrices in quantum mechanics, which are
`QuantumInfo.States.Mixed.MState` density matrices in quantum mechanics, which are
PSD matrices of trace 1, `U` is the underlying matrix.

Why not just stick with existing notions of `Convex`? `Convex` requires that
Expand Down
9 changes: 6 additions & 3 deletions ...mInfo/Finite/AxiomatizedEntropy/Defs.lean → QuantumInfo/Entropy/Axiomatized/Defs.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,9 +6,12 @@ Authors: Alex Meiburg
module

public import QuantumInfo.ClassicalInfo.Entropy
public import QuantumInfo.Finite.MState
public import QuantumInfo.Finite.CPTPMap

public import QuantumInfo.States.Mixed.MState
public import QuantumInfo.Channels.Bundled
public import QuantumInfo.Channels.CPTP
public import QuantumInfo.Channels.Dual
public import QuantumInfo.Channels.MatrixMap
public import QuantumInfo.Channels.Unbundled
/-! # Generalized quantum entropy and relative entropy
Here we define a broad notion of entropy axiomatically, `Entropy`, and the Prop
Expand Down
2 changes: 1 addition & 1 deletion ...Info/Finite/AxiomatizedEntropy/Renyi.lean → QuantumInfo/Entropy/Axiomatized/Renyi.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ Authors: Alex Meiburg
-/
module

public import QuantumInfo.Finite.AxiomatizedEntropy.Defs
public import QuantumInfo.Entropy.Axiomatized.Defs

/-! # Quantum Relative Entropy and α-Renyi Entropy -/

Expand Down
2 changes: 1 addition & 1 deletion QuantumInfo/Finite/Entropy/DPI.lean → QuantumInfo/Entropy/DPI.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ Authors: Alex Meiburg
-/
module

public import QuantumInfo.Finite.Entropy.Relative
public import QuantumInfo.Entropy.Relative
public import QuantumInfo.ForMathlib.HermitianMat.Sqrt
public import QuantumInfo.ForMathlib.HermitianMat.LiebConcavity

Expand Down
4 changes: 3 additions & 1 deletion QuantumInfo/Finite/Entropy/Relative.lean → QuantumInfo/Entropy/Relative.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,8 @@ Authors: Alex Meiburg
-/
module

public import QuantumInfo.Finite.Entropy.VonNeumann
public import QuantumInfo.Entropy.VonNeumann
public import Physlib.Meta.Sorry

@[expose] public section

Expand Down Expand Up @@ -2119,6 +2120,7 @@ TODO:
* Define (joint) convexity as its own thing - a `ConvexOn` for `Mixable` types.
* Maybe, more broadly, find a way to make `ConvexOn` work with the subset of `Matrix` that corresponds to `MState`.
-/
@[sorryful]
theorem qRelativeEnt_joint_convexity :
∀ (ρ₁ ρ₂ σ₁ σ₂ : MState d), ∀ (p : Prob),
𝐃(p [ρ₁ ↔ ρ₂]‖p [σ₁ ↔ σ₂]) ≤ p * 𝐃(ρ₁‖σ₁) + (1 - p) * 𝐃(ρ₂‖σ₂) := by
Expand Down
2 changes: 1 addition & 1 deletion QuantumInfo/Finite/Entropy/SSA.lean → QuantumInfo/Entropy/SSA.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ Authors: Alex Meiburg
-/
module

public import QuantumInfo.Finite.Entropy.VonNeumann
public import QuantumInfo.Entropy.VonNeumann
public import QuantumInfo.ForMathlib.HermitianMat.Sqrt

/-!
Expand Down
8 changes: 6 additions & 2 deletions QuantumInfo/Finite/Entropy/VonNeumann.lean → QuantumInfo/Entropy/VonNeumann.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,12 @@ Authors: Alex Meiburg
-/
module

public import QuantumInfo.Finite.Braket
public import QuantumInfo.Finite.CPTPMap
public import QuantumInfo.States.Pure.Braket
public import QuantumInfo.Channels.Bundled
public import QuantumInfo.Channels.CPTP
public import QuantumInfo.Channels.Dual
public import QuantumInfo.Channels.MatrixMap
public import QuantumInfo.Channels.Unbundled
public import QuantumInfo.ClassicalInfo.Entropy

/-!
Expand Down
12 changes: 0 additions & 12 deletions QuantumInfo/Finite/CPTPMap.lean
View file
Open in desktop

This file was deleted.

22 changes: 0 additions & 22 deletions QuantumInfo/Finite/Distance.lean
View file
Open in desktop

This file was deleted.

11 changes: 0 additions & 11 deletions QuantumInfo/Finite/Entropy.lean
View file
Open in desktop

This file was deleted.

23 changes: 0 additions & 23 deletions QuantumInfo/ForMathlib.lean
View file
Open in desktop

This file was deleted.

Loading
Loading