Documentation

Mathlib.MeasureTheory.Function.SimpleFuncDense

Density of simple functions #

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

Main definitions #

Main results #

Notations #

Pointwise approximation by simple functions #

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
Instances For

    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
    Instances For
      theorem MeasureTheory.SimpleFunc.nearestPtInd_succ {α : Type u_1} [MeasurableSpace α] [PseudoEMetricSpace α] [OpensMeasurableSpace α] (e : α) (N : ) (x : α) :
      (MeasureTheory.SimpleFunc.nearestPtInd e (N + 1)) x = if kN, edist (e (N + 1)) x < edist (e k) x then N + 1 else (MeasureTheory.SimpleFunc.nearestPtInd e N) x
      theorem MeasureTheory.SimpleFunc.edist_nearestPt_le {α : Type u_1} [MeasurableSpace α] [PseudoEMetricSpace α] [OpensMeasurableSpace α] (e : α) (x : α) {k : } {N : } (hk : k N) :
      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 : ) :

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

      Equations
      Instances For
        @[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.

        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.