# mathlibdocumentation

measure_theory.bochner_integration

# 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 by extending the integral on simple functions.

## Main definitions

The Bochner integral is defined following these steps:

1. Define the integral on simple functions of the type simple_func α E (notation : α →ₛ E) where E is a real normed space.

(See simple_func.bintegral and section bintegral for details. Also see simple_func.integral for the integral on simple functions of the type simple_func α ennreal.)

2. Use α →ₛ E to cut out the simple functions from L1 functions, and define integral on these. The type of simple functions in L1 space is written as α →₁ₛ[μ] E.

3. Show that the embedding of α →₁ₛ[μ] E into L1 is a dense and uniform one.

4. Show that the integral defined on α →₁ₛ[μ] E is a continuous linear map.

5. Define the Bochner integral on L1 functions by extending the integral on integrable simple functions α →₁ₛ[μ] E using continuous_linear_map.extend. Define the Bochner integral on functions as the Bochner integral of its equivalence class in L1 space.

## Main statements

1. Basic properties of the Bochner integral on functions of type α → E, where α is a measure space and E is a real normed space.

• integral_zero : ∫ 0 ∂μ = 0
• integral_add : ∫ x, f x + g x ∂μ = ∫ x, f ∂μ + ∫ x, g x ∂μ
• integral_neg : ∫ x, - f x ∂μ = - ∫ x, f x ∂μ
• integral_sub : ∫ x, f x - g x ∂μ = ∫ x, f x ∂μ - ∫ x, g x ∂μ
• integral_smul : ∫ x, r • f x ∂μ = r • ∫ x, f x ∂μ
• integral_congr_ae : f =ᵐ[μ] g → ∫ x, f x ∂μ = ∫ x, g x ∂μ
• norm_integral_le_integral_norm : ∥∫ x, f x ∂μ∥ ≤ ∫ x, ∥f x∥ ∂μ
2. Basic properties of the Bochner integral on functions of type α → ℝ, where α is a measure space.

• integral_nonneg_of_ae : 0 ≤ᵐ[μ] f → 0 ≤ ∫ x, f x ∂μ
• integral_nonpos_of_ae : f ≤ᵐ[μ] 0 → ∫ x, f x ∂μ ≤ 0
• integral_mono_ae : f ≤ᵐ[μ] g → ∫ x, f x ∂μ ≤ ∫ x, g x ∂μ
• integral_nonneg : 0 ≤ f → 0 ≤ ∫ x, f x ∂μ
• integral_nonpos : f ≤ 0 → ∫ x, f x ∂μ ≤ 0
• integral_mono : f ≤ᵐ[μ] g → ∫ x, f x ∂μ ≤ ∫ x, g x ∂μ
3. Propositions connecting the Bochner integral with the integral on ennreal-valued functions, which is called lintegral and has the notation ∫⁻.

• integral_eq_lintegral_max_sub_lintegral_min : ∫ x, f x ∂μ = ∫⁻ x, f⁺ x ∂μ - ∫⁻ x, f⁻ x ∂μ, where f⁺ is the positive part of f and f⁻ is the negative part of f.
• integral_eq_lintegral_of_nonneg_ae : 0 ≤ᵐ[μ] f → ∫ x, f x ∂μ = ∫⁻ x, f x ∂μ
4. tendsto_integral_of_dominated_convergence : the Lebesgue dominated convergence theorem

## Notes

Some tips on how to prove a proposition if the API for the Bochner integral is not enough so that you need to unfold the definition of the Bochner integral and go back to simple functions.

One method is to use the theorem integrable.induction in the file set_integral, which allows you to prove something for an arbitrary measurable + integrable function.

Another method is using the following steps. See integral_eq_lintegral_max_sub_lintegral_min for a complicated example, which proves that ∫ f = ∫⁻ f⁺ - ∫⁻ f⁻, with the first integral sign being the Bochner integral of a real-valued function f : α → ℝ, and second and third integral sign being the integral on ennreal-valued functions (called lintegral). The proof of integral_eq_lintegral_max_sub_lintegral_min is scattered in sections with the name pos_part.

Here are the usual steps of proving that a property p, say ∫ f = ∫⁻ f⁺ - ∫⁻ f⁻, holds for all functions :

1. First go to the L¹ space.

For example, if you see ennreal.to_real (∫⁻ a, ennreal.of_real \$ ∥f a∥), that is the norm of f in L¹ space. Rewrite using l1.norm_of_fun_eq_lintegral_norm.

2. Show that the set {f ∈ L¹ | ∫ f = ∫⁻ f⁺ - ∫⁻ f⁻} is closed in L¹ using is_closed_eq.

3. Show that the property holds for all simple functions s in L¹ space.

Typically, you need to convert various notions to their simple_func counterpart, using lemmas like l1.integral_coe_eq_integral.

4. Since simple functions are dense in L¹,

