OAI/MeasureTheory/SelfSimilar/SumsetBound.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EntropyRateDimension.FairPairs.Law.bandSupport line 15
  2. def OAI.EntropyRateDimension.FairPairs.Law.bandCost line 19
  3. theorem OAI.EntropyRateDimension.FairPairs.Law.support_nonempty line 24
  4. theorem OAI.EntropyRateDimension.FairPairs.Law.subtype_sum line 30
  5. theorem OAI.EntropyRateDimension.FairPairs.mass_support line 33
  6. theorem OAI.EntropyRateDimension.FairPairs.sum_supportâ‚‚ line 40
  7. theorem OAI.EntropyRateDimension.FairPairs.mean_deviation_le_bandCost line 49
  8. theorem OAI.EntropyRateDimension.FairPairs.exists_capacity_refinement line 81
  9. def OAI.EntropyRateDimension.FairPairs.Law.partitionEntropy line 111
  10. def OAI.EntropyRateDimension.FairPairs.Law.refinementCost line 117
  11. theorem OAI.EntropyRateDimension.FairPairs.exists_fine_partition line 120
  12. theorem OAI.EntropyRateDimension.FairPairs.exists_separating_depth line 145
  13. theorem OAI.EntropyRateDimension.FairPairs.dyadic_upper_eq line 164
  14. theorem OAI.EntropyRateDimension.FairPairs.band_scale_sum line 167
  15. theorem OAI.EntropyRateDimension.FairPairs.sum_refinementCost_le line 203
  16. theorem OAI.EntropyRateDimension.FairPairs.observableEntropy_support line 249
  17. def OAI.EntropyRateDimension.FairPairs.Law.sumset line 265
  18. theorem OAI.EntropyRateDimension.FairPairs.pair_bound_natural line 269
  19. def OAI.EntropyRateDimension.FairPairs.Law.shannonEntropy line 323
  20. def OAI.EntropyRateDimension.FairPairs.Law.gridEntropy line 325
  21. theorem OAI.EntropyRateDimension.FairPairs.pair_bound line 329