OAI/MeasureTheory/Falconer/Graphs/GraphEnergyError.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Arbitrary power decay of the explicit graph-energy error

The derivative order is chosen first. The constants obtained at that order may then be used in the uniform graph estimate. Both cap and row counts, and the four model-mass inverses, are included in the polynomial cost.

  1. theorem OAI.Falconer.capGraphError_arbitrary_power line 17