OAI/Probability/FreeIsing/Trees/WordAction.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.TreeKoopman.wordAut line 12
  2. theorem OAI.Problem367.TreeKoopman.wordAut_root line 16
  3. def OAI.Problem367.TreeKoopman.wordRelabel line 30
  4. theorem OAI.Problem367.TreeKoopman.wordRelabel_measurePreserving line 34
  5. theorem OAI.Problem367.TreeKoopman.wordRelabel_nil line 38
  6. theorem OAI.Problem367.TreeKoopman.wordRelabel_cons line 40
  7. def OAI.Problem367.TreeKoopman.generatorOperator line 43
  8. theorem OAI.Problem367.TreeKoopman.generatorOperator_sq line 47
  9. theorem OAI.Problem367.TreeKoopman.list_koopman_eq line 53
  10. theorem OAI.Problem367.TreeKoopman.wordOperator_eq line 72
  11. theorem OAI.Problem367.TreeKoopman.wordOperator_norm line 77
  12. theorem OAI.Problem367.TreeKoopman.operatorAverage_eq line 82
  13. theorem OAI.Problem367.TreeKoopman.wordOperator_toLp_root line 86