OAI/NumberTheory/GaussianMoat/BatchParameters.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.GaussianMoat.one_step_coverage line 8
2. lemma OAI.GaussianMoat.package_list_arithmetic line 68
3. lemma OAI.GaussianMoat.package_rate_arithmetic line 111
4. lemma OAI.GaussianMoat.eventually_poly_le_exp_linear line 135
5. lemma OAI.GaussianMoat.eventually_mul_exp_le_exp line 143
6. def OAI.GaussianMoat.batchWordLength line 154
7. def OAI.GaussianMoat.packageRepetitions line 155
8. lemma OAI.GaussianMoat.batchWordLength_pos line 158
9. lemma OAI.GaussianMoat.batchWordLength_dvd line 161
10. lemma OAI.GaussianMoat.batchWordLength_log line 164
11. lemma OAI.GaussianMoat.batchWordLength_le_scale line 177
12. theorem OAI.GaussianMoat.eventually_integer_batch_bounds line 183