OAI/MeasureTheory/Falconer/Fourier/DescriptorPairDerivativeScale.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform derivatives of the actual two-endpoint amplitude

The finite-order product loss is fixed before scale, classes, lists and points. This supplies the derivative premise of the masked inverse remainder.

  1. theorem OAI.Falconer.uniform_descriptor_pair_derivatives line 16