integral_pos — Mathlib

English

Let f be a ContDiffBump. Then the integral of its normed version equals 1: ∫ f.normed μ x dμ(x) = 1.

Русский

Пусть f — ContDiffBump. Тогда интеграл нормированной функции равен единице: ∫ f.normed μ(x) dμ(x) = 1.

LaTeX

$$$ \int_E f.normed\mu(x) \, d\mu(x) = 1 $$$

Lean4

theorem integral_pos : 0 < ∫ x, f x ∂μ :=
  by
  refine (integral_pos_iff_support_of_nonneg f.nonneg' f.integrable).mpr ?_
  rw [f.support_eq]
  exact measure_ball_pos μ c f.rOut_pos

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