OAI/MeasureTheory/Falconer/Estimates/MixedComposition.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Pointwise mixed derivative budgets for composition

The fixed constant is the actual finite sum over ordered partitions. A derivative budget of degree i for the inner map gives degree n for its composition, with no loss depending on the scale.

  1. theorem OAI.Falconer.compact_iteratedFDeriv_bound line 24
  2. def OAI.Falconer.mixedCompositionBudget line 38
  3. theorem OAI.Falconer.mixedCompositionBudget_nonneg line 41
  4. theorem OAI.Falconer.mixed_composition_derivative_bound line 45