w_integral

Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

URI: https://scilib.ai/kg/mathlib#ExistsContDiffBumpBase.w_integral

← MathLib Explorer

English

For D>0, the integral of w(D,·) over E equals 1.

Русский

При D>0 интеграл по E от w(D,·) равен 1.

LaTeX

$$\\int_E w(D,x)\\, d\\mu(x) = 1, \\quad D>0$$

Lean4

theorem w_integral {D : ℝ} (Dpos : 0 < D) : ∫ x : E, w D x ∂μ = 1 :=
  by
  simp_rw [w, integral_smul]
  rw [integral_comp_inv_smul_of_nonneg μ (u : E → ℝ) Dpos.le, abs_of_nonneg Dpos.le, mul_comm]
  simp [field, (u_int_pos E).ne']

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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