-
Notifications
You must be signed in to change notification settings - Fork 193
Expand file tree
/
Copy pathQuantumInfo.lean
More file actions
87 lines (86 loc) · 4.5 KB
/
Copy pathQuantumInfo.lean
File metadata and controls
87 lines (86 loc) · 4.5 KB
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
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
/-
Copyright (c) 2025 Alex Meiburg. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Alex Meiburg
-/
module
public import QuantumInfo.Capacity.Capacity
public import QuantumInfo.Capacity.Capacity_doc
public import QuantumInfo.Channels.Bundled
public import QuantumInfo.Channels.CPTP
public import QuantumInfo.Channels.DegradableOrder
public import QuantumInfo.Channels.Dual
public import QuantumInfo.Channels.MatrixMap
public import QuantumInfo.Channels.Pinching
public import QuantumInfo.Channels.Unbundled
public import QuantumInfo.ClassicalInfo.Capacity
public import QuantumInfo.ClassicalInfo.Channel
public import QuantumInfo.ClassicalInfo.Distribution
public import QuantumInfo.ClassicalInfo.Entropy
public import QuantumInfo.ClassicalInfo.ForMathlib.Analysis.SpecialFunctions.Log.NegMulLog
public import QuantumInfo.ClassicalInfo.Prob
public import QuantumInfo.Entropy.DPI
public import QuantumInfo.Entropy.Relative
public import QuantumInfo.Entropy.SSA
public import QuantumInfo.Entropy.VonNeumann
public import QuantumInfo.ForMathlib.ComplexLaplaceTransform
public import QuantumInfo.ForMathlib.ContinuousLinearMap
public import QuantumInfo.ForMathlib.ContinuousSup
public import QuantumInfo.ForMathlib.Filter
public import QuantumInfo.ForMathlib.HayataGroup.TraceInequality.BlockDiagonal
public import QuantumInfo.ForMathlib.HayataGroup.TraceInequality.GeneralizedPerspectiveFunction
public import QuantumInfo.ForMathlib.HayataGroup.TraceInequality.HilbertSchmidtOperatorSpace
public import QuantumInfo.ForMathlib.HayataGroup.TraceInequality.JensenOperatorInequality
public import QuantumInfo.ForMathlib.HayataGroup.TraceInequality.JensenOperatorInequalityIImpIV
public import QuantumInfo.ForMathlib.HayataGroup.TraceInequality.JensenOperatorInequalityIVtoV
public import QuantumInfo.ForMathlib.HayataGroup.TraceInequality.LiebAndoTrace
public import QuantumInfo.ForMathlib.HayataGroup.TraceInequality.LownerHeinzCore
public import QuantumInfo.ForMathlib.HayataGroup.TraceInequality.LownerHeinzTheorem
public import QuantumInfo.ForMathlib.HayataGroup.TraceInequality.OperatorGeometricMean
public import QuantumInfo.ForMathlib.HermitianMat
public import QuantumInfo.ForMathlib.HermitianMat.Basic
public import QuantumInfo.ForMathlib.HermitianMat.CFC
public import QuantumInfo.ForMathlib.HermitianMat.CompoundMatrix
public import QuantumInfo.ForMathlib.HermitianMat.Inner
public import QuantumInfo.ForMathlib.HermitianMat.Jordan
public import QuantumInfo.ForMathlib.HermitianMat.LiebConcavity
public import QuantumInfo.ForMathlib.HermitianMat.LogExp
public import QuantumInfo.ForMathlib.HermitianMat.NonSingular
public import QuantumInfo.ForMathlib.HermitianMat.Order
public import QuantumInfo.ForMathlib.HermitianMat.Peierls
public import QuantumInfo.ForMathlib.HermitianMat.Proj
public import QuantumInfo.ForMathlib.HermitianMat.Reindex
public import QuantumInfo.ForMathlib.HermitianMat.Rpow
public import QuantumInfo.ForMathlib.HermitianMat.Schatten
public import QuantumInfo.ForMathlib.HermitianMat.Sqrt
public import QuantumInfo.ForMathlib.HermitianMat.Trace
public import QuantumInfo.ForMathlib.HermitianMat.Unitary
public import QuantumInfo.ForMathlib.IsMaximalSelfAdjoint
public import QuantumInfo.ForMathlib.Isometry
public import QuantumInfo.ForMathlib.LimSupInf
public import QuantumInfo.ForMathlib.LinearEquiv
public import QuantumInfo.ForMathlib.Majorization
public import QuantumInfo.ForMathlib.Matrix
public import QuantumInfo.ForMathlib.MatrixNorm.TraceNorm
public import QuantumInfo.ForMathlib.Minimax
public import QuantumInfo.ForMathlib.Misc
public import QuantumInfo.ForMathlib.SionMinimax
public import QuantumInfo.ForMathlib.Superadditive
public import QuantumInfo.ForMathlib.Tactic.Commutes
public import QuantumInfo.ForMathlib.Tactic.Commutes.Attribute
public import QuantumInfo.ForMathlib.ULift
public import QuantumInfo.ForMathlib.Unitary
public import QuantumInfo.Measurements.POVM
public import QuantumInfo.Operators.Unitary
public import QuantumInfo.ResourceTheory.FreeState
public import QuantumInfo.ResourceTheory.HypothesisTesting
public import QuantumInfo.ResourceTheory.SteinsLemma
public import QuantumInfo.States.Ensemble
public import QuantumInfo.States.Entanglement
public import QuantumInfo.States.Mixed.Fidelity
public import QuantumInfo.States.Mixed.MState
public import QuantumInfo.States.Mixed.TraceDistance
public import QuantumInfo.States.Pure.BargmannInvariant
public import QuantumInfo.States.Pure.BlochSphere
public import QuantumInfo.States.Pure.Braket
public import QuantumInfo.States.Pure.Qubit