truncation_eq_self

Mathlib.Probability.StrongLaw

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

← MathLib Explorer

English

If |f(x)| < A, then truncation(f,A)(x) = f(x).

Русский

Если |f(x)| < A, то truncation(f,A)(x) = f(x).

LaTeX

$$$|f(x)| < A \Rightarrow \operatorname{truncation}(f,A)(x) = f(x)$$$

Lean4

theorem truncation_eq_self {f : α → ℝ} {A : ℝ} {x : α} (h : |f x| < A) : truncation f A x = f x :=
  by
  simp only [truncation, indicator, id, Function.comp_apply, ite_eq_left_iff]
  intro H
  apply H.elim
  simp [(abs_lt.1 h).1, (abs_lt.1 h).2.le]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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