OAI/MeasureTheory/Falconer/Measures/BudgetedEndpointProduct.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual geometric scale product with uniform depth and pencil budgets. Both outputs retain their original dyadic endpoints and half-slope chart.

  1. theorem OAI.Falconer.quarter_endpoint_budgeted_scale_product line 14