OAI/Probability/FreeIsing/Estimates/ComponentPairCount.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.componentPairWeight line 9
  2. def OAI.Problem367.componentPairSum line 15
  3. theorem OAI.Problem367.tail_length line 18
  4. theorem OAI.Problem367.componentPairSum_zero_left line 21
  5. theorem OAI.Problem367.componentPairSum_zero_right line 29
  6. theorem OAI.Problem367.sum_diagonal_constant line 38
  7. theorem OAI.Problem367.componentPairSum_succ line 52
  8. theorem OAI.Problem367.componentPairSum_critical line 93
  9. theorem OAI.Problem367.componentPairSum_critical_le line 128
  10. theorem OAI.Problem367.sum_componentPairSum_critical_le line 140
  11. def OAI.Problem367.componentWordDistance line 156
  12. theorem OAI.Problem367.componentPairWeight_eq_pow_distance line 162
  13. theorem OAI.Problem367.componentPairWeight_eq_weighted_correlation line 191
  14. theorem OAI.Problem367.sum_component_weighted_correlation_critical line 197
  15. theorem OAI.Problem367.sum_component_weighted_correlation_critical_le line 205
  16. theorem OAI.Problem367.sum_component_radial_sq_critical line 214
  17. theorem OAI.Problem367.sum_component_radial_sq_levels_critical line 221