OAI/MeasureTheory/Falconer/Graphs/GraphTwoErrors.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Paying for both graph localization errors

The perpendicular error has an arbitrary derivative-order gain. The radial error has an independent arbitrary Schwartz-decay order. Both pay for the cap pairs, cell pairs and model-mass normalization with the same 11d cost.

  1. theorem OAI.Falconer.graph_two_errors_absorption line 15