theorem
SimpleApproximation.eapprox_ge_ennrealRatEmbed
{X : Type u_1}
[MeasurableSpace X]
{f : X → ENNReal}
(hf : Measurable f)
{k n : ℕ}
(hk : k < n)
(x : X)
(h : MeasureTheory.SimpleFunc.ennrealRatEmbed k ≤ f x)
:
At any point x where the k-th rational test value r_k satisfies
r_k ≤ f x, the standard eapprox simple-function approximation at stage
n > k also satisfies r_k ≤ eapprox f n x.
theorem
SimpleApproximation.eapprox_ge_of_rational
{X : Type u_1}
[MeasurableSpace X]
{f : X → ENNReal}
(hf : Measurable f)
(q : ℚ)
(x : X)
(hqf : ↑(↑q).toNNReal ≤ f x)
{n : ℕ}
(hn : Encodable.encode q < n)
:
A rational lower bound on f x is preserved by the standard simple-function
approximation eapprox f n once n exceeds the encoding index of the
rational.
theorem
SimpleApproximation.eapprox_uniform_on_bounded
{X : Type u_1}
[MeasurableSpace X]
{f : X → ENNReal}
(hf : Measurable f)
(M : NNReal)
{ε : ENNReal}
(hε : 0 < ε)
:
Uniform ε-approximation of a measurable [0, ∞]-valued function f
on the set where f ≤ M: there is an N such that for all n ≥ N, every
point x with f x ≤ M satisfies f x − eapprox f n x ≤ ε.
theorem
SimpleApproximation.exists_monotone_simple_approx_uniform
{X : Type u_1}
[MeasurableSpace X]
{f : X → ENNReal}
(hf : Measurable f)
:
∃ (g : ℕ → X → ENNReal),
(∀ (n : ℕ), Measurable (g n)) ∧ (∀ (n : ℕ), (Set.range (g n)).Finite) ∧ (∀ (n : ℕ) (x : X), g n x ≤ g (n + 1) x) ∧ (∀ (x : X), Filter.Tendsto (fun (n : ℕ) => g n x) Filter.atTop (nhds (f x))) ∧ ∀ (M : NNReal) {ε : ENNReal}, 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∀ (x : X), f x ≤ ↑M → f x - g n x ≤ ε
Melrose Prop. 3.3 (Simple approximation): every measurable [0, ∞]-valued
function f is the pointwise limit of an increasing sequence of measurable
simple functions, with uniform approximation on every set {f ≤ M}.