EuclideanGevreyCutoff.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Euclidean Gevrey cutoffs of order two

L. Hörmander, Between distributions and hyperfunctions, Astérisque 131 (1985), pp. 89–106, §2, equations (2.2) and (2.6), p. 90, describes nonquasianalytic Gevrey classes containing compactly supported functions. Squaring a nonzero bump and convolving its normalized dilation with a ball indicator gives a fixed core and support. Equivalence of coordinate and finite-dimensional multilinear derivative bounds changes only the exponential constant.

https://numdam.org/item/AST_1985__131__89_0.pdf

structure OAI.RegularPointCoordinates.EuclideanGevreyCutoff line 28
Source documentation
A single fixed radial-scale cutoff with all-order Gevrey-two bounds.
```
structure EuclideanGevreyCutoff (n : ℕ) where
…
```
def OAI.RegularPointCoordinates.EuclideanGevreyCutoffInput line 41
Source documentation
The precise compact Gevrey specialization needed by the chart proof.
```
def EuclideanGevreyCutoffInput (n : ℕ) : Prop := Nonempty (EuclideanGevreyCutoff n)
```
Mentions: OAI.RegularPointCoordinates.EuclideanGevreyCutoff

theorem OAI.RegularPointCoordinates.EuclideanGevreyCutoff.affine_jet_le line 45

Source documentation

A fixed affine change preserves the Gevrey order. The base records the actual operator norm, while the derivative order remains unrestricted.

theorem EuclideanGevreyCutoff.affine_jet_le {n : ℕ} (psi : EuclideanGevreyCutoff n)
    (L : Euclidean n →L[ℝ] Euclidean n) (a z : Euclidean n) (m : ℕ)
    {M : ℝ} (hM : 1 ≤ M) (hL : ‖L‖ ≤ M) :
    ‖iteratedFDeriv ℝ m (fun w => psi.value (a + L w)) z‖ ≤
      (psi.constant * M) ^ (m + 1) * (m.factorial : ℝ) ^ 2 := by
…

Mentions: OAI.RegularPointCoordinates.EuclideanGevreyCutoff, OAI.RegularPointCoordinates.Euclidean