Approximation by simple functions

TheoremThe standard simple approximations converge uniformly where the function is bounded#✓fully proved

Let \(\alpha\) be a measurable space and \(f : \alpha \to [0, \infty]\) a measurable function. Let \(r_0, r_1, \ldots\) be the fixed enumeration of \(\mathbb{Q}\) by natural-number codes (\(r_k = 0\) when \(k\) codes no rational), put \(q_k = \max(r_k, 0)\), and let \(\varphi_n(a) = \max(\{0\} \cup \{q_k : k < n,\ q_k \le f(a)\})\) be the \(n\)-th standard simple approximation of \(f\). Then for every \(B \in [0, \infty)\) and every \(\varepsilon \in (0, \infty]\) there is \(N \in \mathbb{N}\) such that \(f(a) - \varphi_n(a) < \varepsilon\) for all \(n \ge N\) and all \(a \in \alpha\) with \(f(a) \le B\), where subtraction in \([0, \infty]\) is truncated at \(0\).

theorem eapprox_sub_lt_of_le
    {α : Type*} [MeasurableSpace α] {f : α → ℝ≥0∞} (hf : Measurable f)
    {B ε : ℝ≥0∞} (hB : B ≠ ⊤) (hε : ε ≠ 0) :
    ∃ N : ℕ, ∀ n ≥ N, ∀ a, f a ≤ B → f a - SimpleFunc.eapprox f n a < ε

Used by 1

Used byApproximation of nonnegative measurable functions by simple functions

TheoremApproximation of nonnegative measurable functions by simple functions#✓fully proved

Let \(\alpha\) be a measurable space and \(f : \alpha \to [0, \infty]\) a measurable function. There is a sequence of simple functions \(\varphi_n : \alpha \to [0, \infty]\) (\(n \in \mathbb{N}\)) such that: (a) \(\varphi_0 \le \varphi_1 \le \cdots \le f\) pointwise; (b) \(\varphi_n(a) \to f(a)\) for every \(a \in \alpha\); and (c) for every \(B \in [0, \infty)\) and every \(\varepsilon \in (0, \infty]\) there is \(N \in \mathbb{N}\) such that \(f(a) - \varphi_n(a) < \varepsilon\) for all \(n \ge N\) and all \(a \in \alpha\) with \(f(a) \le B\), where the subtraction in \([0, \infty]\) is truncated at \(0\).

theorem exists_monotone_tendsto
    {α : Type*} [MeasurableSpace α] {f : α → ℝ≥0∞} (hf : Measurable f) :
    ∃ φ : ℕ → SimpleFunc α ℝ≥0∞,
      ((∀ n a, φ n a ≤ f a) ∧ (Monotone fun n => (φ n : α → ℝ≥0∞))) ∧
      (∀ a, Tendsto (fun n => φ n a) atTop (𝓝 (f a))) ∧
      (∀ B : ℝ≥0∞, B ≠ ⊤ → ∀ ε : ℝ≥0∞, ε ≠ 0 →
        ∃ N : ℕ, ∀ n ≥ N, ∀ a, f a ≤ B → f a - φ n a < ε)

Uses 1

Proof usesThe standard simple approximations converge uniformly where the function is bounded

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.