OAI/MeasureTheory/SelfSimilar/RandomGrid.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.EntropyRateDimension.FiniteDistribution.entropy_map_le line 15
  2. theorem OAI.EntropyRateDimension.FiniteDistribution.js_le_map_add line 21
  3. theorem OAI.EntropyRateDimension.FiniteDistribution.tv_maps_le_disagreement line 35
  4. def OAI.EntropyRateDimension.RandomGrid.hit line 89
  5. theorem OAI.EntropyRateDimension.RandomGrid.hit_eq_indicator line 92
  6. theorem OAI.EntropyRateDimension.RandomGrid.hit_integrable line 99
  7. theorem OAI.EntropyRateDimension.RandomGrid.integral_hit line 103
  8. theorem OAI.EntropyRateDimension.RandomGrid.circle_norm_le_of_floor_ne line 109
  9. theorem OAI.EntropyRateDimension.MeasureEntropy.observationLaw_map_weight line 135
  10. theorem OAI.EntropyRateDimension.MeasureEntropy.integral_finite_observation line 144
  11. theorem OAI.EntropyRateDimension.MeasureEntropy.entropy_binary_extra line 163