OAI/Probability/InvariantIsing/Fields/FieldHeightHessianSign.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Actual mixed-coordinate and quadratic-form signs of the finite scalar Ising height Hessian. The mixed and radial derivative estimates imply the Hessian sign.

  1. lemma OAI.InvariantIsing.fieldHeight_hessian_nonneg_of_coordinate_order line 16
  2. theorem OAI.InvariantIsing.fieldHeight_hessian_mixed_nonneg line 54
  3. theorem OAI.InvariantIsing.fieldHeight_hessian_nonpos line 83