OAI/MeasureTheory/Falconer/Graphs/GraphErrorAbsorption.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Absorbing the finite graph localization errors

There are at most R^(2d) rows (pairs of child cells), and a polynomial number of cap pairs. The four model-mass inverses and the energy prefactor cost at most R^(5d). The derivative order is chosen before the scale, spatial laws, graph and endpoint symbols.

  1. theorem OAI.Falconer.graph_discarded_sum_arbitrary_power line 19