OAI/MeasureTheory/SelfSimilar/LocalEntropy.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EntropyRateDimension.FiniteEntropy.entropy_le_mass_log_card line 14
2. theorem OAI.EntropyRateDimension.FiniteEntropy.entropy_split_bound line 36
3. theorem OAI.EntropyRateDimension.MeasureEntropy.entropy_subset_bound line 72
4. theorem OAI.EntropyRateDimension.MeasureEntropy.card_mul_mass_le_one line 106
5. theorem OAI.EntropyRateDimension.MeasureEntropy.label_ball_disjoint line 118
6. theorem OAI.EntropyRateDimension.MeasureEntropy.good_labels_card_bound line 148
7. theorem OAI.EntropyRateDimension.MeasureEntropy.grid_le_of_ball_mass line 178
8. theorem OAI.EntropyRateDimension.MeasureEntropy.grid_support_card_le line 211
9. theorem OAI.EntropyRateDimension.MeasureEntropy.grid_le_of_power_ball_mass line 229