nonneg_normed

Mathlib.Analysis.Calculus.BumpFunction.Normed

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

English

The normed bump is defined by dividing the bump by its integral.

Русский

Нормированное bump определяется как отношение подиганной функции к ее интегралу.

LaTeX

$$f.normed μ x = f x / ∫ f$$

Lean4

theorem nonneg_normed (x : E) : 0 ≤ f.normed μ x :=
  div_nonneg f.nonneg <| integral_nonneg f.nonneg'

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

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

Разделы

Аффилиация

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