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

• α →ₛ 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.

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.

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.

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

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 α} [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) μ) : ‖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.

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.

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.

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 α} [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 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 α) [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.

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 ℝ.

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] [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.

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 ℝ.

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

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] [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 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‖