OAI/Probability/LogConcave/LowerBounds/HardEigenOutput.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.LowerBound.spectrum_iterate_apply line 27
2. lemma OAI.LogConcaveSampling.LowerBound.orbitHull_in_krylov line 37
3. lemma OAI.LogConcaveSampling.LowerBound.linearReply_eq_quadratic line 52
4. lemma OAI.LogConcaveSampling.LowerBound.linearHistory_eq_quadratic line 64
5. def OAI.LogConcaveSampling.LowerBound.hardEigenOutput line 71
6. lemma OAI.LogConcaveSampling.LowerBound.measurable_hardEigenOutput line 75
7. theorem OAI.LogConcaveSampling.LowerBound.hard_algorithm_separation line 90
8. lemma OAI.LogConcaveSampling.LowerBound.quadratic_gibbs_eigenframe line 127
9. lemma OAI.LogConcaveSampling.LowerBound.hardEigenOutput_tv line 134
10. theorem OAI.LogConcaveSampling.LowerBound.canSample_target_separation_bound line 149
11. lemma OAI.LogConcaveSampling.LowerBound.spectralDecay_bounds line 174
12. theorem OAI.LogConcaveSampling.LowerBound.target_mean_lower line 180
13. lemma OAI.LogConcaveSampling.LowerBound.lower_denominator line 221
14. lemma OAI.LogConcaveSampling.LowerBound.polynomial_threshold_le_pow line 227
15. lemma OAI.LogConcaveSampling.LowerBound.sqrt_exponential_lower line 245
16. lemma OAI.LogConcaveSampling.LowerBound.target_large_mean line 254
17. lemma OAI.LogConcaveSampling.LowerBound.exponential_dimension_bounds line 284
18. lemma OAI.LogConcaveSampling.LowerBound.exponential_tolerance line 291
19. theorem OAI.LogConcaveSampling.LowerBound.target_event_large line 306
20. theorem OAI.LogConcaveSampling.LowerBound.not_canSample_exponential line 338
21. lemma OAI.LogConcaveSampling.LowerBound.exponential_of_small_log line 345
22. theorem OAI.LogConcaveSampling.LowerBound.source_logarithmic_lower line 364