OAI/MeasureTheory/SelfSimilar/RadiusGrowth.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EntropyRateDimension.Coding.shift_iterate line 27
2. theorem OAI.EntropyRateDimension.Coding.contraction_integral line 31
3. theorem OAI.EntropyRateDimension.Coding.slope_log_sum line 41
4. theorem OAI.EntropyRateDimension.Coding.ae_slope_log_limit line 51
5. def OAI.EntropyRateDimension.Coding.exponent line 62
6. theorem OAI.EntropyRateDimension.Coding.infoRate_nonneg line 64
7. theorem OAI.EntropyRateDimension.Coding.exponent_nonneg line 69
8. theorem OAI.EntropyRateDimension.Coding.ae_prefix_exponent line 72