OAI/Probability/FreeIsing/Estimates/RadialRepresentation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem367.RadialWalk.wordOperator line 11
2. theorem OAI.Problem367.RadialWalk.wordOperator_step line 14
3. def OAI.Problem367.RadialWalk.operatorAverage line 23
4. theorem OAI.Problem367.RadialWalk.operatorAverage_apply line 26
5. theorem OAI.Problem367.RadialWalk.vectorAverage_wordOperator line 30
6. theorem OAI.Problem367.RadialWalk.iterate_vectorAverage_wordOperator line 37
7. theorem OAI.Problem367.RadialWalk.matrix_coefficient_power_bound line 49