OAI/MeasureTheory/Falconer/Estimates/ScalarPrefixEntropy.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Entropy accounting for the ungrouped prefix. The lower estimate comes directly from the original finite set's ball bound.

  1. theorem OAI.Falconer.scalar_dyadic_prefix_entropy line 9
  2. theorem OAI.Falconer.scalar_stopped_prefix_length line 20
  3. theorem OAI.Falconer.Regularization.scalar_uniform_prefix_entropy line 34