OAI/Dynamics/StandardMap/Entropy/LiftGrid.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StandardMapEntropy.gridIntIndex line 12
  2. lemma OAI.StandardMapEntropy.gridIndex_coe_int line 17
  3. def OAI.StandardMapEntropy.gridIntLabel line 33
  4. lemma OAI.StandardMapEntropy.gridLabel_complex_lift line 35
  5. lemma OAI.StandardMapEntropy.floor_close_int line 38
  6. def OAI.StandardMapEntropy.liftGridCover line 52
  7. lemma OAI.StandardMapEntropy.liftGridCover_card line 55
  8. lemma OAI.StandardMapEntropy.liftGridCover_mem line 65
  9. lemma OAI.StandardMapEntropy.PlaneAreaPreserving.thin_cover line 89
  10. lemma OAI.StandardMapEntropy.PlaneAreaPreserving.grid_cover line 145
  11. lemma OAI.StandardMapEntropy.norm_sub_le_of_derivative_bound line 192
  12. lemma OAI.StandardMapEntropy.standardLift_iterate_control line 199
  13. lemma OAI.StandardMapEntropy.log_norm_sub_le_of_one_le line 250
  14. def OAI.StandardMapEntropy.Entropy.shannon line 282
  15. lemma OAI.StandardMapEntropy.Entropy.negMulLog_le_cross line 285
  16. lemma OAI.StandardMapEntropy.Entropy.shannon_le_cross line 299
  17. lemma OAI.StandardMapEntropy.Entropy.shannon_nonneg line 308
  18. lemma OAI.StandardMapEntropy.Entropy.shannon_scale line 314
  19. lemma OAI.StandardMapEntropy.Entropy.shannon_bound line 319
  20. lemma OAI.StandardMapEntropy.Entropy.matrix_row_nonneg line 327
  21. lemma OAI.StandardMapEntropy.Entropy.matrix_col_nonneg line 330
  22. lemma OAI.StandardMapEntropy.Entropy.matrix_le_row line 333
  23. lemma OAI.StandardMapEntropy.Entropy.matrix_le_col line 336
  24. lemma OAI.StandardMapEntropy.Entropy.matrix_subadd line 340
  25. lemma OAI.StandardMapEntropy.Entropy.shannon_total_bound line 395
  26. lemma OAI.StandardMapEntropy.Entropy.matrix_super_row line 418