# mathlibdocumentation

measure_theory.integral.bochner

# 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 through the extension process described in the file `set_to_L1`, which follows these steps:

1. Define the integral of the indicator of a set. This is `weighted_smul μ s x = (μ s).to_real * x`. `weighted_smul μ` is shown to be linear in the value `x` and `dominated_fin_meas_additive` (defined in the file `set_to_L1`) with respect to the set `s`.

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

3. Transfer this definition to define the integral on `L1.simple_func α E` (notation : `α →₁ₛ[μ] E`), see `L1.simple_func.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 `continuous_linear_map.extend` and the fact that the embedding of `α →₁ₛ[μ] E` into `α →₁[μ] E` is dense.

5. Define the Bochner integral on functions as the Bochner integral of its equivalence class in L1 space, if it is in L1, and 0 otherwise.

The result of that construction is `∫ a, f a ∂μ`, which is definitionally equal to `set_to_fun (dominated_fin_meas_additive_weighted_smul μ) f`. Some basic properties of the integral (like linearity) are particular cases of the properties of `set_to_fun` (which are described in the file `set_to_L1`).

## 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∥ ∂μ`
1. 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 ∂μ`
1. Propositions connecting the Bochner integral with the integral on `ℝ≥0∞`-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 ∂μ`
1. `tendsto_integral_of_dominated_convergence` : the Lebesgue dominated convergence theorem

2. (In the file `set_integral`) integration commutes with continuous linear maps.

• `continuous_linear_map.integral_comp_comm`
• `linear_isometry.integral_comp_comm`

## 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 `simple_func_dense_lp` (or one of the related results, like `Lp.induction` for functions in `Lp`), which allows you to prove something for an arbitrary 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 `ℝ≥0∞`-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/lp_space`)
• `α →₁ₛ[μ] E` : simple functions in L1 space, i.e., equivalence classes of integrable simple functions (defined in `measure_theory/simple_func_dense`)
• `∫ a, f a ∂μ` : integral of `f` with respect to a measure `μ`
• `∫ a, f a` : integral of `f` with respect to `volume`, the default measure on the ambient type

We also define notations for integral on a set, which are described in the file `measure_theory/set_integral`.

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

noncomputable def measure_theory.weighted_smul {α : Type u_1} {F : Type u_3} [normed_group F] [ F] {m : measurable_space α} (μ : measure_theory.measure α) (s : set α) :

Given a set `s`, return the continuous linear map `λ x, (μ s).to_real • x`. The extension of that set function through `set_to_L1` gives the Bochner integral of L1 functions.

