OAI/InformationTheory/AmplitudeDamping/
476 declarations, 0 contain sorry, 0 declared as axioms; 35 files
Files
- BlockFactors.lean 17 declarations
- CapacityAchievability.lean 1 declarations
- CapacityConverse.lean 7 declarations
- Channel.lean 18 declarations
- CodingAsymptotics.lean 10 declarations
- EnsembleBounds.lean 10 declarations
- EntropyContinuity.lean 25 declarations
- FinitePacking.lean 5 declarations
- GramMatrices.lean 17 declarations
- Holevo.lean 4 declarations
- HolevoInformation.lean 9 declarations
- LogDetConvexity.lean 9 declarations
- LogDetEntropy.lean 12 declarations
- Main.lean 3 declarations
- MatrixDifferentiation.lean 14 declarations
- Model.lean 22 declarations
- Naimark.lean 12 declarations
- OutputConvexity.lean 27 declarations
- OutputEntropy.lean 11 declarations
- PhaseCoding.lean 10 declarations
- PhaseProducts.lean 22 declarations
- PhaseStates.lean 9 declarations
- Pinching.lean 12 declarations
- PureRecursion.lean 36 declarations
- ScalarDeficit.lean 23 declarations
- SequentialDecoder.lean 10 declarations
- SequentialMatrices.lean 10 declarations
- SequentialProjections.lean 1 declarations
- SpectralEntropy.lean 10 declarations
- StateEntropy.lean 16 declarations
- TensorEntropy.lean 8 declarations
- ThermalEntropy.lean 10 declarations
- TypicalProjectors.lean 24 declarations
- TypicalSets.lean 20 declarations
- ZeroBlockEntropy.lean 22 declarations