paretoPDFReal_nonneg — Mathlib

English

The Pareto pdf is nonnegative for all t, r, x with t≥0, r≥0.

Русский

Плотность Парето неотрицательна для всех t≥0, r≥0, x.

LaTeX

$$$0 \\le \\mathrm{paretoPDFReal}(t,r,x)$$$

Lean4

/-- The Pareto pdf is nonnegative. -/
theorem paretoPDFReal_nonneg (ht : 0 ≤ t) (hr : 0 ≤ r) (x : ℝ) : 0 ≤ paretoPDFReal t r x :=
  by
  unfold paretoPDFReal
  split_ifs with h
  ·
    cases le_iff_eq_or_lt.1 ht with
    | inl ht0 =>
      rw [← ht0] at h
      positivity
    | inr htp =>
      have := lt_of_lt_of_le htp h
      positivity
  · positivity

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