Density of simple functions

Show that each Borel measurable function can be approximated pointwise by a sequence of simple functions.

Main definitions

• MeasureTheory.SimpleFunc.nearestPt (e : ℕ → α) (N : ℕ) : α →ₛ ℕ: the SimpleFunc sending each x : α to the point e k which is the nearest to x among e 0, ..., e N.
• MeasureTheory.SimpleFunc.approxOn (f : β → α) (hf : Measurable f) (s : Set α) (y₀ : α) (h₀ : y₀ ∈ s) [SeparableSpace s] (n : ℕ) : β →ₛ α : a simple function that takes values in s and approximates f.

Main results

• tendsto_approxOn (pointwise convergence): If f x ∈ s, then the sequence of simple approximations MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n, evaluated at x, tends to f x as n tends to ∞.

Notations

• α →ₛ β (local notation): the type of simple functions α → β.

Pointwise approximation by simple functions

noncomputable def MeasureTheory.SimpleFunc.nearestPtInd {α : Type u_1} [MeasurableSpace α] [PseudoEMetricSpace α] [OpensMeasurableSpace α] (e : ℕ → α) : ℕ → MeasureTheory.SimpleFunc α ℕ

nearestPtInd e N x is the index k such that e k is the nearest point to x among the points e 0, ..., e N. If more than one point are at the same distance from x, then nearestPtInd e N x returns the least of their indexes.

Equations

• One or more equations did not get rendered due to their size.
• MeasureTheory.SimpleFunc.nearestPtInd e 0 = MeasureTheory.SimpleFunc.const α 0

noncomputable def MeasureTheory.SimpleFunc.nearestPt {α : Type u_1} [MeasurableSpace α] [PseudoEMetricSpace α] [OpensMeasurableSpace α] (e : ℕ → α) (N : ℕ) : MeasureTheory.SimpleFunc α α

nearestPt e N x is the nearest point to x among the points e 0, ..., e N. If more than one point are at the same distance from x, then nearestPt e N x returns the point with the least possible index.

Equations

• MeasureTheory.SimpleFunc.nearestPt e N = MeasureTheory.SimpleFunc.map e (MeasureTheory.SimpleFunc.nearestPtInd e N)

@[simp]

theorem MeasureTheory.SimpleFunc.nearestPtInd_zero {α : Type u_1} [MeasurableSpace α] [PseudoEMetricSpace α] [OpensMeasurableSpace α] (e : ℕ → α) : MeasureTheory.SimpleFunc.nearestPtInd e 0 = MeasureTheory.SimpleFunc.const α 0

@[simp]

theorem MeasureTheory.SimpleFunc.nearestPt_zero {α : Type u_1} [MeasurableSpace α] [PseudoEMetricSpace α] [OpensMeasurableSpace α] (e : ℕ → α) : MeasureTheory.SimpleFunc.nearestPt e 0 = MeasureTheory.SimpleFunc.const α (e 0)

theorem MeasureTheory.SimpleFunc.nearestPtInd_succ {α : Type u_1} [MeasurableSpace α] [PseudoEMetricSpace α] [OpensMeasurableSpace α] (e : ℕ → α) (N : ℕ) (x : α) : ↑(MeasureTheory.SimpleFunc.nearestPtInd e (N + 1)) x = if ∀ (k : ℕ), k ≤ N → edist (e (N + 1)) x < edist (e k) x then N + 1 else ↑(MeasureTheory.SimpleFunc.nearestPtInd e N) x

theorem MeasureTheory.SimpleFunc.nearestPtInd_le {α : Type u_1} [MeasurableSpace α] [PseudoEMetricSpace α] [OpensMeasurableSpace α] (e : ℕ → α) (N : ℕ) (x : α) : ↑(MeasureTheory.SimpleFunc.nearestPtInd e N) x ≤ N

theorem MeasureTheory.SimpleFunc.edist_nearestPt_le {α : Type u_1} [MeasurableSpace α] [PseudoEMetricSpace α] [OpensMeasurableSpace α] (e : ℕ → α) (x : α) {k : ℕ} {N : ℕ} (hk : k ≤ N) : edist (↑(MeasureTheory.SimpleFunc.nearestPt e N) x) x ≤ edist (e k) x

