truncation_nonneg

Mathlib.Probability.StrongLaw

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.truncation_nonneg

English

For all x, if f(x) ≥ 0 then truncation(f,A)(x) ≥ 0.

Русский

Для всех x верно: если f(x) ≥ 0, то truncation(f,A)(x) ≥ 0.

LaTeX

$$∧_{x} (0 ≤ f(x) ⇒ 0 ≤ truncation(f,A)(x))$$

Lean4

theorem truncation_nonneg {f : α → ℝ} (A : ℝ) {x : α} (h : 0 ≤ f x) : 0 ≤ truncation f A x :=
  Set.indicator_apply_nonneg fun _ => h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru