OAI/GroupTheory/SimpleAmenable/RandomFields/FiniteFieldConcentration.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.SimpleAmenable.subgaussian_parameter_monoline 15 - theorem
OAI.SimpleAmenable.finite_weighted_noise_tailline 22 - theorem
OAI.SimpleAmenable.finite_matrix_noise_tailline 57