OAI/Combinatorics/SumProduct/Alignment/CubeRationalization01.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CubeRationalization.bound line 27
2. lemma OAI.CubeRationalization.one_le_bound line 30
3. theorem OAI.CubeRationalization.peel_coefficients line 35
4. theorem OAI.CubeRoundingScales.eventual_small line 134
5. lemma OAI.CubeArithmetic.time_set line 184
6. lemma OAI.CubeArithmetic.block_prime_slopes line 197
7. lemma OAI.CubeArithmetic.block_time_bounds line 213
8. def OAI.CubeSplitProducer.GoodCharacter line 248
9. def OAI.CubeSplitProducer.Split line 251
10. theorem OAI.CubeSplitProducer.split_producer line 267