# mathlib3documentation

measure_theory.integral.set_integral

# Set integral #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we prove some properties of `∫ x in s, f x ∂μ`. Recall that this notation is defined as `∫ x, f x ∂(μ.restrict s)`. In `integral_indicator` we prove that for a measurable function `f` and a measurable set `s` this definition coincides with another natural definition: `∫ x, indicator s f x ∂μ = ∫ x in s, f x ∂μ`, where `indicator s f x` is equal to `f x` for `x ∈ s` and is zero otherwise.

Since `∫ x in s, f x ∂μ` is a notation, one can rewrite or apply any theorem about `∫ x, f x ∂μ` directly. In this file we prove some theorems about dependence of `∫ x in s, f x ∂μ` on `s`, e.g. `integral_union`, `integral_empty`, `integral_univ`.

We use the property `integrable_on f s μ := integrable f (μ.restrict s)`, defined in `measure_theory.integrable_on`. We also defined in that same file a predicate `integrable_at_filter (f : α → E) (l : filter α) (μ : measure α)` saying that `f` is integrable at some set `s ∈ l`.

Finally, we prove a version of the Fundamental theorem of calculus for set integral, see `filter.tendsto.integral_sub_linear_is_o_ae` and its corollaries. Namely, consider a measurably generated filter `l`, a measure `μ` finite at this filter, and a function `f` that has a finite limit `c` at `l ⊓ μ.ae`. Then `∫ x in s, f x ∂μ = μ s • c + o(μ s)` as `s` tends to `l.small_sets`, i.e. for any `ε>0` there exists `t ∈ l` such that `‖∫ x in s, f x ∂μ - μ s • c‖ ≤ ε * μ s` whenever `s ⊆ t`. We also formulate a version of this theorem for a locally finite measure `μ` and a function `f` continuous at a point `a`.

## Notation #

We provide the following notations for expressing the integral of a function on a set :

• `∫ a in s, f a ∂μ` is `measure_theory.integral (μ.restrict s) f`
• `∫ a in s, f a` is `∫ a in s, f a ∂volume`

Note that the set notations are defined in the file `measure_theory/integral/bochner`, but we reference them here because all theorems about set integrals are in this file.

