OAI/Probability/SKGap/Localization/GridSteps.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGap.GaussianHistory.gridSteps line 11
2. def OAI.SKGap.GaussianHistory.gridStep line 12
3. lemma OAI.SKGap.GaussianHistory.gridSteps_pos line 14
4. lemma OAI.SKGap.GaussianHistory.gridStep_nonneg line 15
5. lemma OAI.SKGap.GaussianHistory.grid_total line 18
6. lemma OAI.SKGap.GaussianHistory.gridStep_eq line 21
7. lemma OAI.SKGap.GaussianHistory.inv_succ_tendsto line 24
8. lemma OAI.SKGap.GaussianHistory.gridStep_tendsto line 28
9. lemma OAI.SKGap.GaussianHistory.nat_mul_gridStep_tendsto line 34
10. lemma OAI.SKGap.GaussianHistory.nat_sq_mul_gridStep_tendsto line 44
11. lemma OAI.SKGap.GaussianHistory.nat_inv_tendsto line 54
12. lemma OAI.SKGap.GaussianHistory.sqrt_div_nat_tendsto line 57
13. lemma OAI.SKGap.GaussianHistory.localizationLoss_tendsto line 68
14. lemma OAI.SKGap.GaussianHistory.localizationCost_tendsto line 88
15. theorem OAI.SKGap.GaussianHistory.localization_numeric_choice line 97
16. lemma OAI.SKGap.GaussianHistory.nat_pow_exp_tendsto line 119
17. lemma OAI.SKGap.GaussianHistory.grid_polynomial_exp_tendsto line 131
18. lemma OAI.SKGap.GaussianHistory.grid_exp_absorb line 142
19. lemma OAI.SKGap.GaussianHistory.constant_exp_absorb line 153