GevreyConvolution.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform derivative bounds for a compactly supported convolution

The derivative is placed on the smooth compactly supported factor. The constant is the L¹ norm of the other factor and is independent of the derivative order. This is the estimate used to give the Gevrey bump a plateau.

theorem OAI.RegularPointCoordinates.norm_iteratedFDeriv_convolution_le line 22

Source documentation

A uniform derivative bound passes through convolution with one fixed integrable scalar function. All vector spaces here are in the same universe as the finite-dimensional Euclidean application.

theorem norm_iteratedFDeriv_convolution_le
    (n : ℕ) {E F G : Type} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    [NormedAddCommGroup G] [NormedSpace ℝ G]
    [MeasurableSpace E] [BorelSpace E] {μ : Measure E}
    [SFinite μ] [μ.IsAddLeftInvariant]
    (L : ℝ →L[ℝ] F →L[ℝ] G) {f : E → ℝ} {g : E → F}
    (hf : Integrable f μ) (hg : ContDiff ℝ ∞ g) (hgc : HasCompactSupport g)
    {M : ℝ} (hM : 0 ≤ M) (hb : ∀ x, ‖iteratedFDeriv ℝ n g x‖ ≤ M) (x : E) :
    ‖iteratedFDeriv ℝ n (f ⋆[L, μ] g) x‖ ≤
      ‖L‖ * M * ∫ y, ‖f y‖ ∂μ := by
…