theorem MeasureTheory.SimpleFunc.tendsto_nearestPt {α : Type u_1} [MeasurableSpace α] [PseudoEMetricSpace α] [OpensMeasurableSpace α] {e : ℕ → α} {x : α} (hx : x ∈ closure (Set.range e)) : Filter.Tendsto (fun N => ↑(MeasureTheory.SimpleFunc.nearestPt e N) x) Filter.atTop (nhds x)

noncomputable def MeasureTheory.SimpleFunc.approxOn {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [PseudoEMetricSpace α] [OpensMeasurableSpace α] [MeasurableSpace β] (f : β → α) (hf : Measurable f) (s : Set α) (y₀ : α) (h₀ : y₀ ∈ s) [TopologicalSpace.SeparableSpace ↑s] (n : ℕ) : MeasureTheory.SimpleFunc β α

Approximate a measurable function by a sequence of simple functions F n such that F n x ∈ s.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MeasureTheory.SimpleFunc.approxOn_zero {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [PseudoEMetricSpace α] [OpensMeasurableSpace α] [MeasurableSpace β] {f : β → α} (hf : Measurable f) {s : Set α} {y₀ : α} (h₀ : y₀ ∈ s) [TopologicalSpace.SeparableSpace ↑s] (x : β) : ↑(MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ 0) x = y₀

theorem MeasureTheory.SimpleFunc.approxOn_mem {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [PseudoEMetricSpace α] [OpensMeasurableSpace α] [MeasurableSpace β] {f : β → α} (hf : Measurable f) {s : Set α} {y₀ : α} (h₀ : y₀ ∈ s) [TopologicalSpace.SeparableSpace ↑s] (n : ℕ) (x : β) : ↑(MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n) x ∈ s

@[simp]

theorem MeasureTheory.SimpleFunc.approxOn_comp {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [PseudoEMetricSpace α] [OpensMeasurableSpace α] [MeasurableSpace β] {γ : Type u_7} [MeasurableSpace γ] {f : β → α} (hf : Measurable f) {g : γ → β} (hg : Measurable g) {s : Set α} {y₀ : α} (h₀ : y₀ ∈ s) [TopologicalSpace.SeparableSpace ↑s] (n : ℕ) : MeasureTheory.SimpleFunc.approxOn (f ∘ g) (_ : Measurable (f ∘ g)) s y₀ h₀ n = MeasureTheory.SimpleFunc.comp (MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n) g hg

theorem MeasureTheory.SimpleFunc.tendsto_approxOn {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [PseudoEMetricSpace α] [OpensMeasurableSpace α] [MeasurableSpace β] {f : β → α} (hf : Measurable f) {s : Set α} {y₀ : α} (h₀ : y₀ ∈ s) [TopologicalSpace.SeparableSpace ↑s] {x : β} (hx : f x ∈ closure s) : Filter.Tendsto (fun n => ↑(MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n) x) Filter.atTop (nhds (f x))

theorem MeasureTheory.SimpleFunc.edist_approxOn_mono {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [PseudoEMetricSpace α] [OpensMeasurableSpace α] [MeasurableSpace β] {f : β → α} (hf : Measurable f) {s : Set α} {y₀ : α} (h₀ : y₀ ∈ s) [TopologicalSpace.SeparableSpace ↑s] (x : β) {m : ℕ} {n : ℕ} (h : m ≤ n) : edist (↑(MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n) x) (f x) ≤ edist (↑(MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ m) x) (f x)

theorem MeasureTheory.SimpleFunc.edist_approxOn_le {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [PseudoEMetricSpace α] [OpensMeasurableSpace α] [MeasurableSpace β] {f : β → α} (hf : Measurable f) {s : Set α} {y₀ : α} (h₀ : y₀ ∈ s) [TopologicalSpace.SeparableSpace ↑s] (x : β) (n : ℕ) : edist (↑(MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n) x) (f x) ≤ edist y₀ (f x)

theorem MeasureTheory.SimpleFunc.edist_approxOn_y0_le {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [PseudoEMetricSpace α] [OpensMeasurableSpace α] [MeasurableSpace β] {f : β → α} (hf : Measurable f) {s : Set α} {y₀ : α} (h₀ : y₀ ∈ s) [TopologicalSpace.SeparableSpace ↑s] (x : β) (n : ℕ) : edist y₀ (↑(MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n) x) ≤ edist y₀ (f x) + edist y₀ (f x)