OAI/Probability/FreeIsing/Spectral/ColoredKoopman.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.ColoredEdgeLifts.koopmanEquiv line 11
  2. theorem OAI.Problem367.ColoredEdgeLifts.koopmanEquiv_apply line 16
  3. theorem OAI.Problem367.ColoredEdgeLifts.koopmanEquiv_involutive line 20
  4. def OAI.Problem367.ColoredEdgeLifts.centeredKoopmanIsometry line 26
  5. theorem OAI.Problem367.ColoredEdgeLifts.centeredKoopmanIsometry_apply_coe line 32
  6. theorem OAI.Problem367.ColoredEdgeLifts.centeredKoopmanIsometry_involutive line 37
  7. def OAI.Problem367.ColoredEdgeLifts.centeredKoopmanEquiv line 44
  8. theorem OAI.Problem367.ColoredEdgeLifts.centeredKoopmanEquiv_apply_coe line 49
  9. theorem OAI.Problem367.ColoredEdgeLifts.centeredKoopmanEquiv_involutive line 54
  10. theorem OAI.Problem367.ColoredEdgeLifts.neighborAverage_centeredKoopmanEquiv line 59