OAI/MeasureTheory/SelfSimilar/RetainedLoss.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EntropyRateDimension.MeasureEntropy.grid_le_averaged_add_log_two line 10
2. def OAI.EntropyRateDimension.Typed.fineScale line 29
3. def OAI.EntropyRateDimension.Typed.bandStart line 30
4. theorem OAI.EntropyRateDimension.Typed.fineScale_pos line 32
5. theorem OAI.EntropyRateDimension.Typed.fineScale_lt_one line 34
6. theorem OAI.EntropyRateDimension.Typed.fineScale_log line 39
7. theorem OAI.EntropyRateDimension.Typed.expected_loss_linear line 43
8. theorem OAI.EntropyRateDimension.Typed.discarded_loss_bound line 70
9. def OAI.EntropyRateDimension.Typed.retainedLoss line 96
10. theorem OAI.EntropyRateDimension.Typed.retained_loss_linear line 100