OAI/Dynamics/StandardMap/MiddlePrefixBridge.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StandardMapEntropy.torusPrefixGrowth line 11
  2. lemma OAI.StandardMapEntropy.isClosed_torusPrefixGrowth line 13
  3. lemma OAI.StandardMapEntropy.torusPrefixGrowth_lift line 17
  4. lemma OAI.StandardMapEntropy.prefix_row_cover line 22
  5. def OAI.StandardMapEntropy.bridgeRowLength line 32
  6. lemma OAI.StandardMapEntropy.bridgeRowLength_pos line 33
  7. lemma OAI.StandardMapEntropy.bridgeRowLength_choice line 35
  8. lemma OAI.StandardMapEntropy.prefix_row_cover_bool line 40
  9. def OAI.StandardMapEntropy.middlePrefixEvent line 46
  10. lemma OAI.StandardMapEntropy.measurableSet_middlePrefixEvent line 48
  11. def OAI.StandardMapEntropy.middleBridgeConstant line 50
  12. lemma OAI.StandardMapEntropy.middleBridgeConstant_ne_top line 51
  13. lemma OAI.StandardMapEntropy.actual_middle_prefix_product line 53