OAI/Dynamics/StandardMap/Entropy/LocallyFiniteLower.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StandardMapEntropy.LocalCoding.codeFiber line 14
  2. lemma OAI.StandardMapEntropy.LocalCoding.masked_history_none_iff line 18
  3. lemma OAI.StandardMapEntropy.LocalCoding.masked_history_small_atoms line 29
  4. lemma OAI.StandardMapEntropy.LocalCoding.masked_history_entropy_lower line 60
  5. lemma OAI.StandardMapEntropy.LocalCoding.tendsto_code_tail line 75
  6. lemma OAI.StandardMapEntropy.LocalCoding.lower_rate_truncation line 94
  7. theorem OAI.StandardMapEntropy.LocalCoding.lower_of_finite_rate_bound line 124
  8. lemma OAI.StandardMapEntropy.complexProjection_sub line 144
  9. lemma OAI.StandardMapEntropy.adaptive_rep_radius line 147
  10. lemma OAI.StandardMapEntropy.adaptive_lift_difference line 155
  11. lemma OAI.StandardMapEntropy.adaptive_codeFiber_trapped line 195
  12. lemma OAI.StandardMapEntropy.measurableSet_codeFiber line 210
  13. theorem OAI.StandardMapEntropy.adaptive_codeFiber_volume line 218
  14. lemma OAI.StandardMapEntropy.exists_fine_parameters line 245
  15. lemma OAI.StandardMapEntropy.exists_spectral_rate_code line 253
  16. lemma OAI.StandardMapEntropy.Entropy.obs_lower_information line 296
  17. lemma OAI.StandardMapEntropy.LocalCoding.masked_history_atom_subset line 318
  18. def OAI.StandardMapEntropy.LocalCoding.initialInformation line 335
  19. lemma OAI.StandardMapEntropy.LocalCoding.initialInformation_history line 339
  20. lemma OAI.StandardMapEntropy.LocalCoding.masked_history_weighted_small line 348
  21. lemma OAI.StandardMapEntropy.LocalCoding.masked_history_weighted_lower line 375
  22. lemma OAI.StandardMapEntropy.LocalCoding.tendsto_integral_code_truncation line 398
  23. lemma OAI.StandardMapEntropy.LocalCoding.weighted_lower_rate_truncation line 414
  24. theorem OAI.StandardMapEntropy.LocalCoding.weighted_lower_of_finite_rate_bound line 442
  25. lemma OAI.StandardMapEntropy.Entropy.rate_equiv line 465
  26. lemma OAI.StandardMapEntropy.finite_rate_le_metricEntropy line 475