integrable_pow_mul — Mathlib

English

A bound for the integral of |x|^k times the norm of the iterated Fréchet derivative, expressed via a seminorm bound.

Русский

Ограничение на интеграл от |x|^k умноженного на норму подвергнутого повторному дифференцированию итератора Фреше через некую семинорму.

LaTeX

$$$\int \|x\|^k \|\mathrm{iteratedFDeriv}\,ℝ\, n\ f\ x\| \, dμ ≤ 2^{μ.integrablePower} \cdot \left( \int (1+\|x\|)^{-(μ.integrablePower)} \, dμ(x) \right) \cdot (SchwartzMap.seminorm 𝕜 0 n f + SchwartzMap.seminorm 𝕜 (k+μ.integrablePower) n f)$$$

Lean4

theorem integrable_pow_mul (f : 𝓢(D, V)) (k : ℕ) : Integrable (fun x ↦ ‖x‖ ^ k * ‖f x‖) μ :=
  by
  convert integrable_pow_mul_iteratedFDeriv μ f k 0 with x
  simp

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