OAI/Probability/FreeIsing/Cavity/MomentRecurrence.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.critical_cavity_moment_step line 10
2. theorem OAI.Problem367.critical_all_moments_of_independent_recursion line 73
3. theorem OAI.Problem367.exists_critical_all_moments_bound line 98
4. theorem OAI.Problem367.exists_uniform_critical_all_moments_bound line 130
5. theorem OAI.Problem367.exists_uniform_critical_moment_and_tail_bound line 168
6. theorem OAI.Problem367.exists_small_time_for_moment_tail line 203