condCDF_nonneg — Mathlib

English

For any ρ, a, and r, the conditional CDF is nonnegative: condCDF ρ a r ≥ 0.

Русский

Для любых ρ, a и r условная функция распределения неотрицательна: condCDF ρ a r ≥ 0.

LaTeX

$$$0 \\leq condCDF(ρ,a,r).$$$

Lean4

/-- The conditional cdf is non-negative for all `a : α`. -/
theorem condCDF_nonneg (ρ : Measure (α × ℝ)) (a : α) (r : ℝ) : 0 ≤ condCDF ρ a r :=
  stieltjesOfMeasurableRat_nonneg _ a r

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