integrable_pow_mul_iteratedFDeriv

English

The integral over the domain defines a continuous linear map from Schwartz maps 𝓢(D,V) to V, provided temperate growth bounds hold.

Русский

Интеграл по области задаёт непрерывно линейное отображение от Schwartz(D,V) в V при соблюдении ограничений темпериатного роста.

LaTeX

$$$integralCLM : 𝓢(D, V) \toL V$$$

Lean4

theorem integrable_pow_mul_iteratedFDeriv (f : 𝓢(D, V)) (k n : ℕ) :
    Integrable (fun x ↦ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖) μ :=
  integrable_of_le_of_pow_mul_le (norm_iteratedFDeriv_le_seminorm ℝ _ _) (le_seminorm ℝ _ _ _)
    ((f.smooth ⊤).continuous_iteratedFDeriv (mod_cast le_top)).aestronglyMeasurable

Похожие утверждения