OAI/MeasureTheory/Falconer/Incidence/ScalarBlockSumProduct.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A quantitative scalar sum-product alternative with all block parameters chosen. The input and output concern the original dyadic leaf set.

  1. theorem OAI.Falconer.Regularization.scalar_block_sum_product line 10