OAI/MeasureTheory/SelfSimilar/BallRatios.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.EntropyRateDimension.BallRatios.exists_small_ratio_bound line 18
  2. abbrev OAI.EntropyRateDimension.BallRatios.Radius line 57
  3. def OAI.EntropyRateDimension.BallRatios.maximal line 59
  4. theorem OAI.EntropyRateDimension.BallRatios.measurable_ball_mass line 62
  5. theorem OAI.EntropyRateDimension.BallRatios.maximal_measurable line 68
  6. theorem OAI.EntropyRateDimension.BallRatios.maximal_tail line 74
  7. theorem OAI.EntropyRateDimension.BallRatios.maximal_finite_ae line 93
  8. def OAI.EntropyRateDimension.BallRatios.logEnvelope line 116
  9. theorem OAI.EntropyRateDimension.BallRatios.logEnvelope_nonneg line 119
  10. theorem OAI.EntropyRateDimension.BallRatios.logEnvelope_measurable line 122
  11. theorem OAI.EntropyRateDimension.BallRatios.logEnvelope_tail line 126
  12. theorem OAI.EntropyRateDimension.BallRatios.logEnvelope_integrable line 150
  13. theorem OAI.EntropyRateDimension.BallRatios.tendsto_ball_mass_right line 169
  14. theorem OAI.EntropyRateDimension.BallRatios.ratio_le_maximal line 178
  15. def OAI.EntropyRateDimension.BallRatios.logRatio line 194
  16. theorem OAI.EntropyRateDimension.BallRatios.logRatio_measurable line 197
  17. theorem OAI.EntropyRateDimension.BallRatios.logRatio_bounds line 206
  18. theorem OAI.EntropyRateDimension.BallRatios.ae_logRatio_limit line 223