OAI/MeasureTheory/Falconer/Geometry/QuarterChartFineGain.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Apply the proved regular gain to the quarter chart arising from the scale-product construction. Both point and line witnesses are transported.

  1. theorem OAI.Falconer.quarter_chart_regular_fine_gain line 12