OAI/MeasureTheory/Falconer/Angular/ControlledCapPartition.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A smooth cap partition with controlled number and overlap

The ambient-dimensional count is sufficient for summing arbitrary-power errors. The positive retained-graph estimate uses the partition identity and therefore incurs no cap-count factor.

The partition is smooth in every adapted chart.

  1. theorem OAI.Falconer.controlled_smooth_cap_partition line 20