OAI/Probability/InvariantIsing/Fields/FieldRefinePaths.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The height and physical magnetization paths survive a one-cut refinement.

  1. lemma OAI.InvariantIsing.fieldInsertCut_cell_subset line 15
  2. lemma OAI.InvariantIsing.fieldFunction_insertCut_ae line 70
  3. lemma OAI.InvariantIsing.fieldMagnetizationPath_insertCut_ae line 82