univ = closure {s simple}
= closure {s simple | ∫ s = ∫⁻ s⁺ - ∫⁻ s⁻} : the property holds for all simple functions
⊆ closure {f | ∫ f = ∫⁻ f⁺ - ∫⁻ f⁻}
= {f | ∫ f = ∫⁻ f⁺ - ∫⁻ f⁻} : closure of a closed set is itself


Use is_closed_property or dense_range.induction_on for this argument.

## Notations

• α →ₛ E : simple functions (defined in measure_theory/integration)
• α →₁[μ] E : functions in L1 space, i.e., equivalence classes of integrable functions (defined in measure_theory/l1_space)
• α →₁ₛ[μ] E : simple functions in L1 space, i.e., equivalence classes of integrable simple functions

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

## Tags

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

def measure_theory.simple_func.pos_part {α : Type u_1} {E : Type u_2} [linear_order E] [has_zero E] (f : E) :

Positive part of a simple function.

Equations
def measure_theory.simple_func.neg_part {α : Type u_1} {E : Type u_2} [linear_order E] [has_zero E] [has_neg E] (f : E) :

Negative part of a simple function.

Equations
theorem measure_theory.simple_func.pos_part_map_norm {α : Type u_1} (f : ) :

theorem measure_theory.simple_func.neg_part_map_norm {α : Type u_1} (f : ) :

theorem measure_theory.simple_func.pos_part_sub_neg_part {α : Type u_1} (f : ) :
= 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.

theorem measure_theory.simple_func.integrable_iff_fin_meas_supp {α : Type u_1} {E : Type u_2} [normed_group E] {f : E} {μ : measure_theory.measure α} :

For simple functions with a normed_group as codomain, being integrable is the same as having finite volume support.

theorem measure_theory.simple_func.fin_meas_supp.integrable {α : Type u_1} {E : Type u_2} [normed_group E] {μ : measure_theory.measure α} {f : E} (h : f.fin_meas_supp μ) :

theorem measure_theory.simple_func.integrable_pair {α : Type u_1} {E : Type u_2} {F : Type u_3} [normed_group E] [normed_group F] {μ : measure_theory.measure α} {f : E} {g : F} :
μ

def measure_theory.simple_func.integral {α : Type u_1} {F : Type u_3} [normed_group F] [ F] (μ : measure_theory.measure α) (f : F) :
F

Bochner integral of simple functions whose codomain is a real normed_space.

