GevreyCompactBump.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

A compact Euclidean Gevrey bump

Products of affine copies of the flat exponential give a nonnegative Gevrey-two function, positive at the origin, supported in a fixed small ball. No existence theorem for Gevrey functions is assumed.

theorem OAI.RegularPointCoordinates.factorial_product_le line 20

theorem OAI.RegularPointCoordinates.gevreyTwo_mul_bound line 37

Source documentation

The product estimate used to assemble the coordinate bump.

theorem gevreyTwo_mul_bound {f g : E → ℝ} {A : ℝ} (hA : 1 ≤ A)
    (hf : ContDiff ℝ ∞ f) (hg : ContDiff ℝ ∞ g)
    (hfb : ∀ m x, ‖iteratedFDeriv ℝ m f x‖ ≤ A ^ (m + 1) * (m.factorial : ℝ) ^ 2)
    (hgb : ∀ m x, ‖iteratedFDeriv ℝ m g x‖ ≤ A ^ (m + 1) * (m.factorial : ℝ) ^ 2)
    (m : ℕ) (x : E) :
    ‖iteratedFDeriv ℝ m (fun y => f y * g y) x‖ ≤
      (2 * A ^ 2) ^ (m + 1) * (m.factorial : ℝ) ^ 2 := by
…

theorem OAI.RegularPointCoordinates.exists_gevreyTwo_prod_bound line 72

Source documentation

Finite products preserve the all-order bounds needed here.

theorem exists_gevreyTwo_prod_bound {ι : Type*} (s : Finset ι) (f : ι → E → ℝ)
    (hf : ∀ i ∈ s, ContDiff ℝ ∞ (f i))
    (hb : ∀ i ∈ s, ∃ A : ℝ, 1 ≤ A ∧ ∀ m x,
      ‖iteratedFDeriv ℝ m (f i) x‖ ≤ A ^ (m + 1) * (m.factorial : ℝ) ^ 2) :
    ∃ A : ℝ, 1 ≤ A ∧ ∀ m x,
      ‖iteratedFDeriv ℝ m (fun y => ∏ i ∈ s, f i y) x‖ ≤
        A ^ (m + 1) * (m.factorial : ℝ) ^ 2 := by
…

theorem OAI.RegularPointCoordinates.exists_gevreyTwo_affine_glue_bound line 105

Source documentation

An affine flat exponential has a Gevrey-two bound.

theorem exists_gevreyTwo_affine_glue_bound (L : E →L[ℝ] ℝ) (a : ℝ) :
    ∃ A : ℝ, 1 ≤ A ∧ ∀ m x,
      ‖iteratedFDeriv ℝ m (fun y => expNegInvGlue (a + L y)) x‖ ≤
        A ^ (m + 1) * (m.factorial : ℝ) ^ 2 := by
…

theorem OAI.RegularPointCoordinates.exists_small_gevreyTwo_bump line 128

Source documentation

A nonnegative compact bump with Gevrey-two jets and support in radius 1/4.

theorem exists_small_gevreyTwo_bump (n : ℕ) :
    ∃ b : EuclideanSpace ℝ (Fin n) → ℝ, ContDiff ℝ ∞ b ∧
      (∀ x, 0 ≤ b x) ∧ 0 < b 0 ∧ tsupport b ⊆ closedBall 0 (1 / 4) ∧
      ∃ A : ℝ, 1 ≤ A ∧ ∀ m x,
        ‖iteratedFDeriv ℝ m b x‖ ≤ A ^ (m + 1) * (m.factorial : ℝ) ^ 2 := by
…