OAI/Probability/FreeIsing/Spectral/KoopmanInvolutions.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem367.koopmanL2 line 14
2. theorem OAI.Problem367.koopmanL2_norm line 18
3. theorem OAI.Problem367.koopmanL2_involutive line 22
4. theorem OAI.Problem367.koopmanL2_selfAdjoint line 30
5. def OAI.Problem367.koopmanAverage line 39
6. theorem OAI.Problem367.koopmanAverage_selfAdjoint line 44
7. theorem OAI.Problem367.koopmanAverage_norm_le_one line 53
8. theorem OAI.Problem367.koopmanL2_const line 71
9. theorem OAI.Problem367.inner_const_one_eq_integral line 77
10. def OAI.Problem367.centeredL2 line 85
11. theorem OAI.Problem367.mem_centeredL2_iff line 88
12. instance OAI.Problem367.centeredL2Complete line 93
13. theorem OAI.Problem367.koopmanL2_integral line 96
14. theorem OAI.Problem367.koopmanL2_preserves_centered line 105
15. theorem OAI.Problem367.koopmanAverage_preserves_centered line 112
16. def OAI.Problem367.centeredKoopmanAverage line 122
17. theorem OAI.Problem367.centeredKoopmanAverage_apply_coe line 128
18. theorem OAI.Problem367.centeredKoopmanAverage_selfAdjoint line 133
19. theorem OAI.Problem367.centeredKoopmanAverage_norm_le_one line 141