OAI/Combinatorics/SharpRamsey/Exposure/
253 declarations, 0 contain sorry, 0 declared as axioms; 25 files
Files
- DivergenceMap.lean 46 declarations
- DominatedCoupling.lean 3 declarations
- DominatedMixture.lean 4 declarations
- ExposureAverages.lean 11 declarations
- ExposureBudget.lean 43 declarations
- ExposureContexts.lean 9 declarations
- ExposureGood.lean 6 declarations
- ExposureMixture.lean 11 declarations
- ExposureModel.lean 12 declarations
- ExposureRealization.lean 6 declarations
- ExposureSupport.lean 4 declarations
- FreshBlockBudgets.lean 5 declarations
- FreshBlockCollision.lean 2 declarations
- HighRankMixture.lean 2 declarations
- MixtureRealization.lean 6 declarations
- PreparedMixture.lean 7 declarations
- RemainingEmbedding.lean 30 declarations
- RestrictionBudget.lean 1 declarations
- RestrictionGeometry.lean 4 declarations
- SourceCoupling.lean 5 declarations
- SourceExposure.lean 6 declarations
- SourceZero.lean 3 declarations
- StreamTransport.lean 5 declarations
- SupportMixtures.lean 12 declarations
- ZeroExposure.lean 10 declarations