OAI/Dynamics/StandardMap/Entropy/PhysicalVolume.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StandardMapEntropy.fineCoordinate_continuous line 12
  2. lemma OAI.StandardMapEntropy.fineTrapped_closed line 16
  3. def OAI.StandardMapEntropy.fineLiftTrapped line 29
  4. lemma OAI.StandardMapEntropy.fineLiftTrapped_image line 31
  5. lemma OAI.StandardMapEntropy.volume_pairToComplex_image line 47
  6. def OAI.StandardMapEntropy.fineVolumeFactor line 58
  7. lemma OAI.StandardMapEntropy.fineLiftTrapped_volume_eq line 60
  8. theorem OAI.StandardMapEntropy.fineLiftTrapped_volume line 74
  9. def OAI.StandardMapEntropy.complexCell line 94
  10. lemma OAI.StandardMapEntropy.complexRep_projection_of_cell line 95
  11. lemma OAI.StandardMapEntropy.measurePreserving_complexProjection_cell line 99
  12. lemma OAI.StandardMapEntropy.area_le_volume_of_complexRep_subset line 107
  13. lemma OAI.StandardMapEntropy.measurableSet_fineLiftTrapped line 115
  14. lemma OAI.StandardMapEntropy.exists_fineVolumeFactor_bound line 123
  15. lemma OAI.StandardMapEntropy.circle_coe_eq_of_close line 135
  16. lemma OAI.StandardMapEntropy.complexProjection_eq_of_close line 147
  17. def OAI.StandardMapEntropy.Entropy.history line 164
  18. lemma OAI.StandardMapEntropy.Entropy.history_measurable line 166
  19. def OAI.StandardMapEntropy.Entropy.historySnocEquiv line 168
  20. lemma OAI.StandardMapEntropy.Entropy.historySnocEquiv_apply line 174
  21. lemma OAI.StandardMapEntropy.Entropy.cond_history_succ line 177
  22. lemma OAI.StandardMapEntropy.Entropy.cond_history_one line 183
  23. lemma OAI.StandardMapEntropy.Entropy.cond_history_markov line 187
  24. lemma OAI.StandardMapEntropy.Entropy.obs_history_markov line 206
  25. lemma OAI.StandardMapEntropy.Entropy.cond_support_integral line 215
  26. lemma OAI.StandardMapEntropy.Entropy.log_card_le_of_card_le line 223
  27. lemma OAI.StandardMapEntropy.Entropy.cond_support_bound_ae line 242
  28. lemma OAI.StandardMapEntropy.Entropy.cond_support_integral_ae line 260
  29. lemma OAI.StandardMapEntropy.Entropy.mass_le_one line 268
  30. lemma OAI.StandardMapEntropy.Entropy.obs_lower_small_atoms line 272
  31. def OAI.StandardMapEntropy.LocalCoding.truncate line 308
  32. lemma OAI.StandardMapEntropy.LocalCoding.truncate_none_iff line 310
  33. lemma OAI.StandardMapEntropy.LocalCoding.truncate_some line 313
  34. lemma OAI.StandardMapEntropy.LocalCoding.truncate_eq_some_iff line 314
  35. lemma OAI.StandardMapEntropy.LocalCoding.truncate_inj line 320
  36. def OAI.StandardMapEntropy.LocalCoding.reach line 325
  37. lemma OAI.StandardMapEntropy.LocalCoding.reach_step line 328
  38. lemma OAI.StandardMapEntropy.LocalCoding.reach_mono line 329
  39. lemma OAI.StandardMapEntropy.LocalCoding.base_subset_reach line 331
  40. lemma OAI.StandardMapEntropy.LocalCoding.next_mem_reach line 332
  41. lemma OAI.StandardMapEntropy.LocalCoding.path_mem_reach line 335
  42. instance OAI.StandardMapEntropy.LocalCoding.optionFinsetMeasurableSpace line 341
  43. instance OAI.StandardMapEntropy.LocalCoding.optionFinsetMeasurableSingleton line 342
  44. lemma OAI.StandardMapEntropy.LocalCoding.measurable_truncate line 346
  45. def OAI.StandardMapEntropy.LocalCoding.maskedState line 347
  46. lemma OAI.StandardMapEntropy.LocalCoding.measurable_maskedState line 349
  47. lemma OAI.StandardMapEntropy.LocalCoding.maskedState_of_mem line 353
  48. lemma OAI.StandardMapEntropy.LocalCoding.maskedState_of_not_mem line 356
  49. lemma OAI.StandardMapEntropy.LocalCoding.maskedState_zero_none line 359
  50. lemma OAI.StandardMapEntropy.LocalCoding.ae_transition_orbit line 369
  51. def OAI.StandardMapEntropy.LocalCoding.transitionSupport line 387
  52. lemma OAI.StandardMapEntropy.LocalCoding.transitionSupport_log_bound line 393
  53. lemma OAI.StandardMapEntropy.LocalCoding.masked_transition_mem line 411
  54. lemma OAI.StandardMapEntropy.LocalCoding.tail_integral line 429
  55. lemma OAI.StandardMapEntropy.LocalCoding.masked_cond_le_tail line 442
  56. lemma OAI.StandardMapEntropy.LocalCoding.masked_initial_entropy line 457
  57. lemma OAI.StandardMapEntropy.LocalCoding.masked_history_entropy_upper line 474