OAI/MeasureTheory/SelfSimilar/BallLimits.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EntropyRateDimension.Coding.clippedCorr line 26
  2. def OAI.EntropyRateDimension.Coding.clippedLimit line 28
  3. theorem OAI.EntropyRateDimension.Coding.clippedCorr_measurable line 31
  4. theorem OAI.EntropyRateDimension.Coding.clippedLimit_measurable line 33
  5. theorem OAI.EntropyRateDimension.Coding.clip_bound line 37
  6. theorem OAI.EntropyRateDimension.Coding.clippedCorr_bound line 42
  7. theorem OAI.EntropyRateDimension.Coding.clippedLimit_bound line 45
  8. theorem OAI.EntropyRateDimension.Coding.ae_clipped_limit line 48
  9. theorem OAI.EntropyRateDimension.Coding.ae_corr_triangle line 53
  10. def OAI.EntropyRateDimension.Coding.weightObs line 76
  11. def OAI.EntropyRateDimension.Coding.contractionObs line 77
  12. def OAI.EntropyRateDimension.Coding.prefixInfo line 79
  13. theorem OAI.EntropyRateDimension.Coding.prefixInfo_succ line 82
  14. theorem OAI.EntropyRateDimension.Coding.triangle_succ line 94
  15. theorem OAI.EntropyRateDimension.Coding.prefixInfo_telescope line 102
  16. theorem OAI.EntropyRateDimension.Coding.head_integrable line 119
  17. theorem OAI.EntropyRateDimension.Coding.head_integral line 129
  18. theorem OAI.EntropyRateDimension.Coding.ae_point_support line 141
  19. theorem OAI.EntropyRateDimension.Coding.law_support_compact line 150
  20. def OAI.EntropyRateDimension.Coding.infoRate line 155
  21. theorem OAI.EntropyRateDimension.Coding.ae_prefixInfo_limit line 158