Equations
theorem measure_theory.simple_func.integral_eq_sum_filter {α : Type u_1} {F : Type u_3} [normed_group F] [ F] (f : F) (μ : measure_theory.measure α) :
= ∑ (x : F) in finset.filter (λ (x : F), x 0) f.range, (μ (f ⁻¹' {x})).to_real x

theorem measure_theory.simple_func.integral_eq_sum_of_subset {α : Type u_1} {F : Type u_3} [normed_group F] [ F] {f : F} {μ : measure_theory.measure α} {s : finset F} (hs : finset.filter (λ (x : F), x 0) f.range s) :
= ∑ (x : F) in s, (μ (f ⁻¹' {x})).to_real x

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

theorem measure_theory.simple_func.map_integral {α : Type u_1} {E : Type u_2} {F : Type u_3} [normed_group E] [normed_group F] {μ : measure_theory.measure α} [ F] (f : E) (g : E → F) (hf : μ) (hg : g 0 = 0) :
= ∑ (x : E) in f.range, (μ (f ⁻¹' {x})).to_real 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 measure_theory.simple_func.integral_eq_lintegral' {α : Type u_1} {E : Type u_2} [normed_group E] {μ : measure_theory.measure α} {f : E} {g : E → ennreal} (hf : μ) (hg0 : g 0 = 0) (hgt : ∀ (b : E), g b < ) :
= (∫⁻ (a : α), g (f a) μ).to_real

simple_func.integral and simple_func.lintegral agree when the integrand has type α →ₛ ennreal. But since ennreal is not a normed_space, we need some form of coercion. See integral_eq_lintegral for a simpler version.

theorem measure_theory.simple_func.integral_congr {α : Type u_1} {E : Type u_2} [normed_group E] {μ : measure_theory.measure α} [ E] {f g : E} (hf : μ) (h : f =ᵐ[μ] g) :

theorem measure_theory.simple_func.integral_eq_lintegral {α : Type u_1} {μ : measure_theory.measure α} {f : } (hf : μ) (h_pos : 0 ≤ᵐ[μ] f) :
= (∫⁻ (a : α), ennreal.of_real (f a) μ).to_real

simple_func.bintegral and simple_func.integral agree when the integrand has type α →ₛ ennreal. But since ennreal is not a normed_space, we need some form of coercion.

theorem measure_theory.simple_func.integral_add {α : Type u_1} {E : Type u_2} [normed_group E] {μ : measure_theory.measure α} [ E] {f g : E} (hf : μ) (hg : μ) :

theorem measure_theory.simple_func.integral_neg {α : Type u_1} {E : Type u_2} [normed_group E] {μ : measure_theory.measure α} [ E] {f : E} (hf : μ) :

theorem measure_theory.simple_func.integral_sub {α : Type u_1} {E : Type u_2} [normed_group E] {μ : measure_theory.measure α} [ E] [borel_space E] {f g : E} (hf : μ) (hg : μ) :

theorem measure_theory.simple_func.integral_smul {α : Type u_1} {E : Type u_2} [normed_group E] {μ : measure_theory.measure α} [ E] (r : ) {f : E} (hf : μ) :

theorem measure_theory.simple_func.norm_integral_le_integral_norm {α : Type u_1} {E : Type u_2} [normed_group E] {μ : measure_theory.measure α} [ E] (f : E) (hf : μ) :

theorem measure_theory.simple_func.integral_add_measure {α : Type u_1} {E : Type u_2} [normed_group E] {μ : measure_theory.measure α} [ E] {ν : . "volume_tac"} (f : E) (hf : + ν)) :

def measure_theory.l1.simple_func (α : Type u_1) (E : Type u_2) [normed_group E] [borel_space E] (μ : measure_theory.measure α) :
Type (max u_1 u_2)

l1.simple_func is a subspace of L1 consisting of equivalence classes of an integrable simple function.

Equations

Simple functions in L1 space form a normed_space.

@[instance]

Equations
@[instance]

Equations
@[simp]
theorem measure_theory.l1.simple_func.coe_coe {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} (f : α →₁ₛ[μ] E) :

theorem measure_theory.l1.simple_func.eq {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} {f g : α →₁ₛ[μ] E} :
f = gf = g

theorem measure_theory.l1.simple_func.eq' {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} {f g : α →₁ₛ[μ] E} :
f = gf = g

theorem measure_theory.l1.simple_func.eq_iff {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} {f g : α →₁ₛ[μ] E} :
f = g f = g

theorem measure_theory.l1.simple_func.eq_iff' {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} {f g : α →₁ₛ[μ] E} :
f = g f = g

L1 simple functions forms a emetric_space, with the emetric being inherited from L1 space, i.e., edist f g = ∫⁻ a, edist (f a) (g a). Not declared as an instance as α →₁ₛ[μ] β will only be useful in the construction of the Bochner integral.

Equations

L1 simple functions forms a metric_space, with the metric being inherited from L1 space, i.e., dist f g = ennreal.to_real (∫⁻ a, edist (f a) (g a)). Not declared as an instance as α →₁ₛ[μ] β will only be useful in the construction of the Bochner integral.

Equations

Functions α →₁ₛ[μ] E form an additive commutative group.

Equations
@[instance]
def measure_theory.l1.simple_func.inhabited {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} :

Equations
@[simp]
theorem measure_theory.l1.simple_func.coe_zero {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} :
0 = 0

@[simp]
theorem measure_theory.l1.simple_func.coe_add {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} (f g : α →₁ₛ[μ] E) :
(f + g) = f + g

@[simp]
theorem measure_theory.l1.simple_func.coe_neg {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} (f : α →₁ₛ[μ] E) :

@[simp]
theorem measure_theory.l1.simple_func.coe_sub {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} (f g : α →₁ₛ[μ] E) :
(f - g) = f - g

@[simp]
theorem measure_theory.l1.simple_func.edist_eq {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} (f g : α →₁ₛ[μ] E) :
g = g

@[simp]
theorem measure_theory.l1.simple_func.dist_eq {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} (f g : α →₁ₛ[μ] E) :
dist f g = g

def measure_theory.l1.simple_func.has_norm {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} :

The norm on α →₁ₛ[μ] E is inherited from L1 space. That is, ∥f∥ = ∫⁻ a, edist (f a) 0. Not declared as an instance as α →₁ₛ[μ] E will only be useful in the construction of the Bochner integral.

Equations
theorem measure_theory.l1.simple_func.norm_eq {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} (f : α →₁ₛ[μ] E) :

theorem measure_theory.l1.simple_func.norm_eq' {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} (f : α →₁ₛ[μ] E) :

Not declared as an instance as α →₁ₛ[μ] E will only be useful in the construction of the Bochner integral.

Equations
def measure_theory.l1.simple_func.has_scalar {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} {𝕜 : Type u_4} [normed_field 𝕜] [ E] :
→₁ₛ[μ] E)

Not declared as an instance as α →₁ₛ[μ] E will only be useful in the construction of the Bochner integral.

Equations
@[simp]
theorem measure_theory.l1.simple_func.coe_smul {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} {𝕜 : Type u_4} [normed_field 𝕜] [ E] (c : 𝕜) (f : α →₁ₛ[μ] E) :
(c f) = c f

def measure_theory.l1.simple_func.semimodule {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} {𝕜 : Type u_4} [normed_field 𝕜] [ E] :
→₁ₛ[μ] E)

Not declared as an instance as α →₁ₛ[μ] E will only be useful in the construction of the Bochner integral.

Equations
def measure_theory.l1.simple_func.normed_space {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} {𝕜 : Type u_4} [normed_field 𝕜] [ E] :
→₁ₛ[μ] E)

Not declared as an instance as α →₁ₛ[μ] E will only be useful in the construction of the Bochner integral.

Equations
def measure_theory.l1.simple_func.of_simple_func {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} (f : E) (hf : μ) :

Construct the equivalence class [f] of an integrable simple function f.

Equations
theorem measure_theory.l1.simple_func.of_simple_func_eq_of_fun {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} (f : E) (hf : μ) :

theorem measure_theory.l1.simple_func.of_simple_func_eq_mk {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} (f : E) (hf : μ) :

theorem measure_theory.l1.simple_func.of_simple_func_add {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} (f g : E) (hf : μ) (hg : μ) :

theorem measure_theory.l1.simple_func.of_simple_func_neg {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} (f : E) (hf : μ) :

theorem measure_theory.l1.simple_func.of_simple_func_sub {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} (f g : E) (hf : μ) (hg : μ) :

theorem measure_theory.l1.simple_func.of_simple_func_smul {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} {𝕜 : Type u_4} [normed_field 𝕜] [ E] (f : E) (hf : μ) (c : 𝕜) :

theorem measure_theory.l1.simple_func.norm_of_simple_func {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} (f : E) (hf : μ) :
= (∫⁻ (a : α), edist (f a) 0 μ).to_real

def measure_theory.l1.simple_func.to_simple_func {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} (f : α →₁ₛ[μ] E) :

Find a representative of a l1.simple_func.

Equations
theorem measure_theory.l1.simple_func.measurable {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} (f : α →₁ₛ[μ] E) :

f.to_simple_func is measurable.

theorem measure_theory.l1.simple_func.ae_measurable {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} (f : α →₁ₛ[μ] E) :

theorem measure_theory.l1.simple_func.integrable {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} (f : α →₁ₛ[μ] E) :

f.to_simple_func is integrable.

theorem measure_theory.l1.simple_func.to_simple_func_of_simple_func {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} (f : E) (hfi : μ) :

theorem measure_theory.l1.simple_func.smul_to_simple_func {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} {𝕜 : Type u_4} [normed_field 𝕜] [ E] (k : 𝕜) (f : α →₁ₛ[μ] E) :

theorem measure_theory.l1.simple_func.dist_to_simple_func {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} (f g : α →₁ₛ[μ] E) :

theorem measure_theory.l1.simple_func.norm_to_simple_func {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} (f : α →₁ₛ[μ] E) :

theorem measure_theory.l1.simple_func.norm_eq_integral {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} (f : α →₁ₛ[μ] E) :

theorem measure_theory.l1.simple_func.uniform_continuous {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} :

theorem measure_theory.l1.simple_func.uniform_embedding {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} :

theorem measure_theory.l1.simple_func.uniform_inducing {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} :

theorem measure_theory.l1.simple_func.dense_embedding {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} :

theorem measure_theory.l1.simple_func.dense_inducing {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} :

theorem measure_theory.l1.simple_func.dense_range {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} :

def measure_theory.l1.simple_func.coe_to_l1 (α : Type u_1) (E : Type u_2) [normed_group E] [borel_space E] {μ : measure_theory.measure α} (𝕜 : Type u_4) [normed_field 𝕜] [ E] :
→₁ₛ[μ] E) →L[𝕜] α →₁[μ] E

The uniform and dense embedding of L1 simple functions into L1 functions.

Equations

Positive part of a simple function in L1 space.

Equations

Negative part of a simple function in L1 space.

Equations

Define the Bochner integral on α →₁ₛ[μ] E and prove basic properties of this integral.

def measure_theory.l1.simple_func.integral {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} [ E] (f : α →₁ₛ[μ] E) :
E

The Bochner integral over simple functions in l1 space.

Equations
theorem measure_theory.l1.simple_func.integral_eq_integral {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} [ E] (f : α →₁ₛ[μ] E) :

theorem measure_theory.l1.simple_func.integral_congr {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} [ E] {f g : α →₁ₛ[μ] E} (h : (f.to_simple_func) =ᵐ[μ] (g.to_simple_func)) :

theorem measure_theory.l1.simple_func.integral_add {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} [ E] (f g : α →₁ₛ[μ] E) :
(f + g).integral =

theorem measure_theory.l1.simple_func.integral_smul {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} [ E] (r : ) (f : α →₁ₛ[μ] E) :

theorem measure_theory.l1.simple_func.norm_integral_le_norm {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} [ E] (f : α →₁ₛ[μ] E) :

def measure_theory.l1.simple_func.integral_clm {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} [ E] :

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

Equations
theorem measure_theory.l1.simple_func.norm_Integral_le_one {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} [ E] :

def measure_theory.l1.integral_clm {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} [ E]  :
→₁[μ] E) →L[] E

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

