OAI/MeasureTheory/Falconer/Angular/CapCoordinates.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Small sphere caps have small gnomonic coordinates

This estimate converts the geometric cap support of an angular partition into the compact coordinate support required by nonstationary integration.

  1. theorem OAI.Falconer.small_cap_chart_displacement line 15