physlib/QuantumInfo.lean at master · leanprover-community/physlib · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
/-
Copyright (c) 2025 Alex Meiburg. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Alex Meiburg
-/
--Mathlib imports
module

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.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.Capacity.Capacity_doc

--Classical information theory
-- import QuantumInfo.ClassicalInfo.Capacity
-- import QuantumInfo.ClassicalInfo.Channel
public import QuantumInfo.ClassicalInfo.Distribution
public import QuantumInfo.ClassicalInfo.Entropy
public import QuantumInfo.ClassicalInfo.Prob