integrable

Mathlib.Analysis.Calculus.BumpFunction.Normed

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

English

Let f be a ContDiffBump. Then f is integrable with respect to μ on E, i.e., ∫ f dμ < ∞.

Русский

Пусть f — ContDiffBump. Тогда f интегрируема по мере μ на E, то есть ∫ f dμ < ∞.

LaTeX

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

Lean4

protected theorem integrable : Integrable f μ :=
  f.continuous.integrable_of_hasCompactSupport f.hasCompactSupport

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

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

Разделы

Аффилиация

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