OAI/Probability/InvariantIsing/Haar/HaarPolynomialMomentShift.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Removing the positivity normalization from polynomial exponential-moment bounds.

  1. lemma OAI.InvariantIsing.haarPolynomialDerivation_C line 10
  2. lemma OAI.InvariantIsing.haarPolynomialGamma_add_C line 14
  3. lemma OAI.InvariantIsing.haarPolynomialMoment_add_C line 18
  4. theorem OAI.InvariantIsing.haarPolynomialMoment_log_bound line 30