OAI/InformationTheory/BooleanNoise/
743 declarations, 0 contain sorry, 0 declared as axioms; 41 files
Files
- ArtanhBounds.lean 3 declarations
- Attainment.lean 22 declarations
- Basic.lean 19 declarations
- Comparison.lean 54 declarations
- ComparisonEstimates.lean 12 declarations
- ConcavityAcrossJoin.lean 2 declarations
- CubeSplits.lean 33 declarations
- CubeVariance.lean 17 declarations
- CurvatureBounds.lean 15 declarations
- CurvatureCertificates.lean 33 declarations
- EndpointLimits.lean 8 declarations
- EntropyBounds.lean 11 declarations
- EntropyScalars.lean 26 declarations
- EntropySeries.lean 11 declarations
- FiniteDistribution.lean 14 declarations
- FiniteInformation.lean 2 declarations
- FiniteNoise.lean 41 declarations
- GeneralDissipation.lean 8 declarations
- InformationIdentity.lean 11 declarations
- InverseRegularity.lean 29 declarations
- InverseScalars.lean 41 declarations
- JensenGaps.lean 36 declarations
- KRegularity.lean 24 declarations
- LRegularity.lean 15 declarations
- LShape.lean 7 declarations
- LambdaScalars.lean 9 declarations
- LargeCurvature.lean 5 declarations
- Main.lean 5 declarations
- MediumCurvature.lean 9 declarations
- Model.lean 15 declarations
- MonotoneDissipation.lean 25 declarations
- NormalizedPair.lean 24 declarations
- PairEntropy.lean 36 declarations
- PerspectiveCalculus.lean 8 declarations
- PerspectiveInequality.lean 29 declarations
- PerspectiveJensen.lean 2 declarations
- PerspectiveLogTrapezoid.lean 6 declarations
- Rearrangement.lean 48 declarations
- SemigroupFlow.lean 23 declarations
- SmallCurvatureAux.lean 2 declarations
- Statement.lean 3 declarations