OAI/Probability/InvariantIsing/Haar/HaarExponentialMomentBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Gaussian exponential-moment bounds for nonnegative polynomial observables.

  1. lemma OAI.InvariantIsing.haarPolynomialGamma_scaled_value line 11
  2. theorem OAI.InvariantIsing.haarPolynomialMoment_log_bound_of_nonneg line 23