OAI/InformationTheory/SoftChannel/
348 declarations, 0 contain sorry, 0 declared as axioms; 28 files
Files
- Canonical.lean 74 declarations
- Comparison.lean 3 declarations
- Contraction.lean 14 declarations
- CurvatureBounds.lean 3 declarations
- CurvatureCertificates.lean 18 declarations
- EndpointLimits.lean 1 declarations
- HighReserve.lean 14 declarations
- JensenGaps.lean 10 declarations
- Joining.lean 6 declarations
- LRegularity.lean 3 declarations
- Main.lean 12 declarations
- Model.lean 34 declarations
- NormalizedPair.lean 1 declarations
- PairEntropy.lean 4 declarations
- Payment.lean 36 declarations
- PerspectiveCalculus.lean 1 declarations
- PerspectiveInequality.lean 1 declarations
- PerspectiveLogTrapezoid.lean 5 declarations
- Production.lean 10 declarations
- RateSlope.lean 9 declarations
- RateWindow.lean 3 declarations
- Rearrangement.lean 1 declarations
- SemigroupFlow.lean 2 declarations
- SoftInformation.lean 24 declarations
- SoftReserve.lean 13 declarations
- Thinning.lean 17 declarations
- Wall.lean 23 declarations
- Window.lean 6 declarations