OAI/Dynamics/StandardMap/Entropy/FiniteBinCoding.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StandardMapEntropy.LocalCoding.taggedCode line 14
  2. lemma OAI.StandardMapEntropy.LocalCoding.measurable_taggedCode line 16
  3. lemma OAI.StandardMapEntropy.LocalCoding.invariant_iterate line 22
  4. def OAI.StandardMapEntropy.LocalCoding.taggedSuccessors line 27
  5. lemma OAI.StandardMapEntropy.LocalCoding.taggedSuccessors_card line 32
  6. lemma OAI.StandardMapEntropy.LocalCoding.tagged_transition line 38
  7. lemma OAI.StandardMapEntropy.LocalCoding.tagged_codeFiber_subset line 47
  8. lemma OAI.StandardMapEntropy.LocalCoding.integrable_finite_observable line 56
  9. theorem OAI.StandardMapEntropy.entropy_lower_finite_bin_coding line 66
  10. theorem OAI.StandardMapEntropy.entropy_lower_finite_spectral_bins line 105
  11. lemma OAI.StandardMapEntropy.exists_lower_spectral_bins line 167
  12. def OAI.StandardMapEntropy.Entropy.wordPack line 219
  13. lemma OAI.StandardMapEntropy.Entropy.wordPack_apply line 223
  14. lemma OAI.StandardMapEntropy.Entropy.obs_word_pack line 230
  15. lemma OAI.StandardMapEntropy.Entropy.rate_power_word line 234
  16. lemma OAI.StandardMapEntropy.Entropy.word_eval_zero line 254
  17. lemma OAI.StandardMapEntropy.Entropy.obs_word_markov_step line 258
  18. lemma OAI.StandardMapEntropy.Entropy.obs_word_markov_bound line 285
  19. lemma OAI.StandardMapEntropy.Entropy.rate_le_oneStep line 296
  20. lemma OAI.StandardMapEntropy.grid_rate_derivative_upper line 324
  21. lemma OAI.StandardMapEntropy.eventually_grid_rate_derivative_upper line 371
  22. lemma OAI.StandardMapEntropy.metricEntropy_iterate_derivative_upper line 389
  23. lemma OAI.StandardMapEntropy.finite_rate_le_of_grid_rates line 403
  24. lemma OAI.StandardMapEntropy.standardDerivative_average_bounds line 428
  25. lemma OAI.StandardMapEntropy.tendsto_integral_standardDerivative_average line 442
  26. theorem OAI.StandardMapEntropy.metricEntropy_le_integral_standardLyapunov line 452
  27. lemma OAI.StandardMapEntropy.standardLyapunov_le_log_growthBase line 483
  28. theorem OAI.StandardMapEntropy.integral_standardLyapunov_le_metricEntropy line 489
  29. theorem OAI.StandardMapEntropy.metricEntropy_eq_integral_standardLyapunov line 510
  30. theorem OAI.StandardMapEntropy.actual_positive_lyapunov_and_entropy line 522