OAI/Probability/FreeIsing/Trees/SubcriticalPathSums.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.regularPathWeight line 13
  2. theorem OAI.Problem367.regularPathWeight_eq line 16
  3. theorem OAI.Problem367.regularPathWeight_nonneg line 23
  4. theorem OAI.Problem367.summable_regularPathWeight_mul_length_sq line 28
  5. def OAI.Problem367.subcriticalPathConstant line 49
  6. theorem OAI.Problem367.subcriticalPathConstant_nonneg line 52
  7. theorem OAI.Problem367.path_noise_drift_le_length_sq line 59
  8. theorem OAI.Problem367.subcritical_noise_drift_bound line 73
  9. theorem OAI.Problem367.eq_zero_of_subcritical_path_estimates line 113