Documentation

Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Density of simple functions #

Show that each Lᵖ Borel measurable function can be approximated in Lᵖ norm by a sequence of simple functions.

Main definitions #

Main results #

TODO #

For E finite-dimensional, simple functions α →ₛ E are dense in L^∞ -- prove this.

Notations #

Lp approximation by simple functions #

theorem MeasureTheory.SimpleFunc.nnnorm_approxOn_le {β : Type u_2} {E : Type u_4} [MeasurableSpace β] [MeasurableSpace E] [NormedAddCommGroup E] [OpensMeasurableSpace E] {f : βE} (hf : Measurable f) {s : Set E} {y₀ : E} (h₀ : y₀ s) [TopologicalSpace.SeparableSpace s] (x : β) (n : ) :
(MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n) x - f x‖₊ f x - y₀‖₊
theorem MeasureTheory.SimpleFunc.norm_approxOn_y₀_le {β : Type u_2} {E : Type u_4} [MeasurableSpace β] [MeasurableSpace E] [NormedAddCommGroup E] [OpensMeasurableSpace E] {f : βE} (hf : Measurable f) {s : Set E} {y₀ : E} (h₀ : y₀ s) [TopologicalSpace.SeparableSpace s] (x : β) (n : ) :
(MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n) x - y₀ f x - y₀ + f x - y₀
theorem MeasureTheory.SimpleFunc.norm_approxOn_zero_le {β : Type u_2} {E : Type u_4} [MeasurableSpace β] [MeasurableSpace E] [NormedAddCommGroup E] [OpensMeasurableSpace E] {f : βE} (hf : Measurable f) {s : Set E} (h₀ : 0 s) [TopologicalSpace.SeparableSpace s] (x : β) (n : ) :
theorem MeasureTheory.SimpleFunc.tendsto_approxOn_Lp_snorm {β : Type u_2} {E : Type u_4} [MeasurableSpace β] [MeasurableSpace E] [NormedAddCommGroup E] {p : ENNReal} [OpensMeasurableSpace E] {f : βE} (hf : Measurable f) {s : Set E} {y₀ : E} (h₀ : y₀ s) [TopologicalSpace.SeparableSpace s] (hp_ne_top : p ) {μ : MeasureTheory.Measure β} (hμ : ∀ᵐ (x : β) ∂μ, f x closure s) (hi : MeasureTheory.snorm (fun (x : β) => f x - y₀) p μ < ) :
Filter.Tendsto (fun (n : ) => MeasureTheory.snorm ((MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n) - f) p μ) Filter.atTop (nhds 0)
theorem MeasureTheory.SimpleFunc.memℒp_approxOn {β : Type u_2} {E : Type u_4} [MeasurableSpace β] [MeasurableSpace E] [NormedAddCommGroup E] {p : ENNReal} [BorelSpace E] {f : βE} {μ : MeasureTheory.Measure β} (fmeas : Measurable f) (hf : MeasureTheory.Memℒp f p μ) {s : Set E} {y₀ : E} (h₀ : y₀ s) [TopologicalSpace.SeparableSpace s] (hi₀ : MeasureTheory.Memℒp (fun (x : β) => y₀) p μ) (n : ) :
theorem MeasureTheory.SimpleFunc.tendsto_approxOn_range_Lp_snorm {β : Type u_2} {E : Type u_4} [MeasurableSpace β] [MeasurableSpace E] [NormedAddCommGroup E] {p : ENNReal} [BorelSpace E] {f : βE} (hp_ne_top : p ) {μ : MeasureTheory.Measure β} (fmeas : Measurable f) [TopologicalSpace.SeparableSpace (Set.range f {0})] (hf : MeasureTheory.snorm f p μ < ) :
Filter.Tendsto (fun (n : ) => MeasureTheory.snorm ((MeasureTheory.SimpleFunc.approxOn f fmeas (Set.range f {0}) 0 n) - f) p μ) Filter.atTop (nhds 0)
theorem MeasureTheory.SimpleFunc.tendsto_approxOn_range_Lp {β : Type u_2} {E : Type u_4} [MeasurableSpace β] [MeasurableSpace E] [NormedAddCommGroup E] {p : ENNReal} [BorelSpace E] {f : βE} [hp : Fact (1 p)] (hp_ne_top : p ) {μ : MeasureTheory.Measure β} (fmeas : Measurable f) [TopologicalSpace.SeparableSpace (Set.range f {0})] (hf : MeasureTheory.Memℒp f p μ) :
theorem MeasureTheory.Memℒp.exists_simpleFunc_snorm_sub_lt {β : Type u_2} [MeasurableSpace β] {p : ENNReal} {E : Type u_7} [NormedAddCommGroup E] {f : βE} {μ : MeasureTheory.Measure β} (hf : MeasureTheory.Memℒp f p μ) (hp_ne_top : p ) {ε : ENNReal} (hε : ε 0) :
∃ (g : MeasureTheory.SimpleFunc β E), MeasureTheory.snorm (f - g) p μ < ε MeasureTheory.Memℒp (g) p μ

Any function in ℒp can be approximated by a simple function if p < ∞.

L1 approximation by simple functions #

theorem MeasureTheory.SimpleFunc.tendsto_approxOn_L1_nnnorm {β : Type u_2} {E : Type u_4} [MeasurableSpace β] [MeasurableSpace E] [NormedAddCommGroup E] [OpensMeasurableSpace E] {f : βE} (hf : Measurable f) {s : Set E} {y₀ : E} (h₀ : y₀ s) [TopologicalSpace.SeparableSpace s] {μ : MeasureTheory.Measure β} (hμ : ∀ᵐ (x : β) ∂μ, f x closure s) (hi : MeasureTheory.HasFiniteIntegral (fun (x : β) => f x - y₀) μ) :
Filter.Tendsto (fun (n : ) => ∫⁻ (x : β), (MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n) x - f x‖₊μ) Filter.atTop (nhds 0)
theorem MeasureTheory.SimpleFunc.integrable_approxOn {β : Type u_2} {E : Type u_4} [MeasurableSpace β] [MeasurableSpace E] [NormedAddCommGroup E] [BorelSpace E] {f : βE} {μ : MeasureTheory.Measure β} (fmeas : Measurable f) (hf : MeasureTheory.Integrable f μ) {s : Set E} {y₀ : E} (h₀ : y₀ s) [TopologicalSpace.SeparableSpace s] (hi₀ : MeasureTheory.Integrable (fun (x : β) => y₀) μ) (n : ) :
theorem MeasureTheory.SimpleFunc.tendsto_approxOn_range_L1_nnnorm {β : Type u_2} {E : Type u_4} [MeasurableSpace β] [MeasurableSpace E] [NormedAddCommGroup E] [OpensMeasurableSpace E] {f : βE} {μ : MeasureTheory.Measure β} [TopologicalSpace.SeparableSpace (Set.range f {0})] (fmeas : Measurable f) (hf : MeasureTheory.Integrable f μ) :
Filter.Tendsto (fun (n : ) => ∫⁻ (x : β), (MeasureTheory.SimpleFunc.approxOn f fmeas (Set.range f {0}) 0 n) x - f x‖₊μ) Filter.atTop (nhds 0)

Properties of simple functions in Lp spaces #

A simple function f : α →ₛ E into a normed group E verifies, for a measure μ:

