OAI/Probability/FreeIsing/Cavity/Array.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.CavityArray.field line 16
  2. theorem OAI.Problem367.CavityArray.continuous_field line 20
  3. theorem OAI.Problem367.CavityArray.measurable_field line 29
  4. theorem OAI.Problem367.CavityArray.measurable_field_apply line 33
  5. theorem OAI.Problem367.CavityArray.field_reverse line 38
  6. theorem OAI.Problem367.CavityArray.field_spec line 43
  7. theorem OAI.Problem367.CavityArray.field_relabel line 49
  8. theorem OAI.Problem367.CavityArray.field_neg line 54
  9. theorem OAI.Problem367.CavityArray.field_zero line 59
  10. theorem OAI.Problem367.CavityArray.field_site_bound line 65
  11. theorem OAI.Problem367.CavityArray.field_sub_abs_le line 70
  12. abbrev OAI.Problem367.CavityArray.SitePair line 80
  13. def OAI.Problem367.CavityArray.pairRelabel line 82
  14. theorem OAI.Problem367.CavityArray.measurable_pairRelabel line 85
  15. theorem OAI.Problem367.CavityArray.site_sub_identDistrib line 88
  16. theorem OAI.Problem367.CavityArray.integral_field_sub_sq_le line 108