OAI/Dynamics/StandardMap/Entropy/SupportEntropy.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StandardMapEntropy.Entropy.shannon_support_bound line 14
  2. lemma OAI.StandardMapEntropy.Entropy.cond_support_bound line 32
  3. def OAI.StandardMapEntropy.Entropy.errorObs line 60
  4. lemma OAI.StandardMapEntropy.Entropy.errorObs_measurable line 63
  5. lemma OAI.StandardMapEntropy.Entropy.errorObs_false line 68
  6. lemma OAI.StandardMapEntropy.Entropy.obs_bool line 71
  7. lemma OAI.StandardMapEntropy.Entropy.cond_fano line 78
  8. lemma OAI.StandardMapEntropy.Entropy.cond_fano_bound line 99
  9. lemma OAI.StandardMapEntropy.Entropy.cond_small_of_error line 106
  10. lemma OAI.StandardMapEntropy.Entropy.compact_partition_core line 135
  11. lemma OAI.StandardMapEntropy.Entropy.cond_small_of_diameter line 186
  12. lemma OAI.StandardMapEntropy.circleRep_dist_le line 222
  13. lemma OAI.StandardMapEntropy.gridLabel_dist_le line 226
  14. lemma OAI.StandardMapEntropy.metricEntropy_le_of_grid_rates line 232
  15. def OAI.StandardMapEntropy.complexRep line 269
  16. lemma OAI.StandardMapEntropy.complexProjection_complexRep line 270
  17. lemma OAI.StandardMapEntropy.gridLabel_complexRep_close line 272
  18. lemma OAI.StandardMapEntropy.integrable_log_standardDerivativeProduct line 281
  19. lemma OAI.StandardMapEntropy.standard_iterate_grid_cover line 287
  20. lemma OAI.StandardMapEntropy.standard_iterate_grid_log_variation line 316
  21. lemma OAI.StandardMapEntropy.exists_dyadic_level line 337
  22. def OAI.StandardMapEntropy.dyadicLevel line 343
  23. lemma OAI.StandardMapEntropy.dyadicLevel_lower line 344
  24. lemma OAI.StandardMapEntropy.dyadicLevel_upper line 346
  25. lemma OAI.StandardMapEntropy.dyadicLevel_mono_bound line 355
  26. lemma OAI.StandardMapEntropy.measurable_dyadicLevel line 360
  27. lemma OAI.StandardMapEntropy.inv_dyadicLevel_le line 364
  28. abbrev OAI.StandardMapEntropy.AdaptiveSymbol line 374
  29. def OAI.StandardMapEntropy.dyadicGridVal line 375
  30. lemma OAI.StandardMapEntropy.measurable_dyadicGridVal line 377
  31. def OAI.StandardMapEntropy.adaptiveLabel line 380
  32. lemma OAI.StandardMapEntropy.measurable_nat_select line 382
  33. lemma OAI.StandardMapEntropy.measurable_adaptiveLabel line 388
  34. lemma OAI.StandardMapEntropy.adaptiveLabel_level line 391
  35. lemma OAI.StandardMapEntropy.adaptiveLabel_grid line 392
  36. lemma OAI.StandardMapEntropy.adaptiveLabel_rep_close line 398
  37. def OAI.StandardMapEntropy.adaptiveCenter line 403
  38. lemma OAI.StandardMapEntropy.adaptiveCenter_label line 406
  39. def OAI.StandardMapEntropy.adaptiveSuccessors line 410
  40. lemma OAI.StandardMapEntropy.adaptiveSuccessors_card line 413
  41. lemma OAI.StandardMapEntropy.standardLift_lipschitz_bound line 423
  42. lemma OAI.StandardMapEntropy.adaptive_successor_mem line 427