OAI/Dynamics/StandardMap/Entropy/ObservableEntropy.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StandardMapEntropy.Entropy.mass line 16
  2. def OAI.StandardMapEntropy.Entropy.obs line 17
  3. lemma OAI.StandardMapEntropy.Entropy.mass_nonneg line 19
  4. lemma OAI.StandardMapEntropy.Entropy.fiber_disjoint line 21
  5. lemma OAI.StandardMapEntropy.Entropy.mass_sum line 24
  6. lemma OAI.StandardMapEntropy.Entropy.mass_joint_row line 30
  7. lemma OAI.StandardMapEntropy.Entropy.mass_joint_swap line 43
  8. lemma OAI.StandardMapEntropy.Entropy.mass_joint_col line 50
  9. lemma OAI.StandardMapEntropy.Entropy.obs_pair_swap line 56
  10. lemma OAI.StandardMapEntropy.Entropy.obs_pair_ge_left line 62
  11. lemma OAI.StandardMapEntropy.Entropy.obs_pair_ge_right line 67
  12. lemma OAI.StandardMapEntropy.Entropy.obs_pair_subadd line 71
  13. lemma OAI.StandardMapEntropy.Entropy.obs_pair_subadd_prob line 76
  14. lemma OAI.StandardMapEntropy.Entropy.mass_pair_function line 82
  15. lemma OAI.StandardMapEntropy.Entropy.obs_pair_function line 100
  16. lemma OAI.StandardMapEntropy.Entropy.obs_factor line 107
  17. lemma OAI.StandardMapEntropy.Entropy.obs_equiv line 114
  18. lemma OAI.StandardMapEntropy.Entropy.sum_mass_mul_integral line 124
  19. lemma OAI.StandardMapEntropy.Entropy.mass_triple_assoc line 151
  20. lemma OAI.StandardMapEntropy.Entropy.obs_triple_assoc line 160
  21. lemma OAI.StandardMapEntropy.Entropy.obs_strong_subadd line 164
  22. def OAI.StandardMapEntropy.Entropy.cond line 188
  23. lemma OAI.StandardMapEntropy.Entropy.cond_nonneg line 189
  24. lemma OAI.StandardMapEntropy.Entropy.cond_le_obs line 191
  25. lemma OAI.StandardMapEntropy.Entropy.cond_pair_right line 193
  26. lemma OAI.StandardMapEntropy.Entropy.cond_pair_swap_right line 201
  27. lemma OAI.StandardMapEntropy.Entropy.cond_chain line 211
  28. lemma OAI.StandardMapEntropy.Entropy.cond_factor_right line 220
  29. lemma OAI.StandardMapEntropy.Entropy.cond_pair_subadd line 238
  30. lemma OAI.StandardMapEntropy.Entropy.obs_nonneg line 257
  31. lemma OAI.StandardMapEntropy.Entropy.obs_bound line 260
  32. lemma OAI.StandardMapEntropy.Entropy.obs_const line 264
  33. lemma OAI.StandardMapEntropy.Entropy.mass_comp_preserving line 275
  34. lemma OAI.StandardMapEntropy.Entropy.obs_comp_preserving line 280
  35. lemma OAI.StandardMapEntropy.Entropy.cond_comp_preserving line 284
  36. def OAI.StandardMapEntropy.Entropy.word line 290
  37. lemma OAI.StandardMapEntropy.Entropy.word_measurable line 292
  38. def OAI.StandardMapEntropy.Entropy.wordSplit line 294
  39. lemma OAI.StandardMapEntropy.Entropy.wordSplit_apply line 298
  40. lemma OAI.StandardMapEntropy.Entropy.word_split line 303
  41. lemma OAI.StandardMapEntropy.Entropy.obs_word_split line 311
  42. lemma OAI.StandardMapEntropy.Entropy.obs_word_subadd line 315
  43. lemma OAI.StandardMapEntropy.Entropy.obs_word_one line 324
  44. lemma OAI.StandardMapEntropy.Entropy.obs_word_zero line 338
  45. lemma OAI.StandardMapEntropy.Entropy.cond_equiv_left line 344
  46. lemma OAI.StandardMapEntropy.Entropy.cond_equiv_right line 353
  47. lemma OAI.StandardMapEntropy.Entropy.cond_word_split line 362
  48. lemma OAI.StandardMapEntropy.Entropy.cond_word_subadd line 369
  49. lemma OAI.StandardMapEntropy.Entropy.cond_word_one line 383
  50. lemma OAI.StandardMapEntropy.Entropy.cond_word_zero line 396
  51. lemma OAI.StandardMapEntropy.Entropy.cond_word_bound line 401
  52. lemma OAI.StandardMapEntropy.Entropy.obs_word_comparison line 415
  53. lemma OAI.StandardMapEntropy.Entropy.obs_word_bddBelow line 424
  54. def OAI.StandardMapEntropy.Entropy.rate line 442
  55. lemma OAI.StandardMapEntropy.Entropy.rate_eq_lim line 444
  56. lemma OAI.StandardMapEntropy.Entropy.rate_tendsto line 447
  57. lemma OAI.StandardMapEntropy.Entropy.rate_le_div line 451
  58. lemma OAI.StandardMapEntropy.Entropy.rate_nonneg line 455
  59. lemma OAI.StandardMapEntropy.Entropy.rate_le_obs line 459
  60. lemma OAI.StandardMapEntropy.Entropy.rate_comparison line 462
  61. lemma OAI.StandardMapEntropy.Entropy.ofReal_rate_eq_iInf line 469
  62. lemma OAI.StandardMapEntropy.blockAtom_eq_fiber line 490
  63. lemma OAI.StandardMapEntropy.blockEntropy_eq_obs line 495
  64. lemma OAI.StandardMapEntropy.partitionEntropy_eq_ofReal_rate line 499
  65. lemma OAI.StandardMapEntropy.blockEntropy_rate_tendsto line 504
  66. lemma OAI.StandardMapEntropy.partitionEntropy_comparison line 508