OAI/MeasureTheory/Falconer/Estimates/InverseBudget.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Quantitative inverse amplitudes

The inverse coefficient of order j loses exactly 2*j derivatives. Its derivative bounds are asserted on sphere points, the set used by every subsequent stationary chart.

  1. theorem OAI.Falconer.localInverseAmplitude_zero_budget line 17
  2. theorem OAI.Falconer.localInverseAmplitude_scaled_budget line 45