OAI/MeasureTheory/Falconer/Incidence/BlockDescendantCounts.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Local descendant counts in a retained block class, with both binning losses explicit. These are the finite covering counts used by regularity.

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