OAI/Probability/InvariantIsing/Haar/HaarHeatGradient.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Exponential squared-gradient decay for the actual orthogonal polynomial heat flow.

  1. theorem OAI.InvariantIsing.haarPolynomialHeat_gradient_bound line 14