OAI/Probability/FreeIsing/Trees/LawSpectral.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.TreeLawKoopman.reflection line 18
  2. theorem OAI.Problem367.TreeLawKoopman.reflection_involutive line 22
  3. def OAI.Problem367.TreeLawKoopman.average line 29
  4. theorem OAI.Problem367.TreeLawKoopman.average_selfAdjoint line 32
  5. def OAI.Problem367.TreeLawKoopman.generatorOperator line 35
  6. theorem OAI.Problem367.TreeLawKoopman.generatorOperator_sq line 38
  7. def OAI.Problem367.TreeLawKoopman.wordRelabel line 44
  8. theorem OAI.Problem367.TreeLawKoopman.list_koopman_eq line 48
  9. theorem OAI.Problem367.TreeLawKoopman.wordOperator_eq line 67
  10. theorem OAI.Problem367.TreeLawKoopman.operatorAverage_eq line 72
  11. def OAI.Problem367.TreeLawKoopman.centeredAverage line 78
  12. theorem OAI.Problem367.TreeLawKoopman.centeredAverage_selfAdjoint line 82
  13. theorem OAI.Problem367.TreeLawKoopman.centeredAverage_apply_coe line 85
  14. theorem OAI.Problem367.TreeLawKoopman.centeredAverage_pow_apply_coe line 88
  15. def OAI.Problem367.TreeLawKoopman.LocalCriticalDecay line 96
  16. theorem OAI.Problem367.TreeLawKoopman.local_average_power_bound line 106
  17. theorem OAI.Problem367.TreeLawKoopman.centeredAverage_norm_le line 130