OAI/Probability/FreeIsing/Trees/PathSums.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.summable_path_attenuation line 11
  2. theorem OAI.Problem367.pow_le_factorial_mul_choose line 15
  3. theorem OAI.Problem367.tsum_path_attenuation_le line 28
  4. theorem OAI.Problem367.half_le_one_sub_exp_neg line 49
  5. theorem OAI.Problem367.tsum_path_attenuation_small_le line 60
  6. theorem OAI.Problem367.tsum_linear_path_attenuation_le line 78
  7. theorem OAI.Problem367.tsum_quadratic_path_attenuation_le line 84
  8. theorem OAI.Problem367.sqrt_le_path_affine line 90
  9. theorem OAI.Problem367.summable_sqrt_path_attenuation line 98
  10. theorem OAI.Problem367.tsum_sqrt_path_attenuation_le line 116
  11. theorem OAI.Problem367.summable_superexponential_path line 147
  12. theorem OAI.Problem367.summable_superexponential_rpow_path line 159
  13. theorem OAI.Problem367.exp_neg_le_sq_of_log_cutoff line 166
  14. theorem OAI.Problem367.superexponential_path_absorption line 178