UniformHaarMeanTail.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform centered Haar tails for bounded Lipschitz observables. The threshold is independent of the particular observable and of its additive normalization.

theorem OAI.InvariantIsing.uniform_bounded_haar_mean_tail line 12