OAI/Dynamics/StandardMap/Coding/TypicalWordCodebook.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HyperbolicCoding.productWordWeight line 14
  2. def OAI.HyperbolicCoding.wordInformation line 15
  3. lemma OAI.HyperbolicCoding.productWordWeight_sum line 18
  4. lemma OAI.HyperbolicCoding.productWordWeight_nonneg line 23
  5. lemma OAI.HyperbolicCoding.productWordWeight_eq_exp line 27
  6. theorem OAI.HyperbolicCoding.information_codebook_card line 36
  7. lemma OAI.HyperbolicCoding.wordInformation_word line 63
  8. lemma OAI.HyperbolicCoding.information_uniform_bound line 69
  9. theorem OAI.HyperbolicCoding.eventually_upper_information_codebook line 75
  10. def OAI.HyperbolicCoding.weightEntropy line 123
  11. def OAI.HyperbolicCoding.informationVariance line 124
  12. lemma OAI.HyperbolicCoding.weightInformation_centered line 128
  13. lemma OAI.HyperbolicCoding.wordInformation_centered line 134
  14. lemma OAI.HyperbolicCoding.wordInformation_variance line 140
  15. lemma OAI.HyperbolicCoding.productWordWeight_le_exp line 150
  16. lemma OAI.HyperbolicCoding.iid_bad_information_mass line 166
  17. theorem OAI.HyperbolicCoding.eventually_iid_typical_words line 182
  18. def OAI.HyperbolicCoding.finiteWeightLaw line 218
  19. instance OAI.HyperbolicCoding.finiteWeightLaw_finite line 221
  20. lemma OAI.HyperbolicCoding.finiteWeightLaw_singleton line 225
  21. lemma OAI.HyperbolicCoding.finiteWeightLaw_probability line 231
  22. def OAI.HyperbolicCoding.iidShift line 238
  23. lemma OAI.HyperbolicCoding.iidShift_iterate line 247
  24. lemma OAI.HyperbolicCoding.iidShift_preserving line 260
  25. lemma OAI.HyperbolicCoding.iid_word_eq line 267
  26. lemma OAI.HyperbolicCoding.iid_word_law line 274
  27. lemma OAI.HyperbolicCoding.iid_word_mass line 285
  28. lemma OAI.HyperbolicCoding.iid_disjoint_coordinate_independent line 307
  29. lemma OAI.HyperbolicCoding.iidShift_symm_iterate line 330
  30. lemma OAI.HyperbolicCoding.iid_tail_eq line 343
  31. lemma OAI.HyperbolicCoding.iid_past_eq line 349
  32. theorem OAI.HyperbolicCoding.iid_weakBernoulli line 355
  33. lemma OAI.HyperbolicCoding.shannon_product_weights line 385
  34. lemma OAI.HyperbolicCoding.shannon_productWordWeight line 392
  35. theorem OAI.HyperbolicCoding.iid_rate line 417
  36. lemma OAI.HyperbolicCoding.weight_le_one line 442
  37. lemma OAI.HyperbolicCoding.weightEntropy_zero_of_one line 447
  38. lemma OAI.HyperbolicCoding.positive_weightEntropy_max_bound line 464
  39. theorem OAI.HyperbolicCoding.iid_nullSingleton line 479
  40. theorem OAI.HyperbolicCoding.iid_finite_determination line 507