Documentation

Mathlib.MeasureTheory.Integral.Bochner.L1

Bochner integral #

The Bochner integral extends the definition of the Lebesgue integral to functions that map from a measure space into a Banach space (complete normed vector space). It is constructed here for L1 functions by extending the integral on simple functions. See the file Mathlib/MeasureTheory/Integral/Bochner/Basic.lean for the integral of functions and corresponding API.

Main definitions #

The Bochner integral is defined through the extension process described in the file Mathlib/MeasureTheory/Integral/SetToL1.lean, which follows these steps:

  1. Define the integral of the indicator of a set. This is weightedSMul μ s x = μ.real s * x. weightedSMul μ is shown to be linear in the value x and DominatedFinMeasAdditive (defined in the file Mathlib/MeasureTheory/Integral/SetToL1.lean) with respect to the set s.

  2. Define the integral on simple functions of the type SimpleFunc α E (notation : α →ₛ E) where E is a real normed space. (See SimpleFunc.integral for details.)

  3. Transfer this definition to define the integral on L1.simpleFunc α E (notation : α →₁ₛ[μ] E), see L1.simpleFunc.integral. Show that this integral is a continuous linear map from α →₁ₛ[μ] E to E.

  4. Define the Bochner integral on L1 functions by extending the integral on integrable simple functions α →₁ₛ[μ] E using ContinuousLinearMap.extend and the fact that the embedding of α →₁ₛ[μ] E into α →₁[μ] E is dense.

Notations #

We also define notations for integral on a set, which are described in the file Mathlib/MeasureTheory/Integral/SetIntegral.lean.

Note : is typed using \_s. Sometimes it shows as a box if the font is missing.

Tags #

Bochner integral, simple function, function space, Lebesgue dominated convergence theorem

def MeasureTheory.weightedSMul {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace F] {x✝ : MeasurableSpace α} (μ : Measure α) (s : Set α) :

Given a set s, return the continuous linear map fun x => μ.real s • x. The extension of that set function through setToL1 gives the Bochner integral of L1 functions.

