OAI/Probability/InvariantIsing/Haar/HaarGammaCalculus.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

First-order product and square-gradient identities for the rotation carré du champ.

  1. lemma OAI.InvariantIsing.haarPolynomialGamma_mul line 11
  2. lemma OAI.InvariantIsing.haarPolynomialGamma_sq line 21
  3. lemma OAI.InvariantIsing.haarPolynomialGamma_sub line 26
  4. lemma OAI.InvariantIsing.haarPolynomialGamma_smul line 30
  5. lemma OAI.InvariantIsing.haarPolynomialDerivation_gamma_sq line 35