OAI/MeasureTheory/Falconer/Incidence/BlockClassRatios.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Transfer a finite prefix-count bound through the retained block class, keeping the exact class-selection and dyadic-bin losses.

  1. theorem OAI.Falconer.Regularization.blockClass_ratio_le line 10