iInf_le_lintegral — Mathlib

English

For a probability measure μ, the infimum of f over α is less than or equal to the lintegral of f.

Русский

Для вероятностной меры μ инфимум функции f по пространству не превышает линегральный интеграл.

LaTeX

$$$$\\inf_{x} f(x) \\le \\int f \\, d\\mu.$$$$

Lean4

theorem iInf_le_lintegral [IsProbabilityMeasure μ] (f : α → ℝ≥0∞) : ⨅ x, f x ≤ ∫⁻ x, f x ∂μ :=
  le_trans (by simp) (iInf_mul_le_lintegral f)

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