OAI/Geometry/RCD/Coordinates/DyadicRadialFitEstimates.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Estimates for one canonical dyadic radial-fit sequence

  1. def OAI.RegularPointCoordinates.radialFitStepConstant line 15
  2. def OAI.RegularPointCoordinates.radialFitQualitativeConstant line 21
  3. theorem OAI.RegularPointCoordinates.radialFitStepConstant_nonneg line 25
  4. theorem OAI.RegularPointCoordinates.radialFitQualitativeConstant_nonneg line 30
  5. theorem OAI.RegularPointCoordinates.dyadicRadialFit_step line 46
  6. theorem OAI.RegularPointCoordinates.dyadicRadialFit_smallness line 85