integrable_normed

Mathlib.Analysis.Calculus.BumpFunction.Normed

URI: https://scilib.ai/kg/mathlib#ContDiffBump.integrable_normed

English

For f a ContDiffBump, f.normed μ is integrable with respect to μ.

Русский

Для f — ContDiffBump, f.normed μ интегрируема по мере μ.

LaTeX

$$$ \int_E |f.normed\mu(x)| \, d\mu(x) < \infty $$$

Lean4

protected theorem integrable_normed : Integrable (f.normed μ) μ :=
  f.integrable.div_const _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru