OAI/MeasureTheory/Falconer/Measures/EndpointScaleProduct.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual scale-product step on dyadic endpoint configurations. Both outputs stay in the same fixed quarter chart, with the same slope interval.

  1. theorem OAI.Falconer.quarter_endpoint_scale_product line 13