OAI/Probability/InvariantIsing/Haar/HaarHeatTestLimit.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Continuous tests of the polynomial heat flow and their Haar limits.

  1. lemma OAI.InvariantIsing.haarPolynomialHeat_test_bound line 11
  2. theorem OAI.InvariantIsing.haarPolynomialHeat_test_tendsto_mean line 24
  3. theorem OAI.InvariantIsing.continuousOn_haarPolynomialHeat_test_integral line 44