OAI/Analysis/FreeEntropy/BlockGaussianQuantitative.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteEntropySeparation.two_pow_le_exp line 10
2. theorem OAI.FiniteEntropySeparation.blockEvent_gaussian_four line 13
3. def OAI.FiniteEntropySeparation.chosenP line 73
4. def OAI.FiniteEntropySeparation.chosenTime line 74
5. instance OAI.FiniteEntropySeparation.chosenP_neZero line 75
6. theorem OAI.FiniteEntropySeparation.chosenP_ge_two line 76
7. theorem OAI.FiniteEntropySeparation.chosenTime_pos line 77
8. theorem OAI.FiniteEntropySeparation.chosen_time_noise_budget line 78
9. theorem OAI.FiniteEntropySeparation.chosen_gaussian_block line 79