OAI/MeasureTheory/Falconer/Angular/MixedCapDenominator.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Full ambient derivative bounds for the cap denominator

At a point of the sphere, only the bounded number of nearby centers can contribute. The estimate applies to the full multilinear derivative.

  1. theorem OAI.Falconer.capDenominator_ambient_derivatives line 16