theorem measure_theory.set_integral_congr_ae₀ {α : Type u_1} {E : Type u_3} {f g : α E} {s : set α} {μ : measure_theory.measure α} [ E] (hs : μ) (h : ∀ᵐ (x : α) μ, x s f x = g x) :
(x : α) in s, f x μ = (x : α) in s, g x μ
theorem measure_theory.set_integral_congr_ae {α : Type u_1} {E : Type u_3} {f g : α E} {s : set α} {μ : measure_theory.measure α} [ E] (hs : measurable_set s) (h : ∀ᵐ (x : α) μ, x s f x = g x) :
(x : α) in s, f x μ = (x : α) in s, g x μ
theorem measure_theory.set_integral_congr₀ {α : Type u_1} {E : Type u_3} {f g : α E} {s : set α} {μ : measure_theory.measure α} [ E] (hs : μ) (h : g s) :
(x : α) in s, f x μ = (x : α) in s, g x μ
theorem measure_theory.set_integral_congr {α : Type u_1} {E : Type u_3} {f g : α E} {s : set α} {μ : measure_theory.measure α} [ E] (hs : measurable_set s) (h : g s) :
(x : α) in s, f x μ = (x : α) in s, g x μ
theorem measure_theory.set_integral_congr_set_ae {α : Type u_1} {E : Type u_3} {f : α E} {s t : set α} {μ : measure_theory.measure α} [ E] (hst : s =ᵐ[μ] t) :
(x : α) in s, f x μ = (x : α) in t, f x μ
theorem measure_theory.integral_union_ae {α : Type u_1} {E : Type u_3} {f : α E} {s t : set α} {μ : measure_theory.measure α} [ E] (hst : t) (ht : μ) (hfs : μ) (hft : μ) :
(x : α) in s t, f x μ = (x : α) in s, f x μ + (x : α) in t, f x μ
theorem measure_theory.integral_union {α : Type u_1} {E : Type u_3} {f : α E} {s t : set α} {μ : measure_theory.measure α} [ E] (hst : t) (ht : measurable_set t) (hfs : μ) (hft : μ) :
(x : α) in s t, f x μ = (x : α) in s, f x μ + (x : α) in t, f x μ
theorem measure_theory.integral_diff {α : Type u_1} {E : Type u_3} {f : α E} {s t : set α} {μ : measure_theory.measure α} [ E] (ht : measurable_set t) (hfs : μ) (hts : t s) :
(x : α) in s \ t, f x μ = (x : α) in s, f x μ - (x : α) in t, f x μ
theorem measure_theory.integral_inter_add_diff₀ {α : Type u_1} {E : Type u_3} {f : α E} {s t : set α} {μ : measure_theory.measure α} [ E] (ht : μ) (hfs : μ) :
(x : α) in s t, f x μ + (x : α) in s \ t, f x μ = (x : α) in s, f x μ
theorem measure_theory.integral_inter_add_diff {α : Type u_1} {E : Type u_3} {f : α E} {s t : set α} {μ : measure_theory.measure α} [ E] (ht : measurable_set t) (hfs : μ) :
(x : α) in s t, f x μ + (x : α) in s \ t, f x μ = (x : α) in s, f x μ
theorem measure_theory.integral_finset_bUnion {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} [ E] {ι : Type u_2} (t : finset ι) {s : ι set α} (hs : (i : ι), i t measurable_set (s i)) (h's : t.pairwise (disjoint on s)) (hf : (i : ι), i t (s i) μ) :
(x : α) in (i : ι) (H : i t), s i, f x μ = t.sum (λ (i : ι), (x : α) in s i, f x μ)
theorem measure_theory.integral_fintype_Union {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} [ E] {ι : Type u_2} [fintype ι] {s : ι set α} (hs : (i : ι), measurable_set (s i)) (h's : pairwise (disjoint on s)) (hf : (i : ι), (s i) μ) :
(x : α) in (i : ι), s i, f x μ = finset.univ.sum (λ (i : ι), (x : α) in s i, f x μ)
theorem measure_theory.integral_empty {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} [ E] :
(x : α) in , f x μ = 0
theorem measure_theory.integral_univ {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} [ E] :
(x : α) in set.univ, f x μ = (x : α), f x μ
theorem measure_theory.integral_add_compl₀ {α : Type u_1} {E : Type u_3} {f : α E} {s : set α} {μ : measure_theory.measure α} [ E] (hs : μ) (hfi : μ) :
(x : α) in s, f x μ + (x : α) in s, f x μ = (x : α), f x μ
theorem measure_theory.integral_add_compl {α : Type u_1} {E : Type u_3} {f : α E} {s : set α} {μ : measure_theory.measure α} [ E] (hs : measurable_set s) (hfi : μ) :
(x : α) in s, f x μ + (x : α) in s, f x μ = (x : α), f x μ
theorem measure_theory.integral_indicator {α : Type u_1} {E : Type u_3} {f : α E} {s : set α} {μ : measure_theory.measure α} [ E] (hs : measurable_set s) :
(x : α), s.indicator f x μ = (x : α) in s, f x μ

For a function `f` and a measurable set `s`, the integral of `indicator s f` over the whole space is equal to `∫ x in s, f x ∂μ` defined as `∫ x, f x ∂(μ.restrict s)`.

theorem measure_theory.set_integral_indicator {α : Type u_1} {E : Type u_3} {f : α E} {s t : set α} {μ : measure_theory.measure α} [ E] (ht : measurable_set t) :
(x : α) in s, t.indicator f x μ = (x : α) in s t, f x μ
theorem measure_theory.of_real_set_integral_one_of_measure_ne_top {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {s : set α} (hs : μ s ) :
ennreal.of_real ( (x : α) in s, 1 μ) = μ s
theorem measure_theory.of_real_set_integral_one {α : Type u_1} {m : measurable_space α} (μ : measure_theory.measure α) (s : set α) :
ennreal.of_real ( (x : α) in s, 1 μ) = μ s
theorem measure_theory.integral_piecewise {α : Type u_1} {E : Type u_3} {f g : α E} {s : set α} {μ : measure_theory.measure α} [ E] [decidable_pred (λ (_x : α), _x s)] (hs : measurable_set s) (hf : μ) (hg : μ) :
(x : α), s.piecewise f g x μ = (x : α) in s, f x μ + (x : α) in s, g x μ
theorem measure_theory.tendsto_set_integral_of_monotone {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} [ E] {ι : Type u_2} [countable ι] {s : ι set α} (hsm : (i : ι), measurable_set (s i)) (h_mono : monotone s) (hfi : ( (n : ι), s n) μ) :
filter.tendsto (λ (i : ι), (a : α) in s i, f a μ) filter.at_top (nhds ( (a : α) in (n : ι), s n, f a μ))
theorem measure_theory.has_sum_integral_Union_ae {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} [ E] {ι : Type u_2} [countable ι] {s : ι set α} (hm : (i : ι), ) (hd : pairwise ) (hfi : ( (i : ι), s i) μ) :
has_sum (λ (n : ι), (a : α) in s n, f a μ) ( (a : α) in (n : ι), s n, f a μ)
theorem measure_theory.has_sum_integral_Union {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} [ E] {ι : Type u_2} [countable ι] {s : ι set α} (hm : (i : ι), measurable_set (s i)) (hd : pairwise (disjoint on s)) (hfi : ( (i : ι), s i) μ) :
has_sum (λ (n : ι), (a : α) in s n, f a μ) ( (a : α) in (n : ι), s n, f a μ)
theorem measure_theory.integral_Union {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} [ E] {ι : Type u_2} [countable ι] {s : ι set α} (hm : (i : ι), measurable_set (s i)) (hd : pairwise (disjoint on s)) (hfi : ( (i : ι), s i) μ) :
(a : α) in (n : ι), s n, f a μ = ∑' (n : ι), (a : α) in s n, f a μ
theorem measure_theory.integral_Union_ae {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} [ E] {ι : Type u_2} [countable ι] {s : ι set α} (hm : (i : ι), ) (hd : pairwise ) (hfi : ( (i : ι), s i) μ) :
(a : α) in (n : ι), s n, f a μ = ∑' (n : ι), (a : α) in s n, f a μ
theorem measure_theory.set_integral_eq_zero_of_ae_eq_zero {α : Type u_1} {E : Type u_3} {f : α E} {t : set α} {μ : measure_theory.measure α} [ E] (ht_eq : ∀ᵐ (x : α) μ, x t f x = 0) :
(x : α) in t, f x μ = 0
theorem measure_theory.set_integral_eq_zero_of_forall_eq_zero {α : Type u_1} {E : Type u_3} {f : α E} {t : set α} {μ : measure_theory.measure α} [ E] (ht_eq : (x : α), x t f x = 0) :
(x : α) in t, f x μ = 0
theorem measure_theory.integral_union_eq_left_of_ae_aux {α : Type u_1} {E : Type u_3} {f : α E} {s t : set α} {μ : measure_theory.measure α} [ E] (ht_eq : ∀ᵐ (x : α) μ.restrict t, f x = 0) (haux : measure_theory.strongly_measurable f) (H : (s t) μ) :
(x : α) in s t, f x μ = (x : α) in s, f x μ
theorem measure_theory.integral_union_eq_left_of_ae {α : Type u_1} {E : Type u_3} {f : α E} {s t : set α} {μ : measure_theory.measure α} [ E] (ht_eq : ∀ᵐ (x : α) μ.restrict t, f x = 0) :
(x : α) in s t, f x μ = (x : α) in s, f x μ
theorem measure_theory.integral_union_eq_left_of_forall₀ {α : Type u_1} {E : Type u_3} {s t : set α} {μ : measure_theory.measure α} [ E] {f : α E} (ht : μ) (ht_eq : (x : α), x t f x = 0) :
(x : α) in s t, f x μ = (x : α) in s, f x μ
theorem measure_theory.integral_union_eq_left_of_forall {α : Type u_1} {E : Type u_3} {s t : set α} {μ : measure_theory.measure α} [ E] {f : α E} (ht : measurable_set t) (ht_eq : (x : α), x t f x = 0) :
(x : α) in s t, f x μ = (x : α) in s, f x μ
theorem measure_theory.set_integral_eq_of_subset_of_ae_diff_eq_zero_aux {α : Type u_1} {E : Type u_3} {f : α E} {s t : set α} {μ : measure_theory.measure α} [ E] (hts : s t) (h't : ∀ᵐ (x : α) μ, x t \ s f x = 0) (haux : measure_theory.strongly_measurable f) (h'aux : μ) :
(x : α) in t, f x μ = (x : α) in s, f x μ
theorem measure_theory.set_integral_eq_of_subset_of_ae_diff_eq_zero {α : Type u_1} {E : Type u_3} {f : α E} {s t : set α} {μ : measure_theory.measure α} [ E] (ht : μ) (hts : s t) (h't : ∀ᵐ (x : α) μ, x t \ s f x = 0) :
(x : α) in t, f x μ = (x : α) in s, f x μ

If a function vanishes almost everywhere on `t \ s` with `s ⊆ t`, then its integrals on `s` and `t` coincide if `t` is null-measurable.

theorem measure_theory.set_integral_eq_of_subset_of_forall_diff_eq_zero {α : Type u_1} {E : Type u_3} {f : α E} {s t : set α} {μ : measure_theory.measure α} [ E] (ht : measurable_set t) (hts : s t) (h't : (x : α), x t \ s f x = 0) :
(x : α) in t, f x μ = (x : α) in s, f x μ

If a function vanishes on `t \ s` with `s ⊆ t`, then its integrals on `s` and `t` coincide if `t` is measurable.

theorem measure_theory.set_integral_eq_integral_of_ae_compl_eq_zero {α : Type u_1} {E : Type u_3} {f : α E} {s : set α} {μ : measure_theory.measure α} [ E] (h : ∀ᵐ (x : α) μ, x s f x = 0) :
(x : α) in s, f x μ = (x : α), f x μ

If a function vanishes almost everywhere on `sᶜ`, then its integral on `s` coincides with its integral on the whole space.

theorem measure_theory.set_integral_eq_integral_of_forall_compl_eq_zero {α : Type u_1} {E : Type u_3} {f : α E} {s : set α} {μ : measure_theory.measure α} [ E] (h : (x : α), x s f x = 0) :
(x : α) in s, f x μ = (x : α), f x μ

If a function vanishes on `sᶜ`, then its integral on `s` coincides with its integral on the whole space.

theorem measure_theory.set_integral_neg_eq_set_integral_nonpos {α : Type u_1} {E : Type u_3} {μ : measure_theory.measure α} [ E] [linear_order E] {f : α E}  :
(x : α) in {x : α | f x < 0}, f x μ = (x : α) in {x : α | f x 0}, f x μ
theorem measure_theory.integral_norm_eq_pos_sub_neg {α : Type u_1} {μ : measure_theory.measure α} {f : α } (hfi : μ) :
(x : α), f x μ = (x : α) in {x : α | 0 f x}, f x μ - (x : α) in {x : α | f x 0}, f x μ
theorem measure_theory.set_integral_const {α : Type u_1} {E : Type u_3} {s : set α} {μ : measure_theory.measure α} [ E] (c : E) :
(x : α) in s, c μ = (μ s).to_real c
@[simp]
theorem measure_theory.integral_indicator_const {α : Type u_1} {E : Type u_3} {μ : measure_theory.measure α} [ E] (e : E) ⦃s : set α⦄ (s_meas : measurable_set s) :
(a : α), s.indicator (λ (x : α), e) a μ = (μ s).to_real e
@[simp]
theorem measure_theory.integral_indicator_one {α : Type u_1} {μ : measure_theory.measure α} ⦃s : set α⦄ (hs : measurable_set s) :
(a : α), s.indicator 1 a μ = (μ s).to_real
theorem measure_theory.set_integral_indicator_const_Lp {α : Type u_1} {E : Type u_3} {s t : set α} {μ : measure_theory.measure α} [ E] {p : ennreal} (hs : measurable_set s) (ht : measurable_set t) (hμt : μ t ) (x : E) :
(a : α) in s, hμt x) a μ = (μ (t s)).to_real x
theorem measure_theory.integral_indicator_const_Lp {α : Type u_1} {E : Type u_3} {t : set α} {μ : measure_theory.measure α} [ E] {p : ennreal} (ht : measurable_set t) (hμt : μ t ) (x : E) :
(a : α), hμt x) a μ = (μ t).to_real x
theorem measure_theory.set_integral_map {α : Type u_1} {E : Type u_3} {μ : measure_theory.measure α} [ E] {β : Type u_2} {g : α β} {f : β E} {s : set β} (hs : measurable_set s) (hg : μ) :
(y : β) in s, f y = (x : α) in g ⁻¹' s, f (g x) μ
theorem measurable_embedding.set_integral_map {α : Type u_1} {E : Type u_3} {μ : measure_theory.measure α} [ E] {β : Type u_2} {_x : measurable_space β} {f : α β} (hf : measurable_embedding f) (g : β E) (s : set β) :
(y : β) in s, g y = (x : α) in f ⁻¹' s, g (f x) μ
theorem closed_embedding.set_integral_map {α : Type u_1} {E : Type u_3} {μ : measure_theory.measure α} [ E] [borel_space α] {β : Type u_2} [borel_space β] {g : α β} {f : β E} (s : set β) (hg : closed_embedding g) :
(y : β) in s, f y = (x : α) in g ⁻¹' s, f (g x) μ
theorem measure_theory.measure_preserving.set_integral_preimage_emb {α : Type u_1} {E : Type u_3} {μ : measure_theory.measure α} [ E] {β : Type u_2} {_x : measurable_space β} {f : α β} {ν : . "volume_tac"} (h₁ : ν) (h₂ : measurable_embedding f) (g : β E) (s : set β) :
(x : α) in f ⁻¹' s, g (f x) μ = (y : β) in s, g y ν
theorem measure_theory.measure_preserving.set_integral_image_emb {α : Type u_1} {E : Type u_3} {μ : measure_theory.measure α} [ E] {β : Type u_2} {_x : measurable_space β} {f : α β} {ν : . "volume_tac"} (h₁ : ν) (h₂ : measurable_embedding f) (g : β E) (s : set α) :
(y : β) in f '' s, g y ν = (x : α) in s, g (f x) μ
theorem measure_theory.set_integral_map_equiv {α : Type u_1} {E : Type u_3} {μ : measure_theory.measure α} [ E] {β : Type u_2} (e : α ≃ᵐ β) (f : β E) (s : set β) :
(y : β) in s, f y = (x : α) in e ⁻¹' s, f (e x) μ
theorem measure_theory.norm_set_integral_le_of_norm_le_const_ae {α : Type u_1} {E : Type u_3} {f : α E} {s : set α} {μ : measure_theory.measure α} [ E] {C : } (hs : μ s < ) (hC : ∀ᵐ (x : α) μ.restrict s, f x C) :
(x : α) in s, f x μ C * (μ s).to_real
theorem measure_theory.norm_set_integral_le_of_norm_le_const_ae' {α : Type u_1} {E : Type u_3} {f : α E} {s : set α} {μ : measure_theory.measure α} [ E] {C : } (hs : μ s < ) (hC : ∀ᵐ (x : α) μ, x s f x C) (hfm : (μ.restrict s)) :
(x : α) in s, f x μ C * (μ s).to_real
theorem measure_theory.norm_set_integral_le_of_norm_le_const_ae'' {α : Type u_1} {E : Type u_3} {f : α E} {s : set α} {μ : measure_theory.measure α} [ E] {C : } (hs : μ s < ) (hsm : measurable_set s) (hC : ∀ᵐ (x : α) μ, x s f x C) :
(x : α) in s, f x μ C * (μ s).to_real
theorem measure_theory.norm_set_integral_le_of_norm_le_const {α : Type u_1} {E : Type u_3} {f : α E} {s : set α} {μ : measure_theory.measure α} [ E] {C : } (hs : μ s < ) (hC : (x : α), x s f x C) (hfm : (μ.restrict s)) :
(x : α) in s, f x μ C * (μ s).to_real
theorem measure_theory.norm_set_integral_le_of_norm_le_const' {α : Type u_1} {E : Type u_3} {f : α E} {s : set α} {μ : measure_theory.measure α} [ E] {C : } (hs : μ s < ) (hsm : measurable_set s) (hC : (x : α), x s f x C) :
(x : α) in s, f x μ C * (μ s).to_real
theorem measure_theory.set_integral_eq_zero_iff_of_nonneg_ae {α : Type u_1} {s : set α} {μ : measure_theory.measure α} {f : α } (hf : 0 ≤ᵐ[μ.restrict s] f) (hfi : μ) :
(x : α) in s, f x μ = 0 f =ᵐ[μ.restrict s] 0
theorem measure_theory.set_integral_pos_iff_support_of_nonneg_ae {α : Type u_1} {s : set α} {μ : measure_theory.measure α} {f : α } (hf : 0 ≤ᵐ[μ.restrict s] f) (hfi : μ) :
0 < (x : α) in s, f x μ 0 < μ s)
theorem measure_theory.set_integral_gt_gt {α : Type u_1} {μ : measure_theory.measure α} {R : } {f : α } (hR : 0 R) (hfm : measurable f) (hfint : {x : α | R < f x} μ) (hμ : μ {x : α | R < f x} 0) :
(μ {x : α | R < f x}).to_real * R < (x : α) in {x : α | R < f x}, f x μ
theorem measure_theory.set_integral_trim {E : Type u_3} [ E] {α : Type u_1} {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) {f : α E} (hf_meas : measure_theory.strongly_measurable f) {s : set α} (hs : measurable_set s) :
(x : α) in s, f x μ = (x : α) in s, f x μ.trim hm

### Lemmas about adding and removing interval boundaries #

The primed lemmas take explicit arguments about the endpoint having zero measure, while the unprimed ones use `[has_no_atoms μ]`.

theorem measure_theory.integral_Icc_eq_integral_Ioc' {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} [ E] {a b : α} (ha : μ {a} = 0) :
(t : α) in b, f t μ = (t : α) in b, f t μ
theorem measure_theory.integral_Icc_eq_integral_Ico' {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} [ E] {a b : α} (hb : μ {b} = 0) :
(t : α) in b, f t μ = (t : α) in b, f t μ
theorem measure_theory.integral_Ioc_eq_integral_Ioo' {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} [ E] {a b : α} (hb : μ {b} = 0) :
(t : α) in b, f t μ = (t : α) in b, f t μ
theorem measure_theory.integral_Ico_eq_integral_Ioo' {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} [ E] {a b : α} (ha : μ {a} = 0) :
(t : α) in b, f t μ = (t : α) in b, f t μ
theorem measure_theory.integral_Icc_eq_integral_Ioo' {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} [ E] {a b : α} (ha : μ {a} = 0) (hb : μ {b} = 0) :
(t : α) in b, f t μ = (t : α) in b, f t μ
theorem measure_theory.integral_Iic_eq_integral_Iio' {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} [ E] {a : α} (ha : μ {a} = 0) :
(t : α) in , f t μ = (t : α) in , f t μ
theorem measure_theory.integral_Ici_eq_integral_Ioi' {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} [ E] {a : α} (ha : μ {a} = 0) :
(t : α) in , f t μ = (t : α) in , f t μ
theorem measure_theory.integral_Icc_eq_integral_Ioc {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} [ E] {a b : α}  :
(t : α) in b, f t μ = (t : α) in b, f t μ
theorem measure_theory.integral_Icc_eq_integral_Ico {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} [ E] {a b : α}  :
(t : α) in b, f t μ = (t : α) in b, f t μ
theorem measure_theory.integral_Ioc_eq_integral_Ioo {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} [ E] {a b : α}  :
(t : α) in b, f t μ = (t : α) in b, f t μ
theorem measure_theory.integral_Ico_eq_integral_Ioo {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} [ E] {a b : α}  :
(t : α) in b, f t μ = (t : α) in b, f t μ
theorem measure_theory.integral_Icc_eq_integral_Ioo {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} [ E] {a b : α}  :
(t : α) in b, f t μ = (t : α) in b, f t μ
theorem measure_theory.integral_Iic_eq_integral_Iio {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} [ E] {a : α}  :
(t : α) in , f t μ = (t : α) in , f t μ
theorem measure_theory.integral_Ici_eq_integral_Ioi {α : Type u_1} {E : Type u_3} {f : α E} {μ : measure_theory.measure α} [ E] {a : α}  :
(t : α) in , f t μ = (t : α) in , f t μ
theorem measure_theory.set_integral_mono_ae_restrict {α : Type u_1} {μ : measure_theory.measure α} {f g : α } {s : set α} (hf : μ) (hg : μ) (h : f ≤ᵐ[μ.restrict s] g) :
(a : α) in s, f a μ (a : α) in s, g a μ
theorem measure_theory.set_integral_mono_ae {α : Type u_1} {μ : measure_theory.measure α} {f g : α } {s : set α} (hf : μ) (hg : μ) (h : f ≤ᵐ[μ] g) :
(a : α) in s, f a μ (a : α) in s, g a μ
theorem measure_theory.set_integral_mono_on {α : Type u_1} {μ : measure_theory.measure α} {f g : α } {s : set α} (hf : μ) (hg : μ) (hs : measurable_set s) (h : (x : α), x s f x g x) :
(a : α) in s, f a μ (a : α) in s, g a μ
theorem measure_theory.set_integral_mono_on_ae {α : Type u_1} {μ : measure_theory.measure α} {f g : α } {s : set α} (hf : μ) (hg : μ) (hs : measurable_set s) (h : ∀ᵐ (x : α) μ, x s f x g x) :
(a : α) in s, f a μ (a : α) in s, g a μ
theorem measure_theory.set_integral_mono {α : Type u_1} {μ : measure_theory.measure α} {f g : α } {s : set α} (hf : μ) (hg : μ) (h : f g) :
(a : α) in s, f a μ (a : α) in s, g a μ
theorem measure_theory.set_integral_mono_set {α : Type u_1} {μ : measure_theory.measure α} {f : α } {s t : set α} (hfi : μ) (hf : 0 ≤ᵐ[μ.restrict t] f) (hst : s ≤ᵐ[μ] t) :
(x : α) in s, f x μ (x : α) in t, f x μ
theorem measure_theory.set_integral_ge_of_const_le {α : Type u_1} {μ : measure_theory.measure α} {f : α } {s : set α} {c : } (hs : measurable_set s) (hμs : μ s ) (hf : (x : α), x s c f x) (hfint : measure_theory.integrable_on (λ (x : α), f x) s μ) :
c * (μ s).to_real (x : α) in s, f x μ
theorem measure_theory.set_integral_nonneg_of_ae_restrict {α : Type u_1} {μ : measure_theory.measure α} {f : α } {s : set α} (hf : 0 ≤ᵐ[μ.restrict s] f) :
0 (a : α) in s, f a μ
theorem measure_theory.set_integral_nonneg_of_ae {α : Type u_1} {μ : measure_theory.measure α} {f : α } {s : set α} (hf : 0 ≤ᵐ[μ] f) :
0 (a : α) in s, f a μ
theorem measure_theory.set_integral_nonneg {α : Type u_1} {μ : measure_theory.measure α} {f : α } {s : set α} (hs : measurable_set s) (hf : (a : α), a s 0 f a) :
0 (a : α) in s, f a μ
theorem measure_theory.set_integral_nonneg_ae {α : Type u_1} {μ : measure_theory.measure α} {f : α } {s : set α} (hs : measurable_set s) (hf : ∀ᵐ (a : α) μ, a s 0 f a) :
0 (a : α) in s, f a μ
theorem measure_theory.set_integral_le_nonneg {α : Type u_1} {μ : measure_theory.measure α} {f : α } {s : set α} (hs : measurable_set s) (hfi : μ) :
(x : α) in s, f x μ (x : α) in {y : α | 0 f y}, f x μ
theorem measure_theory.set_integral_nonpos_of_ae_restrict {α : Type u_1} {μ : measure_theory.measure α} {f : α } {s : set α} (hf : f ≤ᵐ[μ.restrict s] 0) :
(a : α) in s, f a μ 0
theorem measure_theory.set_integral_nonpos_of_ae {α : Type u_1} {μ : measure_theory.measure α} {f : α } {s : set α} (hf : f ≤ᵐ[μ] 0) :
(a : α) in s, f a μ 0
theorem measure_theory.set_integral_nonpos {α : Type u_1} {μ : measure_theory.measure α} {f : α } {s : set α} (hs : measurable_set s) (hf : (a : α), a s f a 0) :
(a : α) in s, f a μ 0
theorem measure_theory.set_integral_nonpos_ae {α : Type u_1} {μ : measure_theory.measure α} {f : α } {s : set α} (hs : measurable_set s) (hf : ∀ᵐ (a : α) μ, a s f a 0) :
(a : α) in s, f a μ 0
theorem measure_theory.set_integral_nonpos_le {α : Type u_1} {μ : measure_theory.measure α} {f : α } {s : set α} (hs : measurable_set s) (hfi : μ) :
(x : α) in {y : α | f y 0}, f x μ (x : α) in s, f x μ
theorem measure_theory.integrable_on_Union_of_summable_integral_norm {α : Type u_1} {β : Type u_2} {E : Type u_3} {μ : measure_theory.measure α} [countable β] {f : α E} {s : β set α} (hs : (b : β), measurable_set (s b)) (hi : (b : β), (s b) μ) (h : summable (λ (b : β), (a : α) in s b, f a μ)) :
theorem measure_theory.integrable_on_Union_of_summable_norm_restrict {α : Type u_1} {β : Type u_2} {E : Type u_3} {μ : measure_theory.measure α} [countable β] [borel_space α] {f : C(α, E)} {s : β } (hf : summable (λ (i : β), f * (μ (s i)).to_real)) :
( (i : β), (s i)) μ

If `s` is a countable family of compact sets, `f` is a continuous function, and the sequence `‖f.restrict (s i)‖ * μ (s i)` is summable, then `f` is integrable on the union of the `s i`.

theorem measure_theory.integrable_of_summable_norm_restrict {α : Type u_1} {β : Type u_2} {E : Type u_3} {μ : measure_theory.measure α} [countable β] [borel_space α] {f : C(α, E)} {s : β } (hf : summable (λ (i : β), f * (μ (s i)).to_real)) (hs : ( (i : β), (s i)) = set.univ) :

If `s` is a countable family of compact sets covering `α`, `f` is a continuous function, and the sequence `‖f.restrict (s i)‖ * μ (s i)` is summable, then `f` is integrable.

theorem antitone.tendsto_set_integral {α : Type u_1} {E : Type u_3} {μ : measure_theory.measure α} [ E] {s : set α} {f : α E} (hsm : (i : ), measurable_set (s i)) (h_anti : antitone s) (hfi : (s 0) μ) :
filter.tendsto (λ (i : ), (a : α) in s i, f a μ) filter.at_top (nhds ( (a : α) in (n : ), s n, f a μ))

### Continuity of the set integral #

We prove that for any set `s`, the function `λ f : α →₁[μ] E, ∫ x in s, f x ∂μ` is continuous.

theorem measure_theory.Lp_to_Lp_restrict_add {α : Type u_1} {E : Type u_3} {p : ennreal} {μ : measure_theory.measure α} (f g : μ)) (s : set α) :

For `f : Lp E p μ`, we can define an element of `Lp E p (μ.restrict s)` by `(Lp.mem_ℒp f).restrict s).to_Lp f`. This map is additive.

theorem measure_theory.Lp_to_Lp_restrict_smul {α : Type u_1} {F : Type u_4} {𝕜 : Type u_5} [normed_field 𝕜] [ F] {p : ennreal} {μ : measure_theory.measure α} (c : 𝕜) (f : μ)) (s : set α) :
_ =

