u_int_pos — Mathlib

English

Let E be a finite-dimensional real normed space and let μ be a Haar measure on E. If u is a nonnegative continuous bump with compact support, then the integral of u over E with respect to μ is strictly positive.

Русский

Пусть E – конечномерное вещественное нормированное пространство и μ – гауссовская (гаромовская) мера на E. Пусть u — неотрицательная непрерывная функция-бум с компактной опорой. Тогда интеграл u по μ равен положительному числу.

LaTeX

$$$0 < \\int_E u(x) \\, d\\mu(x)$$$

Lean4

theorem u_int_pos : 0 < ∫ x : E, u x ∂μ :=
  by
  refine (integral_pos_iff_support_of_nonneg u_nonneg ?_).mpr ?_
  · exact (u_continuous E).integrable_of_hasCompactSupport (u_compact_support E)
  · rw [u_support]; exact measure_ball_pos _ _ zero_lt_one

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