OAI/GroupTheory/SimpleAmenable/RandomFields/CovarianceLimit.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SimpleAmenable.sourceFlagMatrix line 18
2. theorem OAI.SimpleAmenable.sourceFlagMatrix_covariance line 24
3. def OAI.SimpleAmenable.sourceActiveSites line 50
4. theorem OAI.SimpleAmenable.sourceFlagMatrix_support line 54
5. theorem OAI.SimpleAmenable.sourceActiveSites_card line 75
6. theorem OAI.SimpleAmenable.sourceDyadicWeight_eventually_sq_le_one line 90
7. theorem OAI.SimpleAmenable.sourceFlagMatrix_concentration line 96