OAI/Probability/InvariantIsing/Haar/HaarPolynomialGamma.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.InvariantIsing.derivation_double_product line 11
2. def OAI.InvariantIsing.haarPolynomialGamma line 17
3. lemma OAI.InvariantIsing.haarPolynomialLaplacian_mul line 21
4. lemma OAI.InvariantIsing.haarPolynomialLaplacian_sq line 27
5. theorem OAI.InvariantIsing.haarPolynomial_bochner_identity line 34

   Source documentation

   The exact Bochner identity before the nonnegative Hessian estimate.

   theorem haarPolynomial_bochner_identity {N : ℕ} (p : MatrixPolynomial N) :
       haarPolynomialLaplacian N (haarPolynomialGamma p p) =
         2*(haarPolynomialGamma p (haarPolynomialLaplacian N p)+
           ∑ i, ∑ j, ∑ k, ∑ l,
             (matrixPolynomialDerivation (planeGenerator k l)
               (matrixPolynomialDerivation (planeGenerator i j) p))^2) := by
   …

   Mentions: OAI.InvariantIsing.MatrixPolynomial, OAI.InvariantIsing.haarPolynomialLaplacian, OAI.InvariantIsing.haarPolynomialGamma, OAI.InvariantIsing.matrixPolynomialDerivation, OAI.InvariantIsing.planeGenerator