OAI/Probability/InvariantIsing/Haar/HaarPolynomialCurvature.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The curvature inequality for polynomial observables, proved by finite algebra.

  1. def OAI.InvariantIsing.matrixPolynomialDifferential line 13
  2. lemma OAI.InvariantIsing.matrixPolynomial_hessian_bound line 20
  3. theorem OAI.InvariantIsing.matrixPolynomial_curvature line 59

    Source documentation

    With the ordered-plane Laplacian, the Ricci lower bound is N - 2.

    theorem matrixPolynomial_curvature {N : ℕ}
    (p : MatrixPolynomial N) (M : Matrix (Fin N) (Fin N) ℝ) :
    ((N : ℝ)-2)*matrixPolynomialEval M (haarPolynomialGamma p p) ≤
      matrixPolynomialEval M (haarPolynomialLaplacian N (haarPolynomialGamma p p))/2-
        matrixPolynomialEval M (haarPolynomialGamma p (haarPolynomialLaplacian N p)) := by
…

    Mentions: OAI.InvariantIsing.MatrixPolynomial, OAI.InvariantIsing.matrixPolynomialEval, OAI.InvariantIsing.haarPolynomialGamma, OAI.InvariantIsing.haarPolynomialLaplacian