OAI/MeasureTheory/Falconer/Estimates/EndpointSelectionLift.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Lift a retained set of endpoint cells to its actual original leaves. The cost is measured inside the active parent and uses the existing block fiber bounds, rather than the cardinality of the whole configuration.

  1. theorem OAI.Falconer.quarter_endpoint_subset_paths line 14
  2. theorem OAI.Falconer.blockClass_lift_endpoint_selection line 39