OAI/MeasureTheory/SelfSimilar/BallIntegrability.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EntropyRateDimension.System.component line 22
  2. instance OAI.EntropyRateDimension.System.component_finite line 25
  3. theorem OAI.EntropyRateDimension.System.component_le line 31
  4. theorem OAI.EntropyRateDimension.System.affine_preimage_closedBall line 38
  5. theorem OAI.EntropyRateDimension.System.component_ball line 46
  6. def OAI.EntropyRateDimension.BallRatios.information line 56
  7. theorem OAI.EntropyRateDimension.BallRatios.massReal_pos line 59
  8. theorem OAI.EntropyRateDimension.BallRatios.information_component line 64
  9. theorem OAI.EntropyRateDimension.Coding.slope_ne_zero line 98
  10. theorem OAI.EntropyRateDimension.Coding.abs_slope_pos line 104
  11. theorem OAI.EntropyRateDimension.Coding.abs_slope_lt_one line 107
  12. theorem OAI.EntropyRateDimension.Coding.slope_tendsto_zero line 112