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