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 ≤ 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

• MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n = (MeasureTheory.SimpleFunc.nearestPt (fun (k : ℕ) => Nat.casesOn k y₀ (Subtype.val ∘ TopologicalSpace.denseSeq ↑s)) n).comp f hf

@[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) ⋯ s y₀ h₀ n = (MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n).comp 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)

theorem HasCompactSupport.exists_simpleFunc_approx_of_prod {X : Type u_7} {Y : Type u_8} {α : Type u_9} [Zero α] [TopologicalSpace X] [TopologicalSpace Y] [MeasurableSpace X] [MeasurableSpace Y] [OpensMeasurableSpace X] [OpensMeasurableSpace Y] [PseudoMetricSpace α] {f : X × Y → α} (hf : Continuous f) (h'f : HasCompactSupport f) {ε : ℝ} (hε : 0 < ε) : ∃ (g : MeasureTheory.SimpleFunc (X × Y) α), ∀ (x : X × Y), dist (f x) (↑g x) < ε

A continuous function with compact support on a product space can be uniformly approximated by simple functions. The subtlety is that we do not assume that the spaces are separable, so the product of the Borel sigma algebras might not contain all open sets, but still it contains enough of them to approximate compactly supported continuous functions.

theorem HasCompactSupport.measurable_of_prod {X : Type u_7} {Y : Type u_8} {α : Type u_9} [Zero α] [TopologicalSpace X] [TopologicalSpace Y] [MeasurableSpace X] [MeasurableSpace Y] [OpensMeasurableSpace X] [OpensMeasurableSpace Y] [TopologicalSpace α] [TopologicalSpace.PseudoMetrizableSpace α] [MeasurableSpace α] [BorelSpace α] {f : X × Y → α} (hf : Continuous f) (h'f : HasCompactSupport f) : Measurable f

A continuous function with compact support on a product space is measurable for the product sigma-algebra. The subtlety is that we do not assume that the spaces are separable, so the product of the Borel sigma algebras might not contain all open sets, but still it contains enough of them to approximate compactly supported continuous functions.