For `f : Lp E p μ`, we can define an element of `Lp E p (μ.restrict s)` by `(Lp.mem_ℒp f).restrict s).to_Lp f`. This map commutes with scalar multiplication.

theorem measure_theory.norm_Lp_to_Lp_restrict_le {α : Type u_1} {E : Type u_3} {p : ennreal} {μ : measure_theory.measure α} (s : set α) (f : μ)) :

For `f : Lp E p μ`, we can define an element of `Lp E p (μ.restrict s)` by `(Lp.mem_ℒp f).restrict s).to_Lp f`. This map is non-expansive.

noncomputable def measure_theory.Lp_to_Lp_restrict_clm (α : Type u_1) (F : Type u_4) (𝕜 : Type u_5) [normed_field 𝕜] [ F] (μ : measure_theory.measure α) (p : ennreal) [hp : fact (1 p)] (s : set α) :
μ) →L[𝕜] (μ.restrict s))

Continuous linear map sending a function of `Lp F p μ` to the same function in `Lp F p (μ.restrict s)`.

Equations
theorem measure_theory.Lp_to_Lp_restrict_clm_coe_fn {α : Type u_1} {F : Type u_4} (𝕜 : Type u_5) [normed_field 𝕜] [ F] {p : ennreal} {μ : measure_theory.measure α} [hp : fact (1 p)] (s : set α) (f : μ)) :
( p s) f) =ᵐ[μ.restrict s] f
@[continuity]
theorem measure_theory.continuous_set_integral {α : Type u_1} {E : Type u_3} {μ : measure_theory.measure α} [ E] (s : set α) :
continuous (λ (f : μ)), (x : α) in s, f x μ)
theorem filter.tendsto.integral_sub_linear_is_o_ae {α : Type u_1} {E : Type u_3} {ι : Type u_5} [ E] {μ : measure_theory.measure α} {l : filter α} {f : α E} {b : E} (h : (l μ.ae) (nhds b)) (hfm : μ) (hμ : μ.finite_at_filter l) {s : ι set α} {li : filter ι} (hs : li l.small_sets) (m : ι := λ (i : ι), (μ (s i)).to_real) (hsμ : (λ (i : ι), (μ (s i)).to_real) =ᶠ[li] m . "refl") :
(λ (i : ι), (x : α) in s i, f x μ - m i b) =o[li] m

Fundamental theorem of calculus for set integrals: if `μ` is a measure that is finite at a filter `l` and `f` is a measurable function that has a finite limit `b` at `l ⊓ μ.ae`, then `∫ x in s i, f x ∂μ = μ (s i) • b + o(μ (s i))` at a filter `li` provided that `s i` tends to `l.small_sets` along `li`. Since `μ (s i)` is an `ℝ≥0∞` number, we use `(μ (s i)).to_real` in the actual statement.

Often there is a good formula for `(μ (s i)).to_real`, so the formalization can take an optional argument `m` with this formula and a proof `of`(λ i, (μ (s i)).to_real) =ᶠ[li] m`. Without these arguments,`m i = (μ (s i)).to_real` is used in the output.

theorem continuous_within_at.integral_sub_linear_is_o_ae {α : Type u_1} {E : Type u_3} {ι : Type u_5} [ E] {μ : measure_theory.measure α} {a : α} {t : set α} {f : α E} (ha : a) (ht : measurable_set t) (hfm : μ) {s : ι set α} {li : filter ι} (hs : li t).small_sets) (m : ι := λ (i : ι), (μ (s i)).to_real) (hsμ : (λ (i : ι), (μ (s i)).to_real) =ᶠ[li] m . "refl") :
(λ (i : ι), (x : α) in s i, f x μ - m i f a) =o[li] m

Fundamental theorem of calculus for set integrals, `nhds_within` version: if `μ` is a locally finite measure and `f` is an almost everywhere measurable function that is continuous at a point `a` within a measurable set `t`, then `∫ x in s i, f x ∂μ = μ (s i) • f a + o(μ (s i))` at a filter `li` provided that `s i` tends to `(𝓝[t] a).small_sets` along `li`. Since `μ (s i)` is an `ℝ≥0∞` number, we use `(μ (s i)).to_real` in the actual statement.

Often there is a good formula for `(μ (s i)).to_real`, so the formalization can take an optional argument `m` with this formula and a proof `of`(λ i, (μ (s i)).to_real) =ᶠ[li] m`. Without these arguments,`m i = (μ (s i)).to_real` is used in the output.

