truncation_eq_of_nonneg — Mathlib

English

If f is nonnegative, truncation(f,A) equals the indicator of Ioc(0,A) composed with f.

Русский

Если f≥0, то truncation(f,A) = (indicator_{Ioc(0,A)} ∘ f).

LaTeX

$$$\operatorname{truncation}(f,A) = (\mathbf{1}_{\mathrm{Ioc}(0,A)} \circ f)$, when $f \ge 0$$$

Lean4

theorem truncation_eq_of_nonneg {f : α → ℝ} {A : ℝ} (h : ∀ x, 0 ≤ f x) :
    truncation f A = indicator (Set.Ioc 0 A) id ∘ f := by
  ext x
  rcases (h x).lt_or_eq with (hx | hx)
  · simp only [truncation, indicator, hx, Set.mem_Ioc, id, Function.comp_apply]
    by_cases h'x : f x ≤ A
    · have : -A < f x := by linarith [h x]
      simp only [this, true_and]
    · simp only [h'x, and_false]
  · simp only [truncation, indicator, hx, id, Function.comp_apply, ite_self]

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