exponentialPDFReal_pos — Mathlib

English

The exponential pdf is positive for all positive rates and arguments: if hr>0 and hx>0 then 0 < exponentialPDFReal hr hx.

Русский

Плотность экспоненциального распределения положительна при всех положительных значениях скорости и аргументов: если hr>0 и hx>0, то 0 < exponentialPDFReal(hr, hx).

LaTeX

$$$ (hr>0) \land (hx>0) \Rightarrow 0 < \text{exponentialPDFReal}(hr, hx) $$$

Lean4

/-- The exponential pdf is positive for all positive reals -/
theorem exponentialPDFReal_pos {x r : ℝ} (hr : 0 < r) (hx : 0 < x) : 0 < exponentialPDFReal r x :=
  gammaPDFReal_pos zero_lt_one hr hx

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