OAI/Probability/InvariantIsing/Fields/FieldHessianAlgebra.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The finite-dimensional Hessian argument in fld:concavity: a symmetric matrix with nonpositive off-diagonal entries and nonnegative row sums is nonnegative as a quadratic form, also after positive scaling.

  1. lemma OAI.InvariantIsing.field_quadratic_nonneg_of_row_sums line 14
  2. theorem OAI.InvariantIsing.field_quadratic_nonneg_of_positive_scaling line 58