OAI/MeasureTheory/Falconer/Estimates/ScalarInverseTransfer.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Passing the stationary inverse estimate to the actual scalar transform

The angular normalization is removed exactly. A uniform pointwise error costs only the relative shell length 2^(v-a), before its fixed negative power is selected.

  1. theorem OAI.Falconer.scalar_shell_of_stationary_approximation line 16