OAI/MeasureTheory/Falconer/Recursion/ParentProfileBounds.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Reference-profile bounds persist below an active parent and in the fixed quarter chart used by the actual scale-product construction.

  1. theorem OAI.Falconer.blockClass_parent_endpoint_ball line 13