Theorems · Definition · measure theory

MeasureTheory.StronglyMeasurable.approxBounded

{α : Type u_1} →
  {β : Type u_2} →
    {f : α → β} →
      [inst : TopologicalSpace β] →
        {x : MeasurableSpace α} →
          [Norm β] → [SMul ℝ β] → MeasureTheory.StronglyMeasurable f → ℝ → ℕ → MeasureTheory.SimpleFunc α β

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)).

Defined in

Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Cited by

4 results in Mathlib

Foundations

Depth 98 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceNormSMul