English
Fix a sequence i: N → β. For a function f: α → β, the n-th approximation by simple functions is defined as the supremum (over k < n) of the constant β-valued functions on the sets where i_k ≤ f, i.e. (approx i f n)(a) = sup{ i_k : k < n and i_k ≤ f(a) } with the convention that the supremum of the empty set is 0.
Русский
Пусть i: ℕ → β, f: α → β. Приближение функции f на n-й ступени — это супремум по k < n константных функций на множествах {a : α | i_k ≤ f(a)}: (approx i f n)(a) = sup{ i_k : k < n и i_k ≤ f(a) }, при пустом множестве берём 0.
LaTeX
$$$ (\text{approx } i f n)(a) = \sup_{0 \le k < n} \{ i_k : i_k \le f(a) \} = \sup_{0 \le k < n}(\text{if } i_k \le f(a) \text{ then } i_k \text{ else } 0) $$$
Lean4
/-- Fix a sequence `i : ℕ → β`. Given a function `α → β`, its `n`-th approximation
by simple functions is defined so that in case `β = ℝ≥0∞` it sends each `a` to the supremum
of the set `{i k | k ≤ n ∧ i k ≤ f a}`, see `approx_apply` and `iSup_approx_apply` for details. -/
def approx (i : ℕ → β) (f : α → β) (n : ℕ) : α →ₛ β :=
(Finset.range n).sup fun k => restrict (const α (i k)) {a : α | i k ≤ f a}
