OAI/Probability/InvariantIsing/Haar/HaarHeatConstants.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Preservation of constants by the constructed polynomial heat flow.

  1. lemma OAI.InvariantIsing.continuousLinearMap_exp_apply_of_zero line 11
  2. lemma OAI.InvariantIsing.haarPolynomialHeat_eq_of_laplacian_zero line 30
  3. lemma OAI.InvariantIsing.haarPolynomialLaplacian_one line 43
  4. lemma OAI.InvariantIsing.haarPolynomialHeat_one line 48