OAI/Probability/InvariantIsing/Fields/FieldHeightClosedSupport.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual finite scalar-field supporting inequality on the closed nonnegative height cone. The proof removes the strict approximation by continuity of both the value and its physical magnetization coefficients.

  1. theorem OAI.InvariantIsing.fieldHeight_support line 15