OAI/MeasureTheory/SelfSimilar/TranslationGain.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.EntropyRateDimension.MeasureEntropy.mass_halfMix line 15
  2. theorem OAI.EntropyRateDimension.MeasureEntropy.observationLaw_map_entropy line 27
  3. theorem OAI.EntropyRateDimension.MeasureEntropy.mix_observationLaw_map_entropy line 36
  4. def OAI.EntropyRateDimension.MeasureEntropy.information line 51
  5. theorem OAI.EntropyRateDimension.MeasureEntropy.js_observationLaw_map line 55
  6. theorem OAI.EntropyRateDimension.MeasureEntropy.js_observationLaw line 66
  7. theorem OAI.EntropyRateDimension.MeasureEntropy.information_le_map_add line 79
  8. theorem OAI.EntropyRateDimension.MeasureEntropy.information_map_le_disagreement line 107
  9. theorem OAI.EntropyRateDimension.MeasureEntropy.fairShift_eq_halfMix line 149
  10. def OAI.EntropyRateDimension.MeasureEntropy.gridInformation line 153
  11. theorem OAI.EntropyRateDimension.MeasureEntropy.gridInformation_eq line 156
  12. theorem OAI.EntropyRateDimension.MeasureEntropy.gridInformation_intervalIntegrable line 162
  13. theorem OAI.EntropyRateDimension.MeasureEntropy.integral_gridInformation line 175
  14. theorem OAI.EntropyRateDimension.MeasureEntropy.gridInformation_le_boundary line 190
  15. theorem OAI.EntropyRateDimension.MeasureEntropy.averaged_fairShift_gain_le line 225
  16. theorem OAI.EntropyRateDimension.MeasureEntropy.relativeLabel_zero_of_good line 237
  17. theorem OAI.EntropyRateDimension.MeasureEntropy.gridInformation_le_fine_add_boundary line 262
  18. theorem OAI.EntropyRateDimension.MeasureEntropy.averaged_fairShift_gain_compare line 321
  19. theorem OAI.EntropyRateDimension.MeasureEntropy.two_point_gain line 354