theorem continuous_at.integral_sub_linear_is_o_ae {α : Type u_1} {E : Type u_3} {ι : Type u_5} [ E] {μ : measure_theory.measure α} {a : α} {f : α E} (ha : a) (hfm : μ) {s : ι set α} {li : filter ι} (hs : li (nhds a).small_sets) (m : ι := λ (i : ι), (μ (s i)).to_real) (hsμ : (λ (i : ι), (μ (s i)).to_real) =ᶠ[li] m . "refl") :
(λ (i : ι), (x : α) in s i, f x μ - m i f a) =o[li] m

Fundamental theorem of calculus for set integrals, `nhds` version: if `μ` is a locally finite measure and `f` is an almost everywhere measurable function that is continuous at a point `a`, then `∫ x in s i, f x ∂μ = μ (s i) • f a + o(μ (s i))` at `li` provided that `s` tends to `(𝓝 a).small_sets` along `li. Since`μ (s i)`is an`ℝ≥0∞`number, we use`(μ (s i)).to_real` in the actual statement.

Often there is a good formula for `(μ (s i)).to_real`, so the formalization can take an optional argument `m` with this formula and a proof `of`(λ i, (μ (s i)).to_real) =ᶠ[li] m`. Without these arguments,`m i = (μ (s i)).to_real` is used in the output.

