OAI/Dynamics/MultipleMixing/Tail.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Rokhlin.fullShift line 15
  2. lemma OAI.Rokhlin.fullShift_iterate line 24
  3. def OAI.Rokhlin.symbolicCode line 36
  4. lemma OAI.Rokhlin.symbolicCode_measurable line 40
  5. lemma OAI.Rokhlin.symbolicCode_time line 44
  6. lemma OAI.Rokhlin.symbolicShift_preserving line 51
  7. lemma OAI.Rokhlin.symbolicCode_preserving line 62
  8. lemma OAI.Rokhlin.symbolicShift_mixing line 66
  9. lemma OAI.Rokhlin.symbolicCode_rectangles line 85
  10. lemma OAI.Rokhlin.symbolicCode_integral line 98
  11. lemma OAI.Rokhlin.symbolicCode_entropy line 105
  12. theorem OAI.Rokhlin.finite_alphabet_no_witness line 124
  13. lemma OAI.Rokhlin.exists_signed_subsequence line 205
  14. lemma OAI.Rokhlin.prod_sign_one line 228
  15. theorem OAI.Rokhlin.finite_alphabet_correlation_zero line 233
  16. abbrev OAI.Rokhlin.observableProcess line 278
  17. abbrev OAI.Rokhlin.observableTail line 281
  18. lemma OAI.Rokhlin.observableProcess_translate line 285
  19. lemma OAI.Rokhlin.observableProcess_measurable line 290
  20. theorem OAI.Rokhlin.finite_tail_entropy_zero line 293
  21. theorem OAI.Rokhlin.tail_finite_correlation_zero line 316
  22. lemma OAI.Rokhlin.prod_replace_one line 344
  23. lemma OAI.Rokhlin.prod_replace_dep line 353
  24. lemma OAI.Rokhlin.integral_comp_preserving line 361
  25. lemma OAI.Rokhlin.integral_mean_interval line 367
  26. lemma OAI.Rokhlin.centered_pairing_distance line 375
  27. theorem OAI.Rokhlin.tail_correlation_zero line 419
  28. lemma OAI.Rokhlin.processPast_coord line 494
  29. lemma OAI.Rokhlin.real_integrable_bound line 507
  30. theorem OAI.Rokhlin.remote_last_replacement line 512
  31. theorem OAI.Rokhlin.last_centered_correlation_zero line 577