Equations
Instances For
    theorem MeasureTheory.weightedSMul_apply {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} (μ : Measure α) (s : Set α) (x : F) :
    (weightedSMul μ s) x = μ.real s x
    @[simp]
    theorem MeasureTheory.weightedSMul_add_measure {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} (μ ν : Measure α) {s : Set α} (hμs : μ s ) (hνs : ν s ) :
    theorem MeasureTheory.weightedSMul_smul_measure {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} (μ : Measure α) (c : ENNReal) {s : Set α} :
    theorem MeasureTheory.weightedSMul_congr {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : Measure α} (s t : Set α) (hst : μ s = μ t) :
    theorem MeasureTheory.weightedSMul_null {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : Measure α} {s : Set α} (h_zero : μ s = 0) :
    theorem MeasureTheory.weightedSMul_union' {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : Measure α} (s t : Set α) (ht : MeasurableSet t) (hs_finite : μ s ) (ht_finite : μ t ) (hdisj : Disjoint s t) :
    theorem MeasureTheory.weightedSMul_union {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : Measure α} (s t : Set α) (_hs : MeasurableSet s) (ht : MeasurableSet t) (hs_finite : μ s ) (ht_finite : μ t ) (hdisj : Disjoint s t) :
    theorem MeasureTheory.weightedSMul_smul {α : Type u_1} {F : Type u_3} {𝕜 : Type u_4} [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : Measure α} [SMul 𝕜 F] [SMulCommClass 𝕜 F] (c : 𝕜) (s : Set α) (x : F) :
    (weightedSMul μ s) (c x) = c (weightedSMul μ s) x
    theorem MeasureTheory.norm_weightedSMul_le {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : Measure α} (s : Set α) :
    theorem MeasureTheory.weightedSMul_nonneg {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : Measure α} [PartialOrder F] [OrderedSMul F] (s : Set α) (x : F) (hx : 0 x) :
    0 (weightedSMul μ s) x
    def MeasureTheory.SimpleFunc.posPart {α : Type u_1} {E : Type u_2} [LinearOrder E] [Zero E] [MeasurableSpace α] (f : SimpleFunc α E) :

    Positive part of a simple function.

    Equations
    Instances For
      def MeasureTheory.SimpleFunc.negPart {α : Type u_1} {E : Type u_2} [LinearOrder E] [Zero E] [MeasurableSpace α] [Neg E] (f : SimpleFunc α E) :

      Negative part of a simple function.

      Equations
      Instances For

        The Bochner integral of simple functions #

        Define the Bochner integral of simple functions of the type α →ₛ β where β is a normed group, and prove basic property of this integral.

        def MeasureTheory.SimpleFunc.integral {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace F] {x✝ : MeasurableSpace α} (μ : Measure α) (f : SimpleFunc α F) :
        F

        Bochner integral of simple functions whose codomain is a real NormedSpace. This is equal to ∑ x ∈ f.range, μ.real (f ⁻¹' {x}) • x (see integral_eq).

        Equations
        Instances For
          theorem MeasureTheory.SimpleFunc.integral_eq {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} (μ : Measure α) (f : SimpleFunc α F) :
          integral μ f = xf.range, μ.real (f ⁻¹' {x}) x
          theorem MeasureTheory.SimpleFunc.integral_eq_sum_filter {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace F] [DecidablePred fun (x : F) => x 0] {m : MeasurableSpace α} (f : SimpleFunc α F) (μ : Measure α) :
          integral μ f = xf.range with x 0, μ.real (f ⁻¹' {x}) x
          theorem MeasureTheory.SimpleFunc.integral_eq_sum_of_subset {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : Measure α} [DecidablePred fun (x : F) => x 0] {f : SimpleFunc α F} {s : Finset F} (hs : {xf.range | x 0} s) :
          integral μ f = xs, μ.real (f ⁻¹' {x}) x

          The Bochner integral is equal to a sum over any set that includes f.range (except 0).

          @[simp]
          theorem MeasureTheory.SimpleFunc.integral_const {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} (μ : Measure α) (y : F) :
          integral μ (const α y) = μ.real Set.univ y
          @[simp]
          theorem MeasureTheory.SimpleFunc.integral_piecewise_zero {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} (f : SimpleFunc α F) (μ : Measure α) {s : Set α} (hs : MeasurableSet s) :
          integral μ (piecewise s hs f 0) = integral (μ.restrict s) f
          theorem MeasureTheory.SimpleFunc.map_integral {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : Measure α} (f : SimpleFunc α E) (g : EF) (hf : Integrable (⇑f) μ) (hg : g 0 = 0) :
          integral μ (map g f) = xf.range, μ.real (f ⁻¹' {x}) g x

          Calculate the integral of g ∘ f : α →ₛ F, where f is an integrable function from α to E and g is a function from E to F. We require g 0 = 0 so that g ∘ f is integrable.

          theorem MeasureTheory.SimpleFunc.integral_eq_lintegral' {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {m : MeasurableSpace α} {μ : Measure α} {f : SimpleFunc α E} {g : EENNReal} (hf : Integrable (⇑f) μ) (hg0 : g 0 = 0) (ht : ∀ (b : E), g b ) :
          integral μ (map (ENNReal.toReal g) f) = (∫⁻ (a : α), g (f a) μ).toReal

          SimpleFunc.integral and SimpleFunc.lintegral agree when the integrand has type α →ₛ ℝ≥0∞. But since ℝ≥0∞ is not a NormedSpace, we need some form of coercion. See integral_eq_lintegral for a simpler version.

          theorem MeasureTheory.SimpleFunc.integral_congr {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {m : MeasurableSpace α} {μ : Measure α} [NormedSpace E] {f g : SimpleFunc α E} (hf : Integrable (⇑f) μ) (h : f =ᶠ[ae μ] g) :
          integral μ f = integral μ g
          theorem MeasureTheory.SimpleFunc.integral_eq_lintegral {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : SimpleFunc α } (hf : Integrable (⇑f) μ) (h_pos : 0 ≤ᶠ[ae μ] f) :
          integral μ f = (∫⁻ (a : α), ENNReal.ofReal (f a) μ).toReal

          SimpleFunc.bintegral and SimpleFunc.integral agree when the integrand has type α →ₛ ℝ≥0∞. But since ℝ≥0∞ is not a NormedSpace, we need some form of coercion.

          theorem MeasureTheory.SimpleFunc.integral_add {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {m : MeasurableSpace α} {μ : Measure α} [NormedSpace E] {f g : SimpleFunc α E} (hf : Integrable (⇑f) μ) (hg : Integrable (⇑g) μ) :
          integral μ (f + g) = integral μ f + integral μ g
          theorem MeasureTheory.SimpleFunc.integral_neg {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {m : MeasurableSpace α} {μ : Measure α} [NormedSpace E] {f : SimpleFunc α E} (hf : Integrable (⇑f) μ) :
          integral μ (-f) = -integral μ f
          theorem MeasureTheory.SimpleFunc.integral_sub {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {m : MeasurableSpace α} {μ : Measure α} [NormedSpace E] {f g : SimpleFunc α E} (hf : Integrable (⇑f) μ) (hg : Integrable (⇑g) μ) :
          integral μ (f - g) = integral μ f - integral μ g
          theorem MeasureTheory.SimpleFunc.integral_smul {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [NormedAddCommGroup E] {m : MeasurableSpace α} {μ : Measure α} [NormedSpace E] [DistribSMul 𝕜 E] [SMulCommClass 𝕜 E] (c : 𝕜) {f : SimpleFunc α E} (hf : Integrable (⇑f) μ) :
          integral μ (c f) = c integral μ f
          theorem MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_integral_norm {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : Measure α} [NormedSpace E] (T : Set αE →L[] F) {C : } (hT_norm : ∀ (s : Set α), MeasurableSet sμ s < T s C * μ.real s) {f : SimpleFunc α E} (hf : Integrable (⇑f) μ) :
          theorem MeasureTheory.SimpleFunc.integral_add_measure {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {m : MeasurableSpace α} {μ : Measure α} [NormedSpace E] {ν : Measure α} (f : SimpleFunc α E) (hf : Integrable (⇑f) (μ + ν)) :
          integral (μ + ν) f = integral μ f + integral ν f
          theorem MeasureTheory.SimpleFunc.integral_mono {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : Measure α} [PartialOrder F] [IsOrderedAddMonoid F] [OrderedSMul F] {f g : SimpleFunc α F} (h : f ≤ᶠ[ae μ] g) (hf : Integrable (⇑f) μ) (hg : Integrable (⇑g) μ) :
          theorem MeasureTheory.SimpleFunc.integral_mono_measure {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace F] {m : MeasurableSpace α} {μ : Measure α} [PartialOrder F] [IsOrderedAddMonoid F] [OrderedSMul F] {ν : Measure α} {f : SimpleFunc α F} (hf : 0 ≤ᶠ[ae ν] f) (hμν : μ ν) (hfν : Integrable (⇑f) ν) :
          def MeasureTheory.L1.SimpleFunc.posPart {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} (f : (Lp.simpleFunc 1 μ)) :
          (Lp.simpleFunc 1 μ)

          Positive part of a simple function in L1 space.

          Equations
          Instances For
            def MeasureTheory.L1.SimpleFunc.negPart {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} (f : (Lp.simpleFunc 1 μ)) :
            (Lp.simpleFunc 1 μ)

            Negative part of a simple function in L1 space.

            Equations
            Instances For
              theorem MeasureTheory.L1.SimpleFunc.coe_posPart {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} (f : (Lp.simpleFunc 1 μ)) :
              (posPart f) = Lp.posPart f
              theorem MeasureTheory.L1.SimpleFunc.coe_negPart {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} (f : (Lp.simpleFunc 1 μ)) :
              (negPart f) = Lp.negPart f

              The Bochner integral of L1 #

              Define the Bochner integral on α →₁ₛ[μ] E by extension from the simple functions α →₁ₛ[μ] E, and prove basic properties of this integral.

              def MeasureTheory.L1.SimpleFunc.integral {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {m : MeasurableSpace α} {μ : Measure α} [NormedSpace E] (f : (Lp.simpleFunc E 1 μ)) :
              E

              The Bochner integral over simple functions in L1 space.

              Equations
              Instances For
                theorem MeasureTheory.L1.SimpleFunc.integral_add {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {m : MeasurableSpace α} {μ : Measure α} [NormedSpace E] (f g : (Lp.simpleFunc E 1 μ)) :
                theorem MeasureTheory.L1.SimpleFunc.integral_smul {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [NormedAddCommGroup E] {m : MeasurableSpace α} {μ : Measure α} [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [NormedSpace E] [SMulCommClass 𝕜 E] (c : 𝕜) (f : (Lp.simpleFunc E 1 μ)) :
                def MeasureTheory.L1.SimpleFunc.integralCLM' (α : Type u_1) (E : Type u_2) (𝕜 : Type u_4) [NormedAddCommGroup E] {m : MeasurableSpace α} (μ : Measure α) [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [NormedSpace E] [SMulCommClass 𝕜 E] :
                (Lp.simpleFunc E 1 μ) →L[𝕜] E

                The Bochner integral over simple functions in L1 space as a continuous linear map.

                Equations
                Instances For

                  The Bochner integral over simple functions in L1 space as a continuous linear map over ℝ.

                  Equations
                  Instances For
                    def MeasureTheory.L1.integralCLM' {α : Type u_1} {E : Type u_2} (𝕜 : Type u_4) [NormedAddCommGroup E] {m : MeasurableSpace α} {μ : Measure α} [NormedSpace E] [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [SMulCommClass 𝕜 E] [CompleteSpace E] :
                    (Lp E 1 μ) →L[𝕜] E

                    The Bochner integral in L1 space as a continuous linear map.

                    Equations
                    Instances For
                      def MeasureTheory.L1.integralCLM {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {m : MeasurableSpace α} {μ : Measure α} [NormedSpace E] [CompleteSpace E] :
                      (Lp E 1 μ) →L[] E

                      The Bochner integral in L1 space as a continuous linear map over ℝ.

                      Equations
                      Instances For
                        @[irreducible]
                        def MeasureTheory.L1.integral {α : Type u_5} {E : Type u_6} [NormedAddCommGroup E] {m : MeasurableSpace α} {μ : Measure α} [NormedSpace E] [CompleteSpace E] :
                        (Lp E 1 μ)E

                        The Bochner integral in L1 space

                        Equations
                        Instances For
                          theorem MeasureTheory.L1.integral_eq {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {m : MeasurableSpace α} {μ : Measure α} [NormedSpace E] [CompleteSpace E] (f : (Lp E 1 μ)) :
                          theorem MeasureTheory.L1.integral_eq_setToL1 {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {m : MeasurableSpace α} {μ : Measure α} [NormedSpace E] [CompleteSpace E] (f : (Lp E 1 μ)) :
                          integral f = (setToL1 ) f
                          @[simp]
                          theorem MeasureTheory.L1.integral_add {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {m : MeasurableSpace α} {μ : Measure α} [NormedSpace E] [CompleteSpace E] (f g : (Lp E 1 μ)) :
                          theorem MeasureTheory.L1.integral_neg {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {m : MeasurableSpace α} {μ : Measure α} [NormedSpace E] [CompleteSpace E] (f : (Lp E 1 μ)) :
                          theorem MeasureTheory.L1.integral_sub {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {m : MeasurableSpace α} {μ : Measure α} [NormedSpace E] [CompleteSpace E] (f g : (Lp E 1 μ)) :
                          theorem MeasureTheory.L1.integral_smul {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [NormedAddCommGroup E] {m : MeasurableSpace α} {μ : Measure α} [NormedSpace E] [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [SMulCommClass 𝕜 E] [CompleteSpace E] (c : 𝕜) (f : (Lp E 1 μ)) :
                          theorem MeasureTheory.L1.norm_integral_le {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {m : MeasurableSpace α} {μ : Measure α} [NormedSpace E] [CompleteSpace E] (f : (Lp E 1 μ)) :
                          theorem MeasureTheory.L1.continuous_integral {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {m : MeasurableSpace α} {μ : Measure α} [NormedSpace E] [CompleteSpace E] :
                          Continuous fun (f : (Lp E 1 μ)) => integral f