OAI/MeasureTheory/FalconerCompletion/Estimates/SmoothReciprocal.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Quantitative estimates for the distance-set construction.

  1. def OAI.Attempt4FullFar.smoothReciprocal line 14
  2. lemma OAI.Attempt4FullFar.smoothReciprocal_zero line 17
  3. lemma OAI.Attempt4FullFar.smoothReciprocal_eq_inv line 20
  4. lemma OAI.Attempt4FullFar.smoothReciprocal_contDiff line 23
  5. lemma OAI.Attempt4FullFar.smoothReciprocal_deriv_bound line 34