OAI/Probability/InvariantIsing/Haar/HaarCorrectedHessian.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The curvature estimate survives a symmetric gradient-square correction.

  1. lemma OAI.InvariantIsing.matrixPolynomial_corrected_hessian_bound line 11