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 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, 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) 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

• α →ₛ E : simple functions (defined in Mathlib/MeasureTheory/Function/SimpleFunc.lean)
• α →₁[μ] E : functions in L1 space, i.e., equivalence classes of integrable functions (defined in Mathlib/MeasureTheory/Function/LpSpace/Basic.lean)
• α →₁ₛ[μ] E : simple functions in L1 space, i.e., equivalence classes of integrable simple functions (defined in Mathlib/MeasureTheory/Function/SimpleFuncDense)

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 α) : F →L[ℝ] F

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

• MeasureTheory.weightedSMul μ s = μ.real s • ContinuousLinearMap.id ℝ F

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_zero_measure {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} : weightedSMul 0 = 0

@[simp]

theorem MeasureTheory.weightedSMul_empty {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} (μ : Measure α) : weightedSMul μ ∅ = 0

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 ≠ ⊤) : weightedSMul (μ + ν) s = weightedSMul μ s + weightedSMul ν s

theorem MeasureTheory.weightedSMul_smul_measure {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} (μ : Measure α) (c : ENNReal) {s : Set α} : weightedSMul (c • μ) s = c.toReal • weightedSMul μ s

theorem MeasureTheory.weightedSMul_congr {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} (s t : Set α) (hst : μ s = μ t) : weightedSMul μ s = weightedSMul μ 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) : weightedSMul μ 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) : weightedSMul μ (s ∪ t) = weightedSMul μ s + weightedSMul μ 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) : weightedSMul μ (s ∪ t) = weightedSMul μ s + weightedSMul μ 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 α) : ‖weightedSMul μ s‖ ≤ μ.real s

theorem MeasureTheory.dominatedFinMeasAdditive_weightedSMul {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {x✝ : MeasurableSpace α} (μ : Measure α) : DominatedFinMeasAdditive μ (weightedSMul μ) 1

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) : SimpleFunc α E

Positive part of a simple function.

Equations

• f.posPart = MeasureTheory.SimpleFunc.map (fun (b : E) => max b 0) f

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

Negative part of a simple function.

Equations

• f.negPart = (-f).posPart

theorem MeasureTheory.SimpleFunc.posPart_map_norm {α : Type u_1} [MeasurableSpace α] (f : SimpleFunc α ℝ) : map norm f.posPart = f.posPart

theorem MeasureTheory.SimpleFunc.negPart_map_norm {α : Type u_1} [MeasurableSpace α] (f : SimpleFunc α ℝ) : map norm f.negPart = f.negPart

theorem MeasureTheory.SimpleFunc.posPart_sub_negPart {α : Type u_1} [MeasurableSpace α] (f : SimpleFunc α ℝ) : f.posPart - f.negPart = f

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

• MeasureTheory.SimpleFunc.integral μ f = MeasureTheory.SimpleFunc.setToSimpleFunc (MeasureTheory.weightedSMul μ) f

theorem MeasureTheory.SimpleFunc.integral_def {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {x✝ : MeasurableSpace α} (μ : Measure α) (f : SimpleFunc α F) : integral μ f = setToSimpleFunc (weightedSMul μ) f

theorem MeasureTheory.SimpleFunc.integral_eq {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} (μ : Measure α) (f : SimpleFunc α F) : integral μ f = ∑ x ∈ f.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 = ∑ x ∈ f.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 : {x ∈ f.range | x ≠ 0} ⊆ s) : integral μ f = ∑ x ∈ s, μ.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 : E → F) (hf : Integrable (⇑f) μ) (hg : g 0 = 0) : integral μ (map g f) = ∑ x ∈ f.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 : E → ENNReal} (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 α} [NormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace ℝ 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) μ) : ‖setToSimpleFunc T f‖ ≤ C * integral μ (map norm f)

theorem MeasureTheory.SimpleFunc.norm_integral_le_integral_norm {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {m : MeasurableSpace α} {μ : Measure α} [NormedSpace ℝ E] (f : SimpleFunc α E) (hf : Integrable (⇑f) μ) : ‖integral μ f‖ ≤ integral μ (map norm 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_nonneg {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} [PartialOrder F] [IsOrderedAddMonoid F] [OrderedSMul ℝ F] {f : SimpleFunc α F} (hf : 0 ≤ᶠ[ae μ] ⇑f) : 0 ≤ 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) μ) : integral μ f ≤ integral μ 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) ν) : integral μ f ≤ integral ν f

theorem MeasureTheory.L1.SimpleFunc.norm_eq_integral {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {m : MeasurableSpace α} {μ : Measure α} (f : ↥(Lp.simpleFunc E 1 μ)) : ‖f‖ = MeasureTheory.SimpleFunc.integral μ (SimpleFunc.map norm (Lp.simpleFunc.toSimpleFunc 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

• MeasureTheory.L1.SimpleFunc.posPart f = ⟨MeasureTheory.Lp.posPart ↑f, ⋯⟩

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

• MeasureTheory.L1.SimpleFunc.negPart f = MeasureTheory.L1.SimpleFunc.posPart (-f)

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

• MeasureTheory.L1.SimpleFunc.integral f = MeasureTheory.SimpleFunc.integral μ (MeasureTheory.Lp.simpleFunc.toSimpleFunc f)

theorem MeasureTheory.L1.SimpleFunc.integral_eq_integral {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {m : MeasurableSpace α} {μ : Measure α} [NormedSpace ℝ E] (f : ↥(Lp.simpleFunc E 1 μ)) : integral f = MeasureTheory.SimpleFunc.integral μ (Lp.simpleFunc.toSimpleFunc f)

theorem MeasureTheory.L1.SimpleFunc.integral_eq_lintegral {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : ↥(Lp.simpleFunc ℝ 1 μ)} (h_pos : 0 ≤ᶠ[ae μ] ⇑(Lp.simpleFunc.toSimpleFunc f)) : integral f = (∫⁻ (a : α), ENNReal.ofReal ((Lp.simpleFunc.toSimpleFunc f) a) ∂μ).toReal

theorem MeasureTheory.L1.SimpleFunc.integral_eq_setToL1S {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {m : MeasurableSpace α} {μ : Measure α} [NormedSpace ℝ E] (f : ↥(Lp.simpleFunc E 1 μ)) : integral f = setToL1S (weightedSMul μ) f

theorem MeasureTheory.L1.SimpleFunc.integral_congr {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {m : MeasurableSpace α} {μ : Measure α} [NormedSpace ℝ E] {f g : ↥(Lp.simpleFunc E 1 μ)} (h : ⇑(Lp.simpleFunc.toSimpleFunc f) =ᶠ[ae μ] ⇑(Lp.simpleFunc.toSimpleFunc g)) : integral f = integral g

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 μ)) : integral (f + g) = integral f + integral g

theorem MeasureTheory.L1.SimpleFunc.integral_smul {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [NormedAddCommGroup E] {m : MeasurableSpace α} {μ : Measure α} [NormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace ℝ E] [SMulCommClass ℝ 𝕜 E] (c : 𝕜) (f : ↥(Lp.simpleFunc E 1 μ)) : integral (c • f) = c • integral f

theorem MeasureTheory.L1.SimpleFunc.norm_integral_le_norm {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {m : MeasurableSpace α} {μ : Measure α} [NormedSpace ℝ E] (f : ↥(Lp.simpleFunc E 1 μ)) : ‖integral f‖ ≤ ‖f‖

def MeasureTheory.L1.SimpleFunc.integralCLM' (α : Type u_1) (E : Type u_2) (𝕜 : Type u_4) [NormedAddCommGroup E] {m : MeasurableSpace α} (μ : Measure α) [NormedField 𝕜] [NormedSpace 𝕜 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

• MeasureTheory.L1.SimpleFunc.integralCLM' α E 𝕜 μ = { toFun := MeasureTheory.L1.SimpleFunc.integral, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous 1 ⋯

def MeasureTheory.L1.SimpleFunc.integralCLM (α : Type u_1) (E : Type u_2) [NormedAddCommGroup E] {m : MeasurableSpace α} (μ : Measure α) [NormedSpace ℝ E] : ↥(Lp.simpleFunc E 1 μ) →L[ℝ] E

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

Equations

• MeasureTheory.L1.SimpleFunc.integralCLM α E μ = MeasureTheory.L1.SimpleFunc.integralCLM' α E ℝ μ

theorem MeasureTheory.L1.SimpleFunc.norm_Integral_le_one {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {m : MeasurableSpace α} {μ : Measure α} [NormedSpace ℝ E] : ‖integralCLM α E μ‖ ≤ 1

theorem MeasureTheory.L1.SimpleFunc.posPart_toSimpleFunc {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} (f : ↥(Lp.simpleFunc ℝ 1 μ)) : ⇑(Lp.simpleFunc.toSimpleFunc (posPart f)) =ᶠ[ae μ] ⇑(Lp.simpleFunc.toSimpleFunc f).posPart

theorem MeasureTheory.L1.SimpleFunc.negPart_toSimpleFunc {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} (f : ↥(Lp.simpleFunc ℝ 1 μ)) : ⇑(Lp.simpleFunc.toSimpleFunc (negPart f)) =ᶠ[ae μ] ⇑(Lp.simpleFunc.toSimpleFunc f).negPart

theorem MeasureTheory.L1.SimpleFunc.integral_eq_norm_posPart_sub {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} (f : ↥(Lp.simpleFunc ℝ 1 μ)) : integral f = ‖posPart f‖ - ‖negPart f‖

def MeasureTheory.L1.integralCLM' {α : Type u_1} {E : Type u_2} (𝕜 : Type u_4) [NormedAddCommGroup E] {m : MeasurableSpace α} {μ : Measure α} [NormedSpace ℝ E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [SMulCommClass ℝ 𝕜 E] [CompleteSpace E] : ↥(Lp E 1 μ) →L[𝕜] E

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

Equations

• MeasureTheory.L1.integralCLM' 𝕜 = (MeasureTheory.L1.SimpleFunc.integralCLM' α E 𝕜 μ).extend (MeasureTheory.Lp.simpleFunc.coeToLp α E 𝕜) ⋯ ⋯

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

• MeasureTheory.L1.integralCLM = MeasureTheory.L1.integralCLM' ℝ

@[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

• MeasureTheory.L1.integral = ⇑MeasureTheory.L1.integralCLM

theorem MeasureTheory.L1.integral_def {α : Type u_5} {E : Type u_6} [NormedAddCommGroup E] {m : MeasurableSpace α} {μ : Measure α} [NormedSpace ℝ E] [CompleteSpace E] : integral = ⇑integralCLM

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 μ)) : integral f = integralCLM f

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

theorem MeasureTheory.L1.SimpleFunc.integral_L1_eq_integral {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {m : MeasurableSpace α} {μ : Measure α} [NormedSpace ℝ E] [CompleteSpace E] (f : ↥(Lp.simpleFunc E 1 μ)) : L1.integral ↑f = integral f

@[simp]

theorem MeasureTheory.L1.integral_zero (α : Type u_1) (E : Type u_2) [NormedAddCommGroup E] {m : MeasurableSpace α} {μ : Measure α} [NormedSpace ℝ E] [CompleteSpace E] : integral 0 = 0

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 μ)) : integral (f + g) = integral f + integral g

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 μ)) : integral (-f) = -integral f

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 μ)) : integral (f - g) = integral f - integral g

theorem MeasureTheory.L1.integral_smul {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [NormedAddCommGroup E] {m : MeasurableSpace α} {μ : Measure α} [NormedSpace ℝ E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [SMulCommClass ℝ 𝕜 E] [CompleteSpace E] (c : 𝕜) (f : ↥(Lp E 1 μ)) : integral (c • f) = c • integral f

theorem MeasureTheory.L1.norm_Integral_le_one {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {m : MeasurableSpace α} {μ : Measure α} [NormedSpace ℝ E] [CompleteSpace E] : ‖integralCLM‖ ≤ 1

theorem MeasureTheory.L1.nnnorm_Integral_le_one {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {m : MeasurableSpace α} {μ : Measure α} [NormedSpace ℝ E] [CompleteSpace E] : ‖integralCLM‖₊ ≤ 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 μ)) : ‖integral f‖ ≤ ‖f‖

theorem MeasureTheory.L1.nnnorm_integral_le {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {m : MeasurableSpace α} {μ : Measure α} [NormedSpace ℝ E] [CompleteSpace E] (f : ↥(Lp E 1 μ)) : ‖integral f‖₊ ≤ ‖f‖₊

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

theorem MeasureTheory.L1.integral_eq_norm_posPart_sub {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} (f : ↥(Lp ℝ 1 μ)) : integral f = ‖Lp.posPart f‖ - ‖Lp.negPart f‖