OAI/Dynamics/StandardMap/RemainderLaws.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StandardMapEntropy.arrayTranslate_unit line 11
  2. lemma OAI.StandardMapEntropy.dyadicHalf_add line 17
  3. lemma OAI.StandardMapEntropy.half_translate line 19
  4. lemma OAI.StandardMapEntropy.unit_half_map line 27
  5. lemma OAI.StandardMapEntropy.half_map_translation_invariant line 32
  6. def OAI.StandardMapEntropy.CriticalScaleSequence.backwardLaw line 44
  7. def OAI.StandardMapEntropy.CriticalScaleSequence.backwardSum line 45
  8. def OAI.StandardMapEntropy.CriticalScaleSequence.remainderLaw line 46
  9. lemma OAI.StandardMapEntropy.CriticalScaleSequence.backwardLaw_zero line 47
  10. lemma OAI.StandardMapEntropy.CriticalScaleSequence.backwardLaw_succ line 48
  11. lemma OAI.StandardMapEntropy.CriticalScaleSequence.backwardLaw_unit line 50
  12. lemma OAI.StandardMapEntropy.CriticalScaleSequence.backwardLaw_translate line 54
  13. lemma OAI.StandardMapEntropy.CriticalScaleSequence.backwardSum_le line 58
  14. lemma OAI.StandardMapEntropy.CriticalScaleSequence.remainder_le line 59
  15. lemma OAI.StandardMapEntropy.CriticalScaleSequence.backwardSum_translate line 60
  16. lemma OAI.StandardMapEntropy.CriticalScaleSequence.backward_decomposition line 63
  17. lemma OAI.StandardMapEntropy.CriticalScaleSequence.remainder_unit line 67
  18. lemma OAI.StandardMapEntropy.CriticalScaleSequence.remainder_half line 68
  19. lemma OAI.StandardMapEntropy.CriticalScaleSequence.remainder_dilate line 71
  20. lemma OAI.StandardMapEntropy.CriticalScaleSequence.remainder_translate line 75
  21. lemma OAI.StandardMapEntropy.CriticalScaleSequence.remainder_shape line 85