OAI/MeasureTheory/Falconer/Estimates/ParentChildRetention.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Endpoint retention after restricting inside one actual recursive parent.

  1. theorem OAI.Falconer.Regularization.blockClass_parent_child_retention line 11