OAI/MeasureTheory/Falconer/Shells/MaskedScalarShell.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The weighted scalar shell for the original masked distance law

The only analytic inputs are the precisely published gnomonic formula and quadratic stationary phase. The error and all finite-factor costs remain explicit until the uniform scale absorption step.

  1. theorem OAI.Falconer.exists_masked_scalar_shell_order line 18