OAI/Probability/InvariantIsing/Haar/HaarHeatMixing.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Convergence of the actual orthogonal polynomial heat flow to its Haar mean.

  1. theorem OAI.InvariantIsing.haarPolynomialHeat_tendsto_mean line 13