OAI/MeasureTheory/Falconer/Radial/TwoSlabSingleScale.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Single-scale mass of two transverse thick hyperplanes

Only the stated concentration bound at radius r is used. The long transverse side is covered by O(1/τ) radius-r codimension-two neighborhoods.

  1. theorem OAI.Falconer.two_slab_single_scale_bound line 15