OAI/GroupTheory/SimpleAmenable/RandomFields/AveragingUniformCovariance.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.flagAveragingMatrix_uniform_difference line 15
  2. theorem OAI.SimpleAmenable.pair_card_of_row_bound line 55
  3. theorem OAI.SimpleAmenable.flagAveragingMatrix_support_card line 68
  4. theorem OAI.SimpleAmenable.flagAveragingMatrix_support_quadratic line 94
  5. theorem OAI.SimpleAmenable.flagAveragingMatrix_difference_support line 111
  6. theorem OAI.SimpleAmenable.finite_correlation_bound line 144
  7. theorem OAI.SimpleAmenable.finite_half_geometric_sum line 168
  8. theorem OAI.SimpleAmenable.finite_dyadic_row line 182
  9. theorem OAI.SimpleAmenable.finite_dyadic_energy line 208