OAI/MeasureTheory/SelfSimilar/LocalMass.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EntropyRateDimension.LocalMass.restrict_le_hausdorff line 13
2. theorem OAI.EntropyRateDimension.LocalMass.positive_set_dim_ge line 58
3. theorem OAI.EntropyRateDimension.LocalMass.eventual_upper_of_limit line 92
4. theorem OAI.EntropyRateDimension.LocalMass.eventual_lower_of_limit line 117
5. theorem OAI.EntropyRateDimension.LocalMass.lower_dim_ge_of_limit line 138
6. theorem OAI.EntropyRateDimension.LocalMass.large_uniform_mass_set line 161