Equations
def measure_theory.l1.integral {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} [ E] (f : α →₁[μ] E) :
E

The Bochner integral in l1 space

Equations
theorem measure_theory.l1.integral_eq {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} [ E] (f : α →₁[μ] E) :

theorem measure_theory.l1.simple_func.integral_l1_eq_integral {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} [ E] (f : α →₁ₛ[μ] E) :

@[simp]
theorem measure_theory.l1.integral_zero (α : Type u_1) (E : Type u_2) [normed_group E] [borel_space E] {μ : measure_theory.measure α} [ E]  :

theorem measure_theory.l1.integral_add {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} [ E] (f g : α →₁[μ] E) :
(f + g).integral =

theorem measure_theory.l1.integral_neg {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} [ E] (f : α →₁[μ] E) :

theorem measure_theory.l1.integral_sub {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} [ E] (f g : α →₁[μ] E) :
(f - g).integral =

theorem measure_theory.l1.integral_smul {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} [ E] (r : ) (f : α →₁[μ] E) :

theorem measure_theory.l1.norm_Integral_le_one {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} [ E]  :

theorem measure_theory.l1.norm_integral_le {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} [ E] (f : α →₁[μ] E) :

theorem measure_theory.l1.continuous_integral {α : Type u_1} {E : Type u_2} [normed_group E] [borel_space E] {μ : measure_theory.measure α} [ E]  :
continuous (λ (f : α →₁[μ] E), f.integral)

