OAI/Probability/InvariantIsing/Haar/HaarExponentialGradient.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform logarithmic-gradient bounds for positive exponential truncations.

  1. lemma OAI.InvariantIsing.haarExpPolynomial_gamma line 12
  2. lemma OAI.InvariantIsing.haarExpPolynomial_positive line 22
  3. lemma OAI.InvariantIsing.haarExpPolynomial_log_gradient_bound line 28