OAI/MeasureTheory/Falconer/Estimates/PatchedInverseFactors.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Globally supported factors for the exact local inverse

A fixed smooth patch cutoff is inserted in both endpoint factors. It is one on the support of the original inverse, so the finite sum stays exact. Each individual factor retains its original support on the whole sphere.

  1. def OAI.Falconer.inverseFactorPatch line 16
  2. theorem OAI.Falconer.inverseFactorPatch_contDiff line 19
  3. theorem OAI.Falconer.inverseFactorPatch_one line 23
  4. theorem OAI.Falconer.inverseFactorPatch_ne_zero line 33
  5. def OAI.Falconer.SmoothSeparation.bilateralCutoff line 45
  6. theorem OAI.Falconer.SmoothSeparation.bilateralCutoff_value line 55
  7. theorem OAI.Falconer.SmoothSeparation.HasOrder.bilateralCutoff line 66
  8. theorem OAI.Falconer.patched_finite_class_inverse_factors line 79