OAI/MeasureTheory/Falconer/Estimates/AllDimensionalRegularizationCardinality.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Dimension-dependent counts for regularization labels

A selected-depth gap of length b-a has at most 2^(d*(b-a)) children, so its logarithmic count bin has d*(b-a)+1 possibilities. The number of final labels is polynomial in terminal depth when the number of selected blocks is fixed.

  1. theorem OAI.Falconer.Regularization.labeledChildren_subset_extensions line 17
  2. theorem OAI.Falconer.Regularization.labeledChildren_card_le line 32
  3. theorem OAI.Falconer.Regularization.child_bin_le line 38
  4. theorem OAI.Falconer.Regularization.extendLabel_card_le line 45
  5. theorem OAI.Falconer.Regularization.upwardLabels_card_le line 62