theorem MeasureTheory.SimpleFunc.exists_forall_norm_le {α : Type u_1} {F : Type u_5} [MeasurableSpace α] [NormedAddCommGroup F] (f : MeasureTheory.SimpleFunc α F) :
∃ (C : ), ∀ (x : α), f x C
theorem MeasureTheory.SimpleFunc.snorm'_eq {α : Type u_1} {F : Type u_5} [MeasurableSpace α] [NormedAddCommGroup F] {p : } (f : MeasureTheory.SimpleFunc α F) (μ : MeasureTheory.Measure α) :
MeasureTheory.snorm' (f) p μ = (Finset.sum (MeasureTheory.SimpleFunc.range f) fun (y : F) => y‖₊ ^ p * μ (f ⁻¹' {y})) ^ (1 / p)
theorem MeasureTheory.SimpleFunc.measure_preimage_lt_top_of_memℒp {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} (hp_pos : p 0) (hp_ne_top : p ) (f : MeasureTheory.SimpleFunc α E) (hf : MeasureTheory.Memℒp (f) p μ) (y : E) (hy_ne : y 0) :
μ (f ⁻¹' {y}) <
theorem MeasureTheory.SimpleFunc.memℒp_of_finite_measure_preimage {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} (p : ENNReal) {f : MeasureTheory.SimpleFunc α E} (hf : ∀ (y : E), y 0μ (f ⁻¹' {y}) < ) :
theorem MeasureTheory.SimpleFunc.memℒp_iff {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} {f : MeasureTheory.SimpleFunc α E} (hp_pos : p 0) (hp_ne_top : p ) :
MeasureTheory.Memℒp (f) p μ ∀ (y : E), y 0μ (f ⁻¹' {y}) <
theorem MeasureTheory.SimpleFunc.integrable_iff {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {f : MeasureTheory.SimpleFunc α E} :
MeasureTheory.Integrable (f) μ ∀ (y : E), y 0μ (f ⁻¹' {y}) <
theorem MeasureTheory.SimpleFunc.measure_support_lt_top {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [Zero β] (f : MeasureTheory.SimpleFunc α β) (hf : ∀ (y : β), y 0μ (f ⁻¹' {y}) < ) :
μ (Function.support f) <
theorem MeasureTheory.SimpleFunc.measure_support_lt_top_of_memℒp {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} (f : MeasureTheory.SimpleFunc α E) (hf : MeasureTheory.Memℒp (f) p μ) (hp_ne_zero : p 0) (hp_ne_top : p ) :
μ (Function.support f) <
theorem MeasureTheory.SimpleFunc.measure_lt_top_of_memℒp_indicator {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} (hp_pos : p 0) (hp_ne_top : p ) {c : E} (hc : c 0) {s : Set α} (hs : MeasurableSet s) (hcs : MeasureTheory.Memℒp ((MeasureTheory.SimpleFunc.piecewise s hs (MeasureTheory.SimpleFunc.const α c) (MeasureTheory.SimpleFunc.const α 0))) p μ) :
μ s <

Construction of the space of Lp simple functions, and its dense embedding into Lp.

Lp.simpleFunc is a subspace of Lp consisting of equivalence classes of an integrable simple function.

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

    Simple functions in Lp space form a NormedSpace.

    theorem MeasureTheory.Lp.simpleFunc.eq' {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} {f : (MeasureTheory.Lp.simpleFunc E p μ)} {g : (MeasureTheory.Lp.simpleFunc E p μ)} :
    f = gf = g

    Implementation note: If Lp.simpleFunc E p μ were defined as a 𝕜-submodule of Lp E p μ, then the next few lemmas, putting a normed 𝕜-group structure on Lp.simpleFunc E p μ, would be unnecessary. But instead, Lp.simpleFunc E p μ is defined as an AddSubgroup of Lp E p μ, which does not permit this (but has the advantage of working when E itself is a normed group, i.e. has no scalar action).

    def MeasureTheory.Lp.simpleFunc.smul {α : Type u_1} {E : Type u_4} {𝕜 : Type u_6} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedRing 𝕜] [Module 𝕜 E] [BoundedSMul 𝕜 E] :

    If E is a normed space, Lp.simpleFunc E p μ is a SMul. Not declared as an instance as it is (as of writing) used only in the construction of the Bochner integral.

    Equations
    Instances For
      @[simp]
      theorem MeasureTheory.Lp.simpleFunc.coe_smul {α : Type u_1} {E : Type u_4} {𝕜 : Type u_6} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedRing 𝕜] [Module 𝕜 E] [BoundedSMul 𝕜 E] (c : 𝕜) (f : (MeasureTheory.Lp.simpleFunc E p μ)) :
      (c f) = c f
      def MeasureTheory.Lp.simpleFunc.module {α : Type u_1} {E : Type u_4} {𝕜 : Type u_6} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedRing 𝕜] [Module 𝕜 E] [BoundedSMul 𝕜 E] :

      If E is a normed space, Lp.simpleFunc E p μ is a module. Not declared as an instance as it is (as of writing) used only in the construction of the Bochner integral.

      Equations
      • MeasureTheory.Lp.simpleFunc.module = Module.mk
      Instances For
        theorem MeasureTheory.Lp.simpleFunc.boundedSMul {α : Type u_1} {E : Type u_4} {𝕜 : Type u_6} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedRing 𝕜] [Module 𝕜 E] [BoundedSMul 𝕜 E] [Fact (1 p)] :

        If E is a normed space, Lp.simpleFunc E p μ is a normed space. Not declared as an instance as it is (as of writing) used only in the construction of the Bochner integral.

        If E is a normed space, Lp.simpleFunc E p μ is a normed space. Not declared as an instance as it is (as of writing) used only in the construction of the Bochner integral.

        Equations
        Instances For
          @[reducible]

          Construct the equivalence class [f] of a simple function f satisfying Memℒp.

          Equations
          Instances For
            def MeasureTheory.Lp.simpleFunc.indicatorConst {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] (p : ENNReal) {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) (hμs : μ s ) (c : E) :

            The characteristic function of a finite-measure measurable set s, as an Lp simple function.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem MeasureTheory.Lp.simpleFunc.coe_indicatorConst {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) (hμs : μ s ) (c : E) :
              theorem MeasureTheory.Lp.simpleFunc.induction {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} (hp_pos : p 0) (hp_ne_top : p ) {P : (MeasureTheory.Lp.simpleFunc E p μ)Prop} (h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ), P (MeasureTheory.Lp.simpleFunc.indicatorConst p hs c)) (h_add : ∀ ⦃f g : MeasureTheory.SimpleFunc α E⦄ (hf : MeasureTheory.Memℒp (f) p μ) (hg : MeasureTheory.Memℒp (g) p μ), Disjoint (Function.support f) (Function.support g)P (MeasureTheory.Lp.simpleFunc.toLp f hf)P (MeasureTheory.Lp.simpleFunc.toLp g hg)P (MeasureTheory.Lp.simpleFunc.toLp f hf + MeasureTheory.Lp.simpleFunc.toLp g hg)) (f : (MeasureTheory.Lp.simpleFunc E p μ)) :
              P f

              To prove something for an arbitrary Lp simple function, with 0 < p < ∞, it suffices to show that the property holds for (multiples of) characteristic functions of finite-measure measurable sets and is closed under addition (of functions with disjoint support).

              theorem MeasureTheory.Lp.simpleFunc.denseEmbedding {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} [Fact (1 p)] (hp_ne_top : p ) :
              DenseEmbedding Subtype.val
              theorem MeasureTheory.Lp.simpleFunc.denseInducing {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} [Fact (1 p)] (hp_ne_top : p ) :
              DenseInducing Subtype.val
              theorem MeasureTheory.Lp.simpleFunc.denseRange {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} [Fact (1 p)] (hp_ne_top : p ) :
              DenseRange Subtype.val
              def MeasureTheory.Lp.simpleFunc.coeToLp (α : Type u_1) (E : Type u_4) (𝕜 : Type u_6) [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} [Fact (1 p)] [NormedRing 𝕜] [Module 𝕜 E] [BoundedSMul 𝕜 E] :

              The embedding of Lp simple functions into Lp functions, as a continuous linear map.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                instance MeasureTheory.Lp.simpleFunc.instCovariantClassLE {α : Type u_1} [MeasurableSpace α] {p : ENNReal} {μ : MeasureTheory.Measure α} {G : Type u_7} [NormedLatticeAddCommGroup G] :
                CovariantClass ((MeasureTheory.Lp.simpleFunc G p μ)) ((MeasureTheory.Lp.simpleFunc G p μ)) (fun (x x_1 : (MeasureTheory.Lp.simpleFunc G p μ)) => x + x_1) fun (x x_1 : (MeasureTheory.Lp.simpleFunc G p μ)) => x x_1
                Equations
                • =

                Coercion from nonnegative simple functions of Lp to nonnegative functions of Lp.

                Equations
                Instances For
                  theorem MeasureTheory.Lp.induction {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} [_i : Fact (1 p)] (hp_ne_top : p ) (P : (MeasureTheory.Lp E p μ)Prop) (h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ), P (MeasureTheory.Lp.simpleFunc.indicatorConst p hs c)) (h_add : ∀ ⦃f g : αE⦄ (hf : MeasureTheory.Memℒp f p μ) (hg : MeasureTheory.Memℒp g p μ), Disjoint (Function.support f) (Function.support g)P (MeasureTheory.Memℒp.toLp f hf)P (MeasureTheory.Memℒp.toLp g hg)P (MeasureTheory.Memℒp.toLp f hf + MeasureTheory.Memℒp.toLp g hg)) (h_closed : IsClosed {f : (MeasureTheory.Lp E p μ) | P f}) (f : (MeasureTheory.Lp E p μ)) :
                  P f

                  To prove something for an arbitrary Lp function in a second countable Borel normed group, it suffices to show that

                  • the property holds for (multiples of) characteristic functions;
                  • is closed under addition;
                  • the set of functions in Lp for which the property holds is closed.
                  theorem MeasureTheory.Memℒp.induction {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} [_i : Fact (1 p)] (hp_ne_top : p ) (P : (αE)Prop) (h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet sμ s < P (Set.indicator s fun (x : α) => c)) (h_add : ∀ ⦃f g : αE⦄, Disjoint (Function.support f) (Function.support g)MeasureTheory.Memℒp f p μMeasureTheory.Memℒp g p μP fP gP (f + g)) (h_closed : IsClosed {f : (MeasureTheory.Lp E p μ) | P f}) (h_ae : ∀ ⦃f g : αE⦄, f =ᶠ[MeasureTheory.Measure.ae μ] gMeasureTheory.Memℒp f p μP fP g) ⦃f : αE :
                  MeasureTheory.Memℒp f p μP f

                  To prove something for an arbitrary Memℒp function in a second countable Borel normed group, it suffices to show that

                  • the property holds for (multiples of) characteristic functions;
                  • is closed under addition;
                  • the set of functions in the Lᵖ space for which the property holds is closed.
                  • the property is closed under the almost-everywhere equal relation.

                  It is possible to make the hypotheses in the induction steps a bit stronger, and such conditions can be added once we need them (for example in h_add it is only necessary to consider the sum of a simple function with a multiple of a characteristic function and that the intersection of their images is a subset of {0}).

                  theorem MeasureTheory.Memℒp.induction_dense {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} (hp_ne_top : p ) (P : (αE)Prop) (h0P : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet sμ s < ∀ {ε : ENNReal}, ε 0∃ (g : αE), MeasureTheory.snorm (g - Set.indicator s fun (x : α) => c) p μ ε P g) (h1P : ∀ (f g : αE), P fP gP (f + g)) (h2P : ∀ (f : αE), P fMeasureTheory.AEStronglyMeasurable f μ) {f : αE} (hf : MeasureTheory.Memℒp f p μ) {ε : ENNReal} (hε : ε 0) :
                  ∃ (g : αE), MeasureTheory.snorm (f - g) p μ ε P g

                  If a set of ae strongly measurable functions is stable under addition and approximates characteristic functions in ℒp, then it is dense in ℒp.

                  Lp.simpleFunc is a subspace of Lp consisting of equivalence classes of an integrable simple function.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    theorem MeasureTheory.Integrable.induction {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} (P : (αE)Prop) (h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet sμ s < P (Set.indicator s fun (x : α) => c)) (h_add : ∀ ⦃f g : αE⦄, Disjoint (Function.support f) (Function.support g)MeasureTheory.Integrable f μMeasureTheory.Integrable g μP fP gP (f + g)) (h_closed : IsClosed {f : (MeasureTheory.Lp E 1 μ) | P f}) (h_ae : ∀ ⦃f g : αE⦄, f =ᶠ[MeasureTheory.Measure.ae μ] gMeasureTheory.Integrable f μP fP g) ⦃f : αE :

                    To prove something for an arbitrary integrable function in a normed group, it suffices to show that

                    • the property holds for (multiples of) characteristic functions;
                    • is closed under addition;
                    • the set of functions in the space for which the property holds is closed.
                    • the property is closed under the almost-everywhere equal relation.

                    It is possible to make the hypotheses in the induction steps a bit stronger, and such conditions can be added once we need them (for example in h_add it is only necessary to consider the sum of a simple function with a multiple of a characteristic function and that the intersection of their images is a subset of {0}).