OAI/Probability/FreeIsing/Estimates/FiniteIsingSplit.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.FiniteIsingSplit.splitEquiv line 17
  2. lemma OAI.Problem367.FiniteIsingSplit.splitEquiv_fst line 35
  3. lemma OAI.Problem367.FiniteIsingSplit.splitEquiv_snd line 40
  4. def OAI.Problem367.FiniteIsingSplit.observedEnergy line 47
  5. lemma OAI.Problem367.FiniteIsingSplit.inducedEdges_endpoints line 52
  6. lemma OAI.Problem367.FiniteIsingSplit.observedEnergy_restrict line 58
  7. theorem OAI.Problem367.FiniteIsingSplit.observedEnergy_split_restrict line 73
  8. theorem OAI.Problem367.FiniteIsingSplit.observedEnergy_split line 98
  9. def OAI.Problem367.FiniteIsingSplit.mean line 121
  10. lemma OAI.Problem367.FiniteIsingSplit.mean_eq_fieldMean line 125
  11. theorem OAI.Problem367.FiniteIsingSplit.mean_union_fst line 132
  12. theorem OAI.Problem367.FiniteIsingSplit.mean_union_snd line 149
  13. lemma OAI.Problem367.FiniteIsingSplit.mean_mem_Ioo line 171
  14. def OAI.Problem367.FiniteIsingSplit.field line 181
  15. theorem OAI.Problem367.FiniteIsingSplit.field_union_fst line 184
  16. theorem OAI.Problem367.FiniteIsingSplit.field_union_snd line 197
  17. theorem OAI.Problem367.FiniteIsingSplit.cavityFromSites_eq_component_fields line 213