OAI/MeasureTheory/Falconer/Estimates/ParentRefinedEndpointSelection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A selected endpoint configuration can be regularized again while keeping the original reference profile and an explicit loss in the new active parent.

  1. theorem OAI.Falconer.blockClass_parent_refine_quarter_endpoint_subset line 11