OAI/MeasureTheory/Falconer/Estimates/WeightedCauchy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The L1 cost of the spatial Fourier separation

The coefficient is integrated before estimating the shell energy. Its squared cost is controlled by one L1 factor and a positive weighted energy.

  1. theorem OAI.Falconer.norm_integral_weighted_sq_le line 16