def measure_theory.integral {α : Type u_1} {E : Type u_2} [normed_group E] [ E] [borel_space E] (μ : measure_theory.measure α) (f : α → E) :
E

The Bochner integral

Equations

In the notation for integrals, an expression like ∫ x, g ∥x∥ ∂μ will not be parsed correctly, and needs parentheses. We do not set the binding power of r to 0, because then ∫ x, f x = 0 will be parsed incorrectly.

theorem measure_theory.integral_eq {α : Type u_1} {E : Type u_2} [normed_group E] [ E] [borel_space E] {μ : measure_theory.measure α} (f : α → E) (hf : μ) :
(a : α), f a μ = hf).integral

theorem measure_theory.l1.integral_eq_integral {α : Type u_1} {E : Type u_2} [normed_group E] [ E] [borel_space E] {μ : measure_theory.measure α} (f : α →₁[μ] E) :
f.integral = (a : α), f a μ

theorem measure_theory.integral_undef {α : Type u_1} {E : Type u_2} [normed_group E] [ E] [borel_space E] {f : α → E} {μ : measure_theory.measure α} (h : ¬) :
(a : α), f a μ = 0

theorem measure_theory.integral_non_ae_measurable {α : Type u_1} {E : Type u_2} [normed_group E] [ E] [borel_space E] {f : α → E} {μ : measure_theory.measure α} (h : ¬) :
(a : α), f a μ = 0

theorem measure_theory.integral_zero (α : Type u_1) (E : Type u_2) [normed_group E] [ E] [borel_space E] {μ : measure_theory.measure α} :
(a : α), 0 μ = 0

@[simp]
theorem measure_theory.integral_zero' (α : Type u_1) (E : Type u_2) [normed_group E] [ E] [borel_space E] {μ : measure_theory.measure α} :

theorem measure_theory.integral_add {α : Type u_1} {E : Type u_2} [normed_group E] [ E] [borel_space E] {f g : α → E} {μ : measure_theory.measure α} (hf : μ) (hg : μ) :
(a : α), f a + g a μ = (a : α), f a μ + (a : α), g a μ

theorem measure_theory.integral_add' {α : Type u_1} {E : Type u_2} [normed_group E] [ E] [borel_space E] {f g : α → E} {μ : measure_theory.measure α} (hf : μ) (hg : μ) :
(a : α), (f + g) a μ = (a : α), f a μ + (a : α), g a μ

theorem measure_theory.integral_neg {α : Type u_1} {E : Type u_2} [normed_group E] [ E] [borel_space E] {μ : measure_theory.measure α} (f : α → E) :
(a : α), -f a μ = - (a : α), f a μ

theorem measure_theory.integral_neg' {α : Type u_1} {E : Type u_2} [normed_group E] [ E] [borel_space E] {μ : measure_theory.measure α} (f : α → E) :
(a : α), (-f) a μ = - (a : α), f a μ

theorem measure_theory.integral_sub {α : Type u_1} {E : Type u_2} [normed_group E] [ E] [borel_space E] {f g : α → E} {μ : measure_theory.measure α} (hf : μ) (hg : μ) :
(a : α), f a - g a μ = (a : α), f a μ - (a : α), g a μ

theorem measure_theory.integral_sub' {α : Type u_1} {E : Type u_2} [normed_group E] [ E] [borel_space E] {f g : α → E} {μ : measure_theory.measure α} (hf : μ) (hg : μ) :
(a : α), (f - g) a μ = (a : α), f a μ - (a : α), g a μ