theorem continuous_on.integral_sub_linear_is_o_ae {α : Type u_1} {E : Type u_3} {ι : Type u_5} [ E] {μ : measure_theory.measure α} {a : α} {t : set α} {f : α E} (hft : t) (ha : a t) (ht : measurable_set t) {s : ι set α} {li : filter ι} (hs : li t).small_sets) (m : ι := λ (i : ι), (μ (s i)).to_real) (hsμ : (λ (i : ι), (μ (s i)).to_real) =ᶠ[li] m . "refl") :
(λ (i : ι), (x : α) in s i, f x μ - m i f a) =o[li] m

Fundamental theorem of calculus for set integrals, `nhds_within` version: if `μ` is a locally finite measure, `f` is continuous on a measurable set `t`, and `a ∈ t`, then `∫ x in (s i), f x ∂μ = μ (s i) • f a + o(μ (s i))` at `li` provided that `s i` tends to `(𝓝[t] a).small_sets` along `li`. Since `μ (s i)` is an `ℝ≥0∞` number, we use `(μ (s i)).to_real` in the actual statement.

Often there is a good formula for `(μ (s i)).to_real`, so the formalization can take an optional argument `m` with this formula and a proof `of`(λ i, (μ (s i)).to_real) =ᶠ[li] m`. Without these arguments,`m i = (μ (s i)).to_real` is used in the output.

### Continuous linear maps composed with integration #

The goal of this section is to prove that integration commutes with continuous linear maps. This holds for simple functions. The general result follows from the continuity of all involved operations on the space `L¹`. Note that composition by a continuous linear map on `L¹` is not just the composition, as we are dealing with classes of functions, but it has already been defined as `continuous_linear_map.comp_Lp`. We take advantage of this construction here.

theorem continuous_linear_map.integral_comp_Lp {α : Type u_1} {E : Type u_3} {F : Type u_4} {μ : measure_theory.measure α} {𝕜 : Type u_6} [is_R_or_C 𝕜] [ E] [ F] {p : ennreal} [ F] (L : E →L[𝕜] F) (φ : μ)) :
(a : α), (L.comp_Lp φ) a μ = (a : α), L (φ a) μ
theorem continuous_linear_map.set_integral_comp_Lp {α : Type u_1} {E : Type u_3} {F : Type u_4} {μ : measure_theory.measure α} {𝕜 : Type u_6} [is_R_or_C 𝕜] [ E] [ F] {p : ennreal} [ F] (L : E →L[𝕜] F) (φ : μ)) {s : set α} (hs : measurable_set s) :
(a : α) in s, (L.comp_Lp φ) a μ = (a : α) in s, L (φ a) μ
theorem continuous_linear_map.continuous_integral_comp_L1 {α : Type u_1} {E : Type u_3} {F : Type u_4} {μ : measure_theory.measure α} {𝕜 : Type u_6} [is_R_or_C 𝕜] [ E] [ F] [ F] (L : E →L[𝕜] F) :
continuous (λ (φ : μ)), (a : α), L (φ a) μ)
theorem continuous_linear_map.integral_comp_comm {α : Type u_1} {E : Type u_3} {F : Type u_4} {μ : measure_theory.measure α} {𝕜 : Type u_6} [is_R_or_C 𝕜] [ E] [ F] [ F] [ E] (L : E →L[𝕜] F) {φ : α E} (φ_int : μ) :
(a : α), L (φ a) μ = L ( (a : α), φ a μ)
theorem continuous_linear_map.integral_apply {α : Type u_1} {E : Type u_3} {μ : measure_theory.measure α} {𝕜 : Type u_6} [is_R_or_C 𝕜] [ E] [ E] {H : Type u_2} [ H] {φ : α (H →L[𝕜] E)} (φ_int : μ) (v : H) :
( (a : α), φ a μ) v = (a : α), (φ a) v μ
theorem continuous_linear_map.integral_comp_comm' {α : Type u_1} {E : Type u_3} {F : Type u_4} {μ : measure_theory.measure α} {𝕜 : Type u_6} [is_R_or_C 𝕜] [ E] [ F] [ F] [ E] (L : E →L[𝕜] F) {K : nnreal} (hL : L) (φ : α E) :
(a : α), L (φ a) μ = L ( (a : α), φ a μ)
theorem continuous_linear_map.integral_comp_L1_comm {α : Type u_1} {E : Type u_3} {F : Type u_4} {μ : measure_theory.measure α} {𝕜 : Type u_6} [is_R_or_C 𝕜] [ E] [ F] [ F] [ E] (L : E →L[𝕜] F) (φ : μ)) :
(a : α), L (φ a) μ = L ( (a : α), φ a μ)
theorem linear_isometry.integral_comp_comm {α : Type u_1} {E : Type u_3} {F : Type u_4} {μ : measure_theory.measure α} {𝕜 : Type u_6} [is_R_or_C 𝕜] [ E] [ F] [ F] [ E] (L : E →ₗᵢ[𝕜] F) (φ : α E) :
(a : α), L (φ a) μ = L ( (a : α), φ a μ)
theorem continuous_linear_equiv.integral_comp_comm {α : Type u_1} {E : Type u_3} {F : Type u_4} {μ : measure_theory.measure α} {𝕜 : Type u_6} [is_R_or_C 𝕜] [ E] [ F] [ F] [ E] (L : E ≃L[𝕜] F) (φ : α E) :
(a : α), L (φ a) μ = L ( (a : α), φ a μ)
@[norm_cast]
theorem integral_of_real {α : Type u_1} {μ : measure_theory.measure α} {𝕜 : Type u_6} [is_R_or_C 𝕜] {f : α } :
(a : α), (f a) μ = (a : α), f a μ
theorem integral_re {α : Type u_1} {μ : measure_theory.measure α} {𝕜 : Type u_6} [is_R_or_C 𝕜] {f : α 𝕜} (hf : μ) :
(a : α), is_R_or_C.re (f a) μ = is_R_or_C.re ( (a : α), f a μ)
theorem integral_im {α : Type u_1} {μ : measure_theory.measure α} {𝕜 : Type u_6} [is_R_or_C 𝕜] {f : α 𝕜} (hf : μ) :
(a : α), is_R_or_C.im (f a) μ = is_R_or_C.im ( (a : α), f a μ)
theorem integral_conj {α : Type u_1} {μ : measure_theory.measure α} {𝕜 : Type u_6} [is_R_or_C 𝕜] {f : α 𝕜} :
(a : α), (f a) μ = ( (a : α), f a μ)
theorem integral_coe_re_add_coe_im {α : Type u_1} {μ : measure_theory.measure α} {𝕜 : Type u_6} [is_R_or_C 𝕜] {f : α 𝕜} (hf : μ) :
(x : α), (is_R_or_C.re (f x)) μ + (x : α), (is_R_or_C.im (f x)) μ * is_R_or_C.I = (x : α), f x μ
theorem integral_re_add_im {α : Type u_1} {μ : measure_theory.measure α} {𝕜 : Type u_6} [is_R_or_C 𝕜] {f : α 𝕜} (hf : μ) :
(x : α), is_R_or_C.re (f x) μ + (x : α), is_R_or_C.im (f x) μ * is_R_or_C.I = (x : α), f x μ
theorem set_integral_re_add_im {α : Type u_1} {μ : measure_theory.measure α} {𝕜 : Type u_6} [is_R_or_C 𝕜] {f : α 𝕜} {i : set α} (hf : μ) :
(x : α) in i, is_R_or_C.re (f x) μ + (x : α) in i, is_R_or_C.im (f x) μ * is_R_or_C.I = (x : α) in i, f x μ
theorem fst_integral {α : Type u_1} {E : Type u_3} {F : Type u_4} {μ : measure_theory.measure α} [ E] [ F] {f : α E × F} (hf : μ) :
( (x : α), f x μ).fst = (x : α), (f x).fst μ
theorem snd_integral {α : Type u_1} {E : Type u_3} {F : Type u_4} {μ : measure_theory.measure α} [ E] [ F] {f : α E × F} (hf : μ) :
( (x : α), f x μ).snd = (x : α), (f x).snd μ
theorem integral_pair {α : Type u_1} {E : Type u_3} {F : Type u_4} {μ : measure_theory.measure α} [ E] [ F] {f : α E} {g : α F} (hf : μ) (hg : μ) :
(x : α), (f x, g x) μ = ( (x : α), f x μ, (x : α), g x μ)
theorem integral_smul_const {α : Type u_1} {E : Type u_3} {μ : measure_theory.measure α} [ E] {𝕜 : Type u_2} [is_R_or_C 𝕜] [ E] (f : α 𝕜) (c : E) :
(x : α), f x c μ = ( (x : α), f x μ) c
theorem integral_with_density_eq_integral_smul {α : Type u_1} {E : Type u_3} {μ : measure_theory.measure α} [ E] {f : α nnreal} (f_meas : measurable f) (g : α E) :
(a : α), g a μ.with_density (λ (x : α), (f x)) = (a : α), f a g a μ
theorem integral_with_density_eq_integral_smul₀ {α : Type u_1} {E : Type u_3} {μ : measure_theory.measure α} [ E] {f : α nnreal} (hf : μ) (g : α E) :
(a : α), g a μ.with_density (λ (x : α), (f x)) = (a : α), f a g a μ
theorem set_integral_with_density_eq_set_integral_smul {α : Type u_1} {E : Type u_3} {μ : measure_theory.measure α} [ E] {f : α nnreal} (f_meas : measurable f) (g : α E) {s : set α} (hs : measurable_set s) :
(a : α) in s, g a μ.with_density (λ (x : α), (f x)) = (a : α) in s, f a g a μ
theorem set_integral_with_density_eq_set_integral_smul₀ {α : Type u_1} {E : Type u_3} {μ : measure_theory.measure α} [ E] {f : α nnreal} {s : set α} (hf : (μ.restrict s)) (g : α E) (hs : measurable_set s) :
(a : α) in s, g a μ.with_density (λ (x : α), (f x)) = (a : α) in s, f a g a μ
theorem measure_le_lintegral_thickened_indicator_aux {α : Type u_1} (μ : measure_theory.measure α) {E : set α} (E_mble : measurable_set E) (δ : ) :
μ E ∫⁻ (a : α), μ
theorem measure_le_lintegral_thickened_indicator {α : Type u_1} (μ : measure_theory.measure α) {E : set α} (E_mble : measurable_set E) {δ : } (δ_pos : 0 < δ) :
μ E ∫⁻ (a : α), ((thickened_indicator δ_pos E) a) μ
theorem measure_theory.integrable.simple_func_mul {β : Type u_2} {f : β } {m0 : measurable_space β} {μ : measure_theory.measure β} (g : ) (hf : μ) :
μ
theorem measure_theory.integrable.simple_func_mul' {β : Type u_2} {f : β } {m m0 : measurable_space β} {μ : measure_theory.measure β} (hm : m m0) (g : ) (hf : μ) :
μ