OAI/Combinatorics/Progressions/Sampling/PreparedCanonicalPaddedSamplerData.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Erdos3.RankPreparationFamily.CanonicalSamplerMeasures line 15
2. def OAI.Erdos3.RankPreparationFamily.PreparedHeights.canonicalSamplerMeasures line 34
3. def OAI.Erdos3.RankPreparationFamily.PreparedHeights.paddedCanonicalSamplerMeasures line 76
4. structure OAI.Erdos3.RankPreparationFamily.CanonicalSamplerData line 95
5. def OAI.Erdos3.RankPreparationFamily.PreparedHeights.canonicalPaddedSamplerData line 120