OAI/Probability/InvariantIsing/Fields/FieldMagnetizationTies.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A pointwise plateau criterion for the chosen global representative.

  1. lemma OAI.InvariantIsing.fieldMagnetizationPath_eq_of_index_height_eq line 11