OAI/Probability/InvariantIsing/Fields/FieldCommonRefinement.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Finite common refinements, built only by duplicating constant-height cells.

  1. def OAI.InvariantIsing.fieldCutSet line 14
  2. lemma OAI.InvariantIsing.mem_fieldCutSet line 18
  3. lemma OAI.InvariantIsing.fieldCutSet_bounds line 23
  4. lemma OAI.InvariantIsing.fieldCutSet_insertCut line 30
  5. inductive OAI.InvariantIsing.FieldRefines line 41
  6. lemma OAI.InvariantIsing.FieldRefines.trans line 47
  7. lemma OAI.InvariantIsing.FieldRefines.value line 53
  8. lemma OAI.InvariantIsing.FieldRefines.field_ae line 59
  9. lemma OAI.InvariantIsing.FieldRefines.magnetization_ae line 65
  10. lemma OAI.InvariantIsing.FieldRefines.pairing line 72
  11. lemma OAI.InvariantIsing.field_exists_refinement line 78
  12. lemma OAI.InvariantIsing.field_cutList_eq_of_set_eq line 122
  13. lemma OAI.InvariantIsing.field_common_refinement line 133