exponentialPDFReal_nonneg — Mathlib

English

The exponential pdf is nonnegative for all x when r > 0.

Русский

Плотность экспоненциального распределения неотрицательна при любых x, если r > 0.

LaTeX

$$$\forall r\in\mathbb{R},\ r>0:\ \forall x\in\mathbb{R}:\ 0 \le \text{exponentialPDFReal}(r,x)$$$

Lean4

/-- The exponential pdf is nonnegative -/
theorem exponentialPDFReal_nonneg {r : ℝ} (hr : 0 < r) (x : ℝ) : 0 ≤ exponentialPDFReal r x :=
  gammaPDFReal_nonneg zero_lt_one hr x

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