Equations
theorem measure_theory.weighted_smul_apply {α : Type u_1} {F : Type u_3} [normed_group F] [ F] {m : measurable_space α} (μ : measure_theory.measure α) (s : set α) (x : F) :
= (μ s).to_real x
@[simp]
theorem measure_theory.weighted_smul_zero_measure {α : Type u_1} {F : Type u_3} [normed_group F] [ F] {m : measurable_space α} :
@[simp]
theorem measure_theory.weighted_smul_empty {α : Type u_1} {F : Type u_3} [normed_group F] [ F] {m : measurable_space α} (μ : measure_theory.measure α) :
theorem measure_theory.weighted_smul_add_measure {α : Type u_1} {F : Type u_3} [normed_group F] [ F] {m : measurable_space α} (μ ν : measure_theory.measure α) {s : set α} (hμs : μ s ) (hνs : ν s ) :
theorem measure_theory.weighted_smul_smul_measure {α : Type u_1} {F : Type u_3} [normed_group F] [ F] {m : measurable_space α} (μ : measure_theory.measure α) (c : ennreal) {s : set α} :
s =
theorem measure_theory.weighted_smul_congr {α : Type u_1} {F : Type u_3} [normed_group F] [ F] {m : measurable_space α} {μ : measure_theory.measure α} (s t : set α) (hst : μ s = μ t) :
theorem measure_theory.weighted_smul_null {α : Type u_1} {F : Type u_3} [normed_group F] [ F] {m : measurable_space α} {μ : measure_theory.measure α} {s : set α} (h_zero : μ s = 0) :
theorem measure_theory.weighted_smul_union' {α : Type u_1} {F : Type u_3} [normed_group F] [ F] {m : measurable_space α} {μ : measure_theory.measure α} (s t : set α) (ht : measurable_set t) (hs_finite : μ s ) (ht_finite : μ t ) (h_inter : s t = ) :
@[nolint]
theorem measure_theory.weighted_smul_union {α : Type u_1} {F : Type u_3} [normed_group F] [ F] {m : measurable_space α} {μ : measure_theory.measure α} (s t : set α) (hs : measurable_set s) (ht : measurable_set t) (hs_finite : μ s ) (ht_finite : μ t ) (h_inter : s t = ) :
theorem measure_theory.weighted_smul_smul {α : Type u_1} {F : Type u_3} {𝕜 : Type u_4} [normed_group F] [ F] {m : measurable_space α} {μ : measure_theory.measure α} [normed_field 𝕜] [ F] [ F] (c : 𝕜) (s : set α) (x : F) :
(c x) = c
theorem measure_theory.norm_weighted_smul_le {α : Type u_1} {F : Type u_3} [normed_group F] [ F] {m : measurable_space α} {μ : measure_theory.measure α} (s : set α) :
(μ s).to_real
theorem measure_theory.dominated_fin_meas_additive_weighted_smul {α : Type u_1} {F : Type u_3} [normed_group F] [ F] {m : measurable_space α} (μ : measure_theory.measure α) :
theorem measure_theory.weighted_smul_nonneg {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (s : set α) (x : ) (hx : 0 x) :
0
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.

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

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

Equations
theorem measure_theory.simple_func.integral_def {α : Type u_1} {F : Type u_3} [normed_group F] [ F] {m : measurable_space α} (μ : measure_theory.measure α) (f : F) :
theorem measure_theory.simple_func.integral_eq {α : Type u_1} {F : Type u_3} [normed_group F] [ F] {m : measurable_space α} (μ : measure_theory.measure α) (f : F) :
= f.range.sum (λ (x : F), (μ (f ⁻¹' {x})).to_real x)
theorem measure_theory.simple_func.integral_eq_sum_filter {α : Type u_1} {F : Type u_3} [normed_group F] [ F] [decidable_pred (λ (x : F), x 0)] {m : measurable_space α} (f : F) (μ : measure_theory.measure α) :
= (finset.filter (λ (x : F), x 0) f.range).sum (λ (x : F), (μ (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] {m : measurable_space α} {μ : measure_theory.measure α} [decidable_pred (λ (x : F), x 0)] {f : F} {s : finset F} (hs : finset.filter (λ (x : F), x 0) f.range s) :
= s.sum (λ (x : F), (μ (f ⁻¹' {x})).to_real x)

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

@[simp]
theorem measure_theory.simple_func.integral_const {α : Type u_1} {F : Type u_3} [normed_group F] [ F] {m : measurable_space α} (μ : measure_theory.measure α) (y : F) :
@[simp]
theorem measure_theory.simple_func.integral_piecewise_zero {α : Type u_1} {F : Type u_3} [normed_group F] [ F] {m : measurable_space α} (f : F) (μ : measure_theory.measure α) {s : set α} (hs : measurable_set s) :
theorem measure_theory.simple_func.map_integral {α : Type u_1} {E : Type u_2} {F : Type u_3} [normed_group E] [normed_group F] [ F] {m : measurable_space α} {μ : measure_theory.measure α} (f : E) (g : E → F) (hf : μ) (hg : g 0 = 0) :
= f.range.sum (λ (x : E), (μ (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] {m : measurable_space α} {μ : measure_theory.measure α} {f : E} {g : E → ennreal} (hf : μ) (hg0 : g 0 = 0) (ht : ∀ (b : E), g b ) :
= (∫⁻ (a : α), g (f a) μ).to_real

`simple_func.integral` and `simple_func.lintegral` agree when the integrand has type `α →ₛ ℝ≥0∞`. But since `ℝ≥0∞` 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] {m : measurable_space α} {μ : measure_theory.measure α} [ E] {f g : E} (hf : μ) (h : f =ᵐ[μ] g) :
theorem measure_theory.simple_func.integral_eq_lintegral {α : Type u_1} {m : measurable_space α} {μ : 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 `α →ₛ ℝ≥0∞`. But since `ℝ≥0∞` 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] {m : measurable_space α} {μ : 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] {m : measurable_space α} {μ : measure_theory.measure α} [ E] {f : E} (hf : μ) :
theorem measure_theory.simple_func.integral_sub {α : Type u_1} {E : Type u_2} [normed_group E] {m : measurable_space α} {μ : measure_theory.measure α} [ E] {f g : E} (hf : μ) (hg : μ) :
theorem measure_theory.simple_func.integral_smul {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [normed_group E] {m : measurable_space α} {μ : measure_theory.measure α} [normed_field 𝕜] [ E] [ E] [ E] (c : 𝕜) {f : E} (hf : μ) :
theorem measure_theory.simple_func.norm_set_to_simple_func_le_integral_norm {α : Type u_1} {E : Type u_2} {F : Type u_3} [normed_group E] [normed_group F] [ F] {m : measurable_space α} {μ : measure_theory.measure α} [ E] (T : set α(E →L[] F)) {C : } (hT_norm : ∀ (s : set α), μ s < T s C * (μ s).to_real) {f : E} (hf : μ) :
theorem measure_theory.simple_func.norm_integral_le_integral_norm {α : Type u_1} {E : Type u_2} [normed_group E] {m : measurable_space α} {μ : 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] {m : measurable_space α} {μ : measure_theory.measure α} [ E] {ν : . "volume_tac"} (f : E) (hf : + ν)) :
theorem measure_theory.L1.simple_func.norm_eq_integral {α : Type u_1} {E : Type u_2} [normed_group E] {m : measurable_space α} {μ : measure_theory.measure α} (f : ) :
noncomputable def measure_theory.L1.simple_func.pos_part {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (f : ) :

Positive part of a simple function in L1 space.

Equations
noncomputable def measure_theory.L1.simple_func.neg_part {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (f : ) :

Negative part of a simple function in L1 space.

Equations
@[norm_cast]
theorem measure_theory.L1.simple_func.coe_pos_part {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (f : ) :
@[norm_cast]
theorem measure_theory.L1.simple_func.coe_neg_part {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (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.

noncomputable def measure_theory.L1.simple_func.integral {α : Type u_1} {E : Type u_2} [normed_group E] {m : measurable_space α} {μ : measure_theory.measure α} [ E] (f : ) :
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] {m : measurable_space α} {μ : measure_theory.measure α} [ E] (f : ) :
theorem measure_theory.L1.simple_func.integral_eq_lintegral {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : } (h_pos : 0 ≤ᵐ[μ] ) :
theorem measure_theory.L1.simple_func.integral_eq_set_to_L1s {α : Type u_1} {E : Type u_2} [normed_group E] {m : measurable_space α} {μ : measure_theory.measure α} [ E] (f : ) :
theorem measure_theory.L1.simple_func.integral_congr {α : Type u_1} {E : Type u_2} [normed_group E] {m : measurable_space α} {μ : measure_theory.measure α} [ E] {f g : }  :
theorem measure_theory.L1.simple_func.integral_add {α : Type u_1} {E : Type u_2} [normed_group E] {m : measurable_space α} {μ : measure_theory.measure α} [ E] (f g : ) :
theorem measure_theory.L1.simple_func.integral_smul {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [normed_group E] {m : measurable_space α} {μ : measure_theory.measure α} [normed_field 𝕜] [ E] [ E] [ E] (c : 𝕜) (f : ) :
theorem measure_theory.L1.simple_func.norm_integral_le_norm {α : Type u_1} {E : Type u_2} [normed_group E] {m : measurable_space α} {μ : measure_theory.measure α} [ E] (f : ) :
noncomputable def measure_theory.L1.simple_func.integral_clm' (α : Type u_1) (E : Type u_2) (𝕜 : Type u_4) [normed_group E] {m : measurable_space α} (μ : measure_theory.measure α) [normed_field 𝕜] [ E] [ E] [ E] :
→L[𝕜] E

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

Equations
noncomputable def measure_theory.L1.simple_func.integral_clm (α : Type u_1) (E : Type u_2) [normed_group E] {m : measurable_space α} (μ : measure_theory.measure α) [ E] :

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

Equations
theorem measure_theory.L1.simple_func.norm_Integral_le_one {α : Type u_1} {E : Type u_2} [normed_group E] {m : measurable_space α} {μ : measure_theory.measure α} [ E] :
noncomputable def measure_theory.L1.integral_clm' {α : Type u_1} {E : Type u_2} (𝕜 : Type u_4) [normed_group E] {m : measurable_space α} {μ : measure_theory.measure α} [ E] [ E] [ E]  :
μ) →L[𝕜] E

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

Equations
• = measure_theory.L1.integral_clm'._proof_2 measure_theory.L1.integral_clm'._proof_3
noncomputable def measure_theory.L1.integral_clm {α : Type u_1} {E : Type u_2} [normed_group E] {m : measurable_space α} {μ : measure_theory.measure α} [ E]  :

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

Equations
noncomputable def measure_theory.L1.integral {α : Type u_1} {E : Type u_2} [normed_group E] {m : measurable_space α} {μ : measure_theory.measure α} [ E] (f : μ)) :
E

The Bochner integral in L1 space

Equations
theorem measure_theory.L1.integral_eq {α : Type u_1} {E : Type u_2} [normed_group E] {m : measurable_space α} {μ : measure_theory.measure α} [ E] (f : μ)) :
theorem measure_theory.L1.integral_eq_set_to_L1 {α : Type u_1} {E : Type u_2} [normed_group E] {m : measurable_space α} {μ : measure_theory.measure α} [ E] (f : μ)) :
@[norm_cast]
theorem measure_theory.L1.simple_func.integral_L1_eq_integral {α : Type u_1} {E : Type u_2} [normed_group E] {m : measurable_space α} {μ : measure_theory.measure α} [ E] (f : ) :
@[simp]
theorem measure_theory.L1.integral_zero (α : Type u_1) (E : Type u_2) [normed_group E] {m : measurable_space α} {μ : measure_theory.measure α} [ E]  :
theorem measure_theory.L1.integral_add {α : Type u_1} {E : Type u_2} [normed_group E] {m : measurable_space α} {μ : measure_theory.measure α} [ E] (f g : μ)) :
theorem measure_theory.L1.integral_neg {α : Type u_1} {E : Type u_2} [normed_group E] {m : measurable_space α} {μ : measure_theory.measure α} [ E] (f : μ)) :
theorem measure_theory.L1.integral_sub {α : Type u_1} {E : Type u_2} [normed_group E] {m : measurable_space α} {μ : measure_theory.measure α} [ E] (f g : μ)) :
theorem measure_theory.L1.integral_smul {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [normed_group E] {m : measurable_space α} {μ : measure_theory.measure α} [ E] [ E] [ E] (c : 𝕜) (f : μ)) :
theorem measure_theory.L1.norm_Integral_le_one {α : Type u_1} {E : Type u_2} [normed_group E] {m : measurable_space α} {μ : measure_theory.measure α} [ E]  :
theorem measure_theory.L1.norm_integral_le {α : Type u_1} {E : Type u_2} [normed_group E] {m : measurable_space α} {μ : measure_theory.measure α} [ E] (f : μ)) :
@[continuity]
theorem measure_theory.L1.continuous_integral {α : Type u_1} {E : Type u_2} [normed_group E] {m : measurable_space α} {μ : measure_theory.measure α} [ E]  :
continuous (λ (f : μ)),

## The Bochner integral on functions #

Define the Bochner integral on functions generally to be the `L1` Bochner integral, for integrable functions, and 0 otherwise; prove its basic properties.

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

The Bochner integral

Equations
• = (λ (hf : , (λ (hf : , 0)

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] {m : measurable_space α} {μ : measure_theory.measure α} (f : α → E) (hf : μ) :
(a : α), f a μ =
theorem measure_theory.integral_eq_set_to_fun {α : Type u_1} {E : Type u_2} [normed_group E] [ E] {m : measurable_space α} {μ : measure_theory.measure α} (f : α → E) :
(a : α), f a μ =
theorem measure_theory.L1.integral_eq_integral {α : Type u_1} {E : Type u_2} [normed_group E] [ E] {m : measurable_space α} {μ : measure_theory.measure α} (f : μ)) :
= (a : α), f a μ
theorem measure_theory.integral_undef {α : Type u_1} {E : Type u_2} [normed_group E] [ E] {f : α → E} {m : measurable_space α} {μ : measure_theory.measure α} (h : ¬) :
(a : α), f a μ = 0
theorem measure_theory.integral_non_ae_strongly_measurable {α : Type u_1} {E : Type u_2} [normed_group E] [ E] {f : α → E} {m : measurable_space α} {μ : measure_theory.measure α}  :
(a : α), f a μ = 0
theorem measure_theory.integral_zero (α : Type u_1) (E : Type u_2) [normed_group E] [ E] {m : measurable_space α} {μ : measure_theory.measure α} :
(a : α), 0 μ = 0
@[simp]
theorem measure_theory.integral_zero' (α : Type u_1) (E : Type u_2) [normed_group E] [ E] {m : measurable_space α} {μ : measure_theory.measure α} :
theorem measure_theory.integral_add {α : Type u_1} {E : Type u_2} [normed_group E] [ E] {f g : α → E} {m : measurable_space α} {μ : 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] {f g : α → E} {m : measurable_space α} {μ : measure_theory.measure α} (hf : μ) (hg : μ) :
(a : α), (f + g) a μ = (a : α), f a μ + (a : α), g a μ
theorem measure_theory.integral_finset_sum {α : Type u_1} {E : Type u_2} [normed_group E] [ E] {m : measurable_space α} {μ : measure_theory.measure α} {ι : Type u_3} (s : finset ι) {f : ι → α → E} (hf : ∀ (i : ι), i s μ) :
(a : α), s.sum (λ (i : ι), f i a) μ = s.sum (λ (i : ι), (a : α), f i a μ)
theorem measure_theory.integral_neg {α : Type u_1} {E : Type u_2} [normed_group E] [ E] {m : measurable_space α} {μ : 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] {m : measurable_space α} {μ : 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] {f g : α → E} {m : measurable_space α} {μ : 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] {f g : α → E} {m : measurable_space α} {μ : 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} {𝕜 : Type u_4} [normed_group E] [ E] [ E] [ E] {m : measurable_space α} {μ : measure_theory.measure α} (c : 𝕜) (f : α → E) :
(a : α), c f a μ = c (a : α), f a μ
theorem measure_theory.integral_mul_left {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (r : ) (f : α → ) :
(a : α), r * f a μ = r * (a : α), f a μ
theorem measure_theory.integral_mul_right {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (r : ) (f : α → ) :
(a : α), f a * r μ = (a : α), f a μ * r
theorem measure_theory.integral_div {α : Type u_1} {m : measurable_space α} {μ : 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] {f g : α → E} {m : measurable_space α} {μ : 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] {m : measurable_space α} {μ : measure_theory.measure α} {f : α → E} (hf : μ) :
(a : α), a μ = (a : α), f a μ
@[continuity]
theorem measure_theory.continuous_integral {α : Type u_1} {E : Type u_2} [normed_group E] [ E] {m : measurable_space α} {μ : measure_theory.measure α} :
continuous (λ (f : μ)), (a : α), f a μ)
theorem measure_theory.norm_integral_le_lintegral_norm {α : Type u_1} {E : Type u_2} [normed_group E] [ E] {m : measurable_space α} {μ : 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] {m : measurable_space α} {μ : measure_theory.measure α} (f : α → E) :
(a : α), f a μ∥₊ ∫⁻ (a : α), f a∥₊ μ
theorem measure_theory.integral_eq_zero_of_ae {α : Type u_1} {E : Type u_2} [normed_group E] [ E] {m : measurable_space α} {μ : 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] {m : measurable_space α} {μ : measure_theory.measure α} {ι : Type u_3} {f : α → E} (hf : μ) {l : filter ι} {s : ι → set α} (hs : filter.tendsto (μ s) l (nhds 0)) :
filter.tendsto (λ (i : ι), (x : α) in s i, f x μ) l (nhds 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] {m : measurable_space α} {μ : measure_theory.measure α} {ι : Type u_3} {f : α → E} (hf : μ) {l : filter ι} {s : ι → set α} (hs : filter.tendsto (μ s) l (nhds 0)) :
filter.tendsto (λ (i : ι), (x : α) in s i, f x μ) l (nhds 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] {m : measurable_space α} {μ : measure_theory.measure α} {ι : Type u_3} (f : α → E) (hfi : μ) {F : ι → α → E} {l : filter ι} (hFi : ∀ᶠ (i : ι) in l, μ) (hF : filter.tendsto (λ (i : ι), ∫⁻ (x : α), F i x - f x∥₊ μ) l (nhds 0)) :
filter.tendsto (λ (i : ι), (x : α), F i x μ) l (nhds ( (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] {m : measurable_space α} {μ : measure_theory.measure α} {F : α → E} {f : α → E} (bound : α → ) (F_measurable : ∀ (n : ), ) (bound_integrable : μ) (h_bound : ∀ (n : ), ∀ᵐ (a : α) ∂μ, F n a bound a) (h_lim : ∀ᵐ (a : α) ∂μ, filter.tendsto (λ (n : ), F n a) filter.at_top (nhds (f a))) :
filter.tendsto (λ (n : ), (a : α), F n a μ) filter.at_top (nhds ( (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. We could weaken the condition `bound_integrable` to require `has_finite_integral bound μ` instead (i.e. not requiring that `bound` is measurable), but in all applications proving integrability is easier.

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

Lebesgue dominated convergence theorem for filters with a countable basis

theorem measure_theory.has_sum_integral_of_dominated_convergence {α : Type u_1} {E : Type u_2} [normed_group E] [ E] {m : measurable_space α} {μ : measure_theory.measure α} {ι : Type u_3} [encodable ι] {F : ι → α → E} {f : α → E} (bound : ι → α → ) (hF_meas : ∀ (n : ι), ) (h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, F n a bound n a) (bound_summable : ∀ᵐ (a : α) ∂μ, summable (λ (n : ι), bound n a)) (bound_integrable : measure_theory.integrable (λ (a : α), ∑' (n : ι), bound n a) μ) (h_lim : ∀ᵐ (a : α) ∂μ, has_sum (λ (n : ι), F n a) (f a)) :
has_sum (λ (n : ι), (a : α), F n a μ) ( (a : α), f a μ)

Lebesgue dominated convergence theorem for series.

theorem measure_theory.continuous_at_of_dominated {α : Type u_1} {E : Type u_2} [normed_group E] [ E] {m : measurable_space α} {μ : measure_theory.measure α} {X : Type u_5} {F : X → α → E} {x₀ : X} {bound : α → } (hF_meas : ∀ᶠ (x : X) in nhds x₀, ) (h_bound : ∀ᶠ (x : X) in nhds x₀, ∀ᵐ (a : α) ∂μ, F x a bound a) (bound_integrable : μ) (h_cont : ∀ᵐ (a : α) ∂μ, continuous_at (λ (x : X), F x a) x₀) :
continuous_at (λ (x : X), (a : α), F x a μ) x₀
theorem measure_theory.continuous_of_dominated {α : Type u_1} {E : Type u_2} [normed_group E] [ E] {m : measurable_space α} {μ : measure_theory.measure α} {X : Type u_5} {F : X → α → E} {bound : α → } (hF_meas : ∀ (x : X), ) (h_bound : ∀ (x : X), ∀ᵐ (a : α) ∂μ, F x a bound a) (bound_integrable : μ) (h_cont : ∀ᵐ (a : α) ∂μ, continuous (λ (x : X), F x a)) :
continuous (λ (x : X), (a : α), F x a μ)
theorem measure_theory.integral_eq_lintegral_pos_part_sub_lintegral_neg_part {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → } (hf : μ) :
(a : α), f a μ = (∫⁻ (a : α), ennreal.of_real (f a) μ).to_real - (∫⁻ (a : α), ennreal.of_real (-f a) μ).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} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → } (hf : 0 ≤ᵐ[μ] f) (hfm : μ) :
(a : α), f a μ = (∫⁻ (a : α), ennreal.of_real (f a) μ).to_real
theorem measure_theory.integral_norm_eq_lintegral_nnnorm {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {G : Type u_2} [normed_group G] {f : α → G}  :
(x : α), f x μ = (∫⁻ (x : α), f x∥₊ μ).to_real
theorem measure_theory.of_real_integral_norm_eq_lintegral_nnnorm {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {G : Type u_2} [normed_group G] {f : α → G} (hf : μ) :
ennreal.of_real ( (x : α), f x μ) = ∫⁻ (x : α), f x∥₊ μ
theorem measure_theory.integral_eq_integral_pos_part_sub_integral_neg_part {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → } (hf : μ) :
(a : α), f a μ = (a : α), ((f a).to_nnreal) μ - (a : α), ((-f a).to_nnreal) μ
theorem measure_theory.integral_nonneg_of_ae {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → } (hf : 0 ≤ᵐ[μ] f) :
0 (a : α), f a μ
theorem measure_theory.lintegral_coe_eq_integral {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} (f : α → nnreal) (hfi : measure_theory.integrable (λ (x : α), (f x)) μ) :
∫⁻ (a : α), (f a) μ = ennreal.of_real ( (a : α), (f a) μ)
theorem measure_theory.of_real_integral_eq_lintegral_of_real {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → } (hfi : μ) (f_nn : 0 ≤ᵐ[μ] f) :
ennreal.of_real ( (x : α), f x μ) = ∫⁻ (x : α), ennreal.of_real (f x) μ
theorem measure_theory.integral_to_real {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → ennreal} (hfm : μ) (hf : ∀ᵐ (x : α) ∂μ, f x < ) :
(a : α), (f a).to_real μ = (∫⁻ (a : α), f a μ).to_real
theorem measure_theory.lintegral_coe_le_coe_iff_integral_le {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → nnreal} (hfi : measure_theory.integrable (λ (x : α), (f x)) μ) {b : nnreal} :
∫⁻ (a : α), (f a) μ b (a : α), (f a) μ b
theorem measure_theory.integral_coe_le_of_lintegral_coe_le {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → nnreal} {b : nnreal} (h : ∫⁻ (a : α), (f a) μ b) :
(a : α), (f a) μ b
theorem measure_theory.integral_nonneg {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → } (hf : 0 f) :
0 (a : α), f a μ
theorem measure_theory.integral_nonpos_of_ae {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → } (hf : f ≤ᵐ[μ] 0) :
(a : α), f a μ 0
theorem measure_theory.integral_nonpos {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → } (hf : f 0) :
(a : α), f a μ 0
theorem measure_theory.integral_eq_zero_iff_of_nonneg_ae {α : Type u_1} {m : measurable_space α} {μ : 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} {m : measurable_space α} {μ : 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} {m : measurable_space α} {μ : 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} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → } (hf : 0 f) (hfi : μ) :
0 < (x : α), f x μ 0 < μ
theorem measure_theory.L1.norm_eq_integral_norm {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {H : Type u_6} [normed_group H] (f : μ)) :
f = (a : α), f a μ
theorem measure_theory.L1.norm_of_fun_eq_integral_norm {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {H : Type u_6} [normed_group H] {f : α → H} (hf : μ) :
= (a : α), f a μ
theorem measure_theory.mem_ℒp.snorm_eq_integral_rpow_norm {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {H : Type u_6} [normed_group H] {f : α → H} {p : ennreal} (hp1 : p 0) (hp2 : p ) (hf : μ) :
μ = ennreal.of_real (( (a : α), f a ^ p.to_real μ) ^ (p.to_real)⁻¹)
theorem measure_theory.integral_mono_ae {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f g : α → } (hf : μ) (hg : μ) (h : f ≤ᵐ[μ] g) :
(a : α), f a μ (a : α), g a μ
theorem measure_theory.integral_mono {α : Type u_1} {m : measurable_space α} {μ : 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} {m : measurable_space α} {μ : measure_theory.measure α} {f g : α → } (hf : 0 ≤ᵐ[μ] f) (hgi : μ) (h : f ≤ᵐ[μ] g) :
(a : α), f a μ (a : α), g a μ
theorem measure_theory.integral_mono_measure {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → } {ν : measure_theory.measure α} (hle : μ ν) (hf : 0 ≤ᵐ[ν] f) (hfi : ν) :
(a : α), f a μ (a : α), f a ν
theorem measure_theory.norm_integral_le_integral_norm {α : Type u_1} {E : Type u_2} [normed_group E] [ E] {m : measurable_space α} {μ : 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] {m : measurable_space α} {μ : measure_theory.measure α} {f : α → E} {g : α → } (hg : μ) (h : ∀ᵐ (x : α) ∂μ, f x g x) :
(x : α), f x μ (x : α), g x μ
theorem measure_theory.simple_func.integral_eq_integral {α : Type u_1} {E : Type u_2} [normed_group E] [ E] {m : measurable_space α} {μ : measure_theory.measure α} (f : E) (hfi : μ) :
= (x : α), f x μ
theorem measure_theory.simple_func.integral_eq_sum {α : Type u_1} {E : Type u_2} [normed_group E] [ E] {m : measurable_space α} {μ : measure_theory.measure α} (f : E) (hfi : μ) :
(x : α), f x μ = f.range.sum (λ (x : E), (μ (f ⁻¹' {x})).to_real x)
@[simp]
theorem measure_theory.integral_const {α : Type u_1} {E : Type u_2} [normed_group E] [ E] {m : measurable_space α} {μ : 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] {m : measurable_space α} {μ : 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_of_measurable {α : Type u_1} {E : Type u_2} [normed_group E] [ E] {m : measurable_space α} {μ : measure_theory.measure α} [borel_space E] {f : α → E} {s : set E} (hfi : μ) (hfm : measurable f) (hs : ∀ᵐ (x : α) ∂μ, f x ) {y₀ : E} (h₀ : y₀ s) (h₀i : measure_theory.integrable (λ (x : α), y₀) μ) :
filter.tendsto (λ (n : ), y₀ h₀ n)) filter.at_top (nhds ( (x : α), f x μ))
theorem measure_theory.tendsto_integral_approx_on_of_measurable_of_range_subset {α : Type u_1} {E : Type u_2} [normed_group E] [ E] {m : measurable_space α} {μ : measure_theory.measure α} [borel_space E] {f : α → E} (fmeas : measurable f) (hf : μ) (s : set E) (hs : {0} s) :
filter.tendsto (λ (n : ), s 0 _ n)) filter.at_top (nhds ( (x : α), f x μ))
theorem measure_theory.integral_add_measure {α : Type u_1} {E : Type u_2} [normed_group E] [ E] {m : measurable_space α} {μ ν : 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] {m : measurable_space α} (f : α → E) :
(x : α), f x 0 = 0
theorem measure_theory.integral_finset_sum_measure {α : Type u_1} {E : Type u_2} [normed_group E] [ E] {ι : Type u_3} {m : measurable_space α} {f : α → E} {μ : ι → } {s : finset ι} (hf : ∀ (i : ι), i s (μ i)) :
(a : α), f a s.sum (λ (i : ι), μ i) = s.sum (λ (i : ι), (a : α), f a μ i)
theorem measure_theory.nndist_integral_add_measure_le_lintegral {α : Type u_1} {E : Type u_2} [normed_group E] [ E] {f : α → E} {m : measurable_space α} {μ ν : measure_theory.measure α} (h₁ : μ) (h₂ : ν) :
(has_nndist.nndist ( (x : α), f x μ) ( (x : α), f x + ν))) ∫⁻ (x : α), f x∥₊ ν
theorem measure_theory.has_sum_integral_measure {α : Type u_1} {E : Type u_2} [normed_group E] [ E] {ι : Type u_3} {m : measurable_space α} {f : α → E} {μ : ι → }  :
has_sum (λ (i : ι), (a : α), f a μ i) ( (a : α), f a
theorem measure_theory.integral_sum_measure {α : Type u_1} {E : Type u_2} [normed_group E] [ E] {ι : Type u_3} {m : measurable_space α} {f : α → E} {μ : ι → }  :
(a : α), f a = ∑' (i : ι), (a : α), f a μ i
@[simp]
theorem measure_theory.integral_smul_measure {α : Type u_1} {E : Type u_2} [normed_group E] [ E] {m : measurable_space α} {μ : measure_theory.measure α} (f : α → E) (c : ennreal) :
(x : α), f x c μ = c.to_real (x : α), f x μ
theorem measure_theory.integral_map_of_strongly_measurable {α : Type u_1} {E : Type u_2} [normed_group E] [ E] {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_3} {φ : α → β} (hφ : measurable φ) {f : β → E}  :
(y : β), f y = (x : α), f (φ x) μ
theorem measure_theory.integral_map {α : Type u_1} {E : Type u_2} [normed_group E] [ E] {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_3} {φ : α → β} (hφ : μ) {f : β → E}  :
(y : β), f y = (x : α), f (φ x) μ
theorem measurable_embedding.integral_map {α : Type u_1} {E : Type u_2} [normed_group E] [ E] {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_3} {_x : measurable_space β} {f : α → β} (hf : measurable_embedding f) (g : β → E) :
(y : β), g y = (x : α), g (f x) μ
theorem closed_embedding.integral_map {α : Type u_1} {E : Type u_2} [normed_group E] [ E] {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_3} [borel_space α] [borel_space β] {φ : α → β} (hφ : closed_embedding φ) (f : β → E) :
(y : β), f y = (x : α), f (φ x) μ
theorem measure_theory.integral_map_equiv {α : Type u_1} {E : Type u_2} [normed_group E] [ E] {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_3} (e : α ≃ᵐ β) (f : β → E) :
(y : β), f y = (x : α), f (e x) μ
theorem measure_theory.measure_preserving.integral_comp {α : Type u_1} {E : Type u_2} [normed_group E] [ E] {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_3} {_x : measurable_space β} {f : α → β} {ν : . "volume_tac"} (h₁ : ν) (h₂ : measurable_embedding f) (g : β → E) :
(x : α), g (f x) μ = (y : β), g y ν
theorem measure_theory.set_integral_eq_subtype {E : Type u_2} [normed_group E] [ E] {α : Type u_1} {s : set α} (hs : measurable_set s) (f : α → E) :
∫ (x : α) in s, f x = ∫ (x : s), f x
@[simp]
theorem measure_theory.integral_dirac' {α : Type u_1} {E : Type u_2} [normed_group E] [ E] (f : α → E) (a : α)  :
(x : α), f x = f a
@[simp]
theorem measure_theory.integral_dirac {α : Type u_1} {E : Type u_2} [normed_group E] [ E] (f : α → E) (a : α) :
(x : α), f x = f a

Simp set for integral rules.

def measure_theory.simple_func.to_larger_space {β : Type u_6} {γ : Type u_7} {m m0 : measurable_space β} (hm : m m0) (f : γ) :

Simple function seen as simple function of a larger `measurable_space`.

Equations
theorem measure_theory.simple_func.coe_to_larger_space_eq {β : Type u_6} {γ : Type u_7} {m m0 : measurable_space β} (hm : m m0) (f : γ) :
theorem measure_theory.integral_simple_func_larger_space {F : Type u_3} [normed_group F] [ F] {β : Type u_6} {m m0 : measurable_space β} {μ : measure_theory.measure β} (hm : m m0) (f : F) (hf_int : μ) :
(x : β), f x μ = f.range.sum (λ (x : F), (μ (f ⁻¹' {x})).to_real x)
theorem measure_theory.integral_trim_simple_func {F : Type u_3} [normed_group F] [ F] {β : Type u_6} {m m0 : measurable_space β} {μ : measure_theory.measure β} (hm : m m0) (f : F) (hf_int : μ) :
(x : β), f x μ = (x : β), f x μ.trim hm
theorem measure_theory.integral_trim {F : Type u_3} [normed_group F] [ F] {β : Type u_6} {m m0 : measurable_space β} {μ : measure_theory.measure β} (hm : m m0) {f : β → F}  :
(x : β), f x μ = (x : β), f x μ.trim hm
theorem measure_theory.integral_trim_ae {F : Type u_3} [normed_group F] [ F] {β : Type u_6} {m m0 : measurable_space β} {μ : measure_theory.measure β} (hm : m m0) {f : β → F} (hf : (μ.trim hm)) :
(x : β), f x μ = (x : β), f x μ.trim hm
theorem measure_theory.ae_eq_trim_of_strongly_measurable {β : Type u_6} {γ : Type u_7} {m m0 : measurable_space β} {μ : measure_theory.measure β} (hm : m m0) {f g : β → γ} (hfg : f =ᵐ[μ] g) :
f =ᵐ[μ.trim hm] g
theorem measure_theory.ae_eq_trim_iff {β : Type u_6} {γ : Type u_7} {m m0 : measurable_space β} {μ : measure_theory.measure β} (hm : m m0) {f g : β → γ}  :
f =ᵐ[μ.trim hm] g f =ᵐ[μ] g
theorem measure_theory.ae_le_trim_of_strongly_measurable {β : Type u_6} {γ : Type u_7} {m m0 : measurable_space β} {μ : measure_theory.measure β} [linear_order γ] (hm : m m0) {f g : β → γ} (hfg : f ≤ᵐ[μ] g) :
f ≤ᵐ[μ.trim hm] g
theorem measure_theory.ae_le_trim_iff {β : Type u_6} {γ : Type u_7} {m m0 : measurable_space β} {μ : measure_theory.measure β} [linear_order γ] (hm : m m0) {f g : β → γ}  :
f ≤ᵐ[μ.trim hm] g f ≤ᵐ[μ] g