GevreyCutoffConstruction.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Construction of a Euclidean Gevrey cutoff

Convolve the normalized small Gevrey bump with the indicator of the radius-5/2 ball. The resulting function is one on the radius-two ball, vanishes outside radius three, and retains the order-two derivative bound. This constructs the exact cutoff used in the chart iteration.

theorem OAI.RegularPointCoordinates.euclideanGevreyCutoffInput line 23
Source documentation
The compact Gevrey input is constructed in every finite dimension.
```
theorem euclideanGevreyCutoffInput (n : ℕ) : EuclideanGevreyCutoffInput n := by
…
```
Mentions: OAI.RegularPointCoordinates.EuclideanGevreyCutoffInput