OAI/Probability/InvariantIsing/Haar/HaarHessianBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The antisymmetric part of a finite Hessian controls the curvature term.

  1. theorem OAI.InvariantIsing.sum_antisymmetric_square_le line 10