OAI/Probability/InvariantIsing/Haar/HaarLipschitzGradient.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A Frobenius-Lipschitz polynomial has dimension-free carré-du-champ control.

  1. theorem OAI.InvariantIsing.haarPolynomial_direction_le_lipschitz line 15
  2. theorem OAI.InvariantIsing.haarPolynomial_gamma_le_lipschitz line 29