OAI/MeasureTheory/Falconer/Angular/MixedNormalizedCaps.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Full mixed derivative bounds for the normalized cap partition

The denominator and its fixed smooth reciprocal are the actual functions used by the cap partition. Their bounds depend on the dimension and order, independently of the selected separated net and its radius.

  1. theorem OAI.Falconer.capReciprocal_ambient_derivatives line 18
  2. theorem OAI.Falconer.normalizedCap_ambient_derivatives line 40