theorem measure_theory.integral_smul {α : Type u_1} {E : Type u_2} [normed_group E] [ E] [borel_space E] {μ : measure_theory.measure α} (r : ) (f : α → E) :
(a : α), r f a μ = r (a : α), f a μ

theorem measure_theory.integral_mul_left {α : Type u_1} {μ : measure_theory.measure α} (r : ) (f : α → ) :
(a : α), r * f a μ = r * (a : α), f a μ

theorem measure_theory.integral_mul_right {α : Type u_1} {μ : measure_theory.measure α} (r : ) (f : α → ) :
(a : α), (f a) * r μ = ( (a : α), f a μ) * r

theorem measure_theory.integral_div {α : Type u_1} {μ : measure_theory.measure α} (r : ) (f : α → ) :
(a : α), f a / r μ = (a : α), f a μ / r

theorem measure_theory.integral_congr_ae {α : Type u_1} {E : Type u_2} [normed_group E] [ E] [borel_space E] {f g : α → E} {μ : measure_theory.measure α} (h : f =ᵐ[μ] g) :
(a : α), f a μ = (a : α), g a μ

@[simp]
theorem measure_theory.l1.integral_of_fun_eq_integral {α : Type u_1} {E : Type u_2} [normed_group E] [ E] [borel_space E] {μ : measure_theory.measure α} {f : α → E} (hf : μ) :
(a : α), hf) a μ = (a : α), f a μ

theorem measure_theory.continuous_integral {α : Type u_1} {E : Type u_2} [normed_group E] [ E] [borel_space E] {μ : measure_theory.measure α} :
continuous (λ (f : α →₁[μ] E), (a : α), f a μ)

theorem measure_theory.norm_integral_le_lintegral_norm {α : Type u_1} {E : Type u_2} [normed_group E] [ E] [borel_space E] {μ : measure_theory.measure α} (f : α → E) :
(a : α), f a μ (∫⁻ (a : α), μ).to_real

theorem measure_theory.ennnorm_integral_le_lintegral_ennnorm {α : Type u_1} {E : Type u_2} [normed_group E] [ E] [borel_space E] {μ : measure_theory.measure α} (f : α → E) :
(nnnorm ( (a : α), f a μ)) ∫⁻ (a : α), (nnnorm (f a)) μ

theorem measure_theory.integral_eq_zero_of_ae {α : Type u_1} {E : Type u_2} [normed_group E] [ E] [borel_space E] {μ : measure_theory.measure α} {f : α → E} (hf : f =ᵐ[μ] 0) :
(a : α), f a μ = 0

theorem measure_theory.has_finite_integral.tendsto_set_integral_nhds_zero {α : Type u_1} {E : Type u_2} [normed_group E] [ E] [borel_space E] {μ : measure_theory.measure α} {ι : Type u_3} {f : α → E} (hf : μ) {l : filter ι} {s : ι → set α} (hs : filter.tendsto (μ s) l (𝓝 0)) :
filter.tendsto (λ (i : ι), (x : α) in s i, f x μ) l (𝓝 0)

If f has finite integral, then ∫ x in s, f x ∂μ is absolutely continuous in s: it tends to zero as μ s tends to zero.

theorem measure_theory.integrable.tendsto_set_integral_nhds_zero {α : Type u_1} {E : Type u_2} [normed_group E] [ E] [borel_space E] {μ : measure_theory.measure α} {ι : Type u_3} {f : α → E} (hf : μ) {l : filter ι} {s : ι → set α} (hs : filter.tendsto (μ s) l (𝓝 0)) :
filter.tendsto (λ (i : ι), (x : α) in s i, f x μ) l (𝓝 0)

If f is integrable, then ∫ x in s, f x ∂μ is absolutely continuous in s: it tends to zero as μ s tends to zero.

theorem measure_theory.tendsto_integral_of_l1 {α : Type u_1} {E : Type u_2} [normed_group E] [ E] [borel_space E] {μ : measure_theory.measure α} {ι : Type u_3} (f : α → E) (hfi : μ) {F : ι → α → E} {l : filter ι} (hFi : ∀ᶠ (i : ι) in l, μ) (hF : filter.tendsto (λ (i : ι), ∫⁻ (x : α), edist (F i x) (f x) μ) l (𝓝 0)) :
filter.tendsto (λ (i : ι), (x : α), F i x μ) l (𝓝 ( (x : α), f x μ))

If F i → f in L1, then ∫ x, F i x ∂μ → ∫ x, f x∂μ.

theorem measure_theory.tendsto_integral_of_dominated_convergence {α : Type u_1} {E : Type u_2} [normed_group E] [ E] [borel_space E] {μ : measure_theory.measure α} {F : α → E} {f : α → E} (bound : α → ) (F_measurable : ∀ (n : ), ae_measurable (F n) μ) (f_measurable : μ) (bound_integrable : μ) (h_bound : ∀ (n : ), ∀ᵐ (a : α) ∂μ, F n a bound a) (h_lim : ∀ᵐ (a : α) ∂μ, filter.tendsto (λ (n : ), F n a) filter.at_top (𝓝 (f a))) :
filter.tendsto (λ (n : ), (a : α), F n a μ) filter.at_top (𝓝 ( (a : α), f a μ))

Lebesgue dominated convergence theorem provides sufficient conditions under which almost everywhere convergence of a sequence of functions implies the convergence of their integrals.

theorem measure_theory.tendsto_integral_filter_of_dominated_convergence {α : Type u_1} {E : Type u_2} [normed_group E] [ E] [borel_space E] {μ : measure_theory.measure α} {ι : Type u_3} {l : filter ι} {F : ι → α → E} {f : α → E} (bound : α → ) (hl_cb : l.is_countably_generated) (hF_meas : ∀ᶠ (n : ι) in l, ae_measurable (F n) μ) (f_measurable : μ) (h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a bound a) (bound_integrable : μ) (h_lim : ∀ᵐ (a : α) ∂μ, filter.tendsto (λ (n : ι), F n a) l (𝓝 (f a))) :
filter.tendsto (λ (n : ι), (a : α), F n a μ) l (𝓝 ( (a : α), f a μ))

Lebesgue dominated convergence theorem for filters with a countable basis

theorem measure_theory.integral_eq_lintegral_max_sub_lintegral_min {α : Type u_1} {μ : measure_theory.measure α} {f : α → } (hf : μ) :
(a : α), f a μ = (∫⁻ (a : α), ennreal.of_real (max (f a) 0) μ).to_real - (∫⁻ (a : α), ennreal.of_real (-min (f a) 0) μ).to_real

The Bochner integral of a real-valued function f : α → ℝ is the difference between the integral of the positive part of f and the integral of the negative part of f.

theorem measure_theory.integral_eq_lintegral_of_nonneg_ae {α : Type u_1} {μ : measure_theory.measure α} {f : α → } (hf : 0 ≤ᵐ[μ] f) (hfm : μ) :
(a : α), f a μ = (∫⁻ (a : α), ennreal.of_real (f a) μ).to_real

theorem measure_theory.integral_nonneg_of_ae {α : Type u_1} {μ : measure_theory.measure α} {f : α → } (hf : 0 ≤ᵐ[μ] f) :
0 (a : α), f a μ

theorem measure_theory.lintegral_coe_eq_integral {α : Type u_1} {μ : measure_theory.measure α} (f : α → ℝ≥0) (hfi : measure_theory.integrable (λ (x : α), (f x)) μ) :
∫⁻ (a : α), (f a) μ = ennreal.of_real ( (a : α), (f a) μ)

theorem measure_theory.integral_to_real {α : Type u_1} {μ : measure_theory.measure α} {f : α → ennreal} (hfm : μ) (hf : ∀ᵐ (x : α) ∂μ, f x < ) :
(a : α), (f a).to_real μ = (∫⁻ (a : α), f a μ).to_real

theorem measure_theory.integral_nonneg {α : Type u_1} {μ : measure_theory.measure α} {f : α → } (hf : 0 f) :
0 (a : α), f a μ

theorem measure_theory.integral_nonpos_of_ae {α : Type u_1} {μ : measure_theory.measure α} {f : α → } (hf : f ≤ᵐ[μ] 0) :
(a : α), f a μ 0

theorem measure_theory.integral_nonpos {α : Type u_1} {μ : measure_theory.measure α} {f : α → } (hf : f 0) :
(a : α), f a μ 0

theorem measure_theory.integral_eq_zero_iff_of_nonneg_ae {α : Type u_1} {μ : measure_theory.measure α} {f : α → } (hf : 0 ≤ᵐ[μ] f) (hfi : μ) :
(x : α), f x μ = 0 f =ᵐ[μ] 0

theorem measure_theory.integral_eq_zero_iff_of_nonneg {α : Type u_1} {μ : measure_theory.measure α} {f : α → } (hf : 0 f) (hfi : μ) :
(x : α), f x μ = 0 f =ᵐ[μ] 0

theorem measure_theory.integral_pos_iff_support_of_nonneg_ae {α : Type u_1} {μ : measure_theory.measure α} {f : α → } (hf : 0 ≤ᵐ[μ] f) (hfi : μ) :
0 < (x : α), f x μ 0 < μ

theorem measure_theory.integral_pos_iff_support_of_nonneg {α : Type u_1} {μ : measure_theory.measure α} {f : α → } (hf : 0 f) (hfi : μ) :
0 < (x : α), f x μ 0 < μ

theorem measure_theory.l1.norm_eq_integral_norm {α : Type u_1} {μ : measure_theory.measure α} {H : Type u_4} [normed_group H] [borel_space H] (f : α →₁[μ] H) :
f = (a : α), f a μ

theorem measure_theory.l1.norm_of_fun_eq_integral_norm {α : Type u_1} {μ : measure_theory.measure α} {H : Type u_4} [normed_group H] [borel_space H] {f : α → H} (hf : μ) :
= (a : α), f a μ

theorem measure_theory.integral_mono_ae {α : Type u_1} {μ : measure_theory.measure α} {f g : α → } (hf : μ) (hg : μ) (h : f ≤ᵐ[μ] g) :
(a : α), f a μ (a : α), g a μ

theorem measure_theory.integral_mono {α : Type u_1} {μ : measure_theory.measure α} {f g : α → } (hf : μ) (hg : μ) (h : f g) :
(a : α), f a μ (a : α), g a μ

theorem measure_theory.integral_mono_of_nonneg {α : Type u_1} {μ : measure_theory.measure α} {f g : α → } (hf : 0 ≤ᵐ[μ] f) (hgi : μ) (h : f ≤ᵐ[μ] g) :
(a : α), f a μ (a : α), g a μ

theorem measure_theory.norm_integral_le_integral_norm {α : Type u_1} {E : Type u_2} [normed_group E] [ E] [borel_space E] {μ : measure_theory.measure α} (f : α → E) :
(a : α), f a μ (a : α), f a μ

theorem measure_theory.norm_integral_le_of_norm_le {α : Type u_1} {E : Type u_2} [normed_group E] [ E] [borel_space E] {μ : measure_theory.measure α} {f : α → E} {g : α → } (hg : μ) (h : ∀ᵐ (x : α) ∂μ, f x g x) :
(x : α), f x μ (x : α), g x μ

theorem measure_theory.integral_finset_sum {α : Type u_1} {E : Type u_2} [normed_group E] [ E] [borel_space E] {μ : measure_theory.measure α} {ι : Type u_3} (s : finset ι) {f : ι → α → E} (hf : ∀ (i : ι), μ) :
(a : α), ∑ (i : ι) in s, f i a μ = ∑ (i : ι) in s, (a : α), f i a μ

theorem measure_theory.simple_func.integral_eq_integral {α : Type u_1} {E : Type u_2} [normed_group E] [ E] [borel_space E] {μ : measure_theory.measure α} (f : E) (hfi : μ) :
= (x : α), f x μ

@[simp]
theorem measure_theory.integral_const {α : Type u_1} {E : Type u_2} [normed_group E] [ E] [borel_space E] {μ : measure_theory.measure α} (c : E) :
(x : α), c μ = (μ set.univ).to_real c

theorem measure_theory.norm_integral_le_of_norm_le_const {α : Type u_1} {E : Type u_2} [normed_group E] [ E] [borel_space E] {μ : measure_theory.measure α} {f : α → E} {C : } (h : ∀ᵐ (x : α) ∂μ, f x C) :
(x : α), f x μ C * (μ set.univ).to_real

theorem measure_theory.tendsto_integral_approx_on_univ_of_measurable {α : Type u_1} {E : Type u_2} [normed_group E] [ E] [borel_space E] {μ : measure_theory.measure α} {f : α → E} (fmeas : measurable f) (hf : μ) :
filter.tendsto (λ (n : ), filter.at_top (𝓝 ( (x : α), f x μ))

theorem measure_theory.integral_add_measure {α : Type u_1} {E : Type u_2} [normed_group E] [ E] [borel_space E] {μ ν : measure_theory.measure α} {f : α → E} (hμ : μ) (hν : ν) :
(x : α), f x + ν) = (x : α), f x μ + (x : α), f x ν

@[simp]
theorem measure_theory.integral_zero_measure {α : Type u_1} {E : Type u_2} [normed_group E] [ E] [borel_space E] (f : α → E) :
(x : α), f x 0 = 0

@[simp]
theorem measure_theory.integral_smul_measure {α : Type u_1} {E : Type u_2} [normed_group E] [ E] [borel_space E] {μ : measure_theory.measure α} (f : α → E) (c : ennreal) :
(x : α), f x c μ = c.to_real (x : α), f x μ

theorem measure_theory.integral_map_of_measurable {α : Type u_1} {E : Type u_2} [normed_group E] [ E] [borel_space E] {μ : measure_theory.measure α} {β : Type u_3} {φ : α → β} (hφ : measurable φ) {f : β → E} (hfm : measurable f) :
(y : β), f y = (x : α), f (φ x) μ

theorem measure_theory.integral_map {α : Type u_1} {E : Type u_2} [normed_group E] [ E] [borel_space E] {μ : measure_theory.measure α} {β : Type u_3} {φ : α → β} (hφ : measurable φ) {f : β → E} (hfm : μ)) :
(y : β), f y = (x : α), f (φ x) μ

theorem measure_theory.integral_dirac' {α : Type u_1} {E : Type u_2} [normed_group E] [ E] [borel_space E] (f : α → E) (a : α) (hfm : measurable f) :
(x : α), f x = f a

theorem measure_theory.integral_dirac {α : Type u_1} {E : Type u_2} [normed_group E] [ E] [borel_space E] (f : α → E) (a : α) :
(x : α), f x = f a

Simp set for integral rules.