OAI/Probability/MemoryPrecision/StreamArithmetic.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MemoryPrecision.StreamConstant line 18
2. lemma OAI.MemoryPrecision.streamConstant_pos line 19
3. lemma OAI.MemoryPrecision.blockCount_antitone line 24
4. lemma OAI.MemoryPrecision.power_le_exp line 29
5. lemma OAI.MemoryPrecision.stream_root_exp line 34
6. lemma OAI.MemoryPrecision.stream_step_exp line 62
7. lemma OAI.MemoryPrecision.stream_step_one line 71
8. lemma OAI.MemoryPrecision.stream_exponent_bound line 78
9. lemma OAI.MemoryPrecision.stream_full_factor line 98