OAI/Dynamics/StandardMap/ArrayHalf.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StandardMapEntropy.arrayHalf line 11
  2. lemma OAI.StandardMapEntropy.arrayHalf_unit line 23
  3. lemma OAI.StandardMapEntropy.arrayDilate_unit line 30
  4. lemma OAI.StandardMapEntropy.arrayDilate_half line 37
  5. lemma OAI.StandardMapEntropy.arrayHalf_dilate line 41
  6. def OAI.StandardMapEntropy.nonaffineHalfOn line 45
  7. lemma OAI.StandardMapEntropy.continuous_nonaffineHalfOn line 51
  8. def OAI.StandardMapEntropy.nonaffineHalf line 57
  9. lemma OAI.StandardMapEntropy.measurable_nonaffineHalf line 59
  10. lemma OAI.StandardMapEntropy.nonaffineHalf_unit line 62
  11. lemma OAI.StandardMapEntropy.nonaffineDilate_half line 65
  12. lemma OAI.StandardMapEntropy.nonaffineHalf_dilate line 69
  13. lemma OAI.StandardMapEntropy.map_half_dilate line 74
  14. lemma OAI.StandardMapEntropy.map_dilate_half line 80
  15. lemma OAI.StandardMapEntropy.CriticalScaleSequence.half_balance line 88