OAI/Probability/InvariantIsing/Fields/FieldRefineIncrements.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A one-cut refinement inserts exactly one zero covariance increment.

  1. lemma OAI.InvariantIsing.fieldIncrement_insertCut_at line 13
  2. lemma OAI.InvariantIsing.fieldIncrement_insertCut_below line 30
  3. lemma OAI.InvariantIsing.fieldIncrement_insertCut_above line 51
  4. def OAI.InvariantIsing.fieldNNIncrement line 75
  5. lemma OAI.InvariantIsing.fieldNNIncrement_eq_of_real line 78
  6. lemma OAI.InvariantIsing.fieldNNIncrement_insertCut_at line 86
  7. lemma OAI.InvariantIsing.fieldAllIncrements_insertCut line 97
  8. lemma OAI.InvariantIsing.fieldValue_insertCut line 124