approxBounded — Mathlib

English

There is an equality between approxBounded and a map of approx with a bounded multiplier, for normed spaces.

Русский

Существует равенство между approxBounded и отображением из approx с ограниченным множителем для нормируемых пространств.

LaTeX

$$$\\text{hf.approxBounded } c\; n = \\text{SimpleFunc.map} (x\\mapsto \\min 1 (c/\\|x\\|)) \\; (hf.approx n)$$$

Lean4

/-- Similar to `stronglyMeasurable.approx`, but enforces that the norm of every function in the
sequence is less than `c` everywhere. If `‖f x‖ ≤ c` this sequence of simple functions verifies
`Tendsto (fun n => hf.approxBounded n x) atTop (𝓝 (f x))`. -/
noncomputable def approxBounded {_ : MeasurableSpace α} [Norm β] [SMul ℝ β] (hf : StronglyMeasurable f) (c : ℝ) :
    ℕ → SimpleFunc α β := fun n => (hf.approx n).map fun x => min 1 (c / ‖x‖) • x

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