# Set integral #

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. `setIntegral_union`, `setIntegral_empty`, `setIntegral_univ`.

We use the property `IntegrableOn f s μ := Integrable f (μ.restrict s)`, defined in `MeasureTheory.IntegrableOn`. We also defined in that same file a predicate `IntegrableAtFilter (f : X → E) (l : Filter X) (μ : Measure X)` saying that `f` is integrable at some set `s ∈ l`.

## Notation #

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

- `∫ x in s, f x ∂μ` is `MeasureTheory.integral (μ.restrict s) f`
- `∫ x in s, f x` is `∫ x in s, f x ∂volume`

Note that the set notations are defined in the file `Mathlib/MeasureTheory/Integral/Bochner/Basic.lean`, but we reference them here because all theorems about set integrals are in this file.

source
theorem MeasureTheory.setIntegral_congr_ae₀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : X → E} {s : Set X} {μ : Measure X} (hs : NullMeasurableSet s μ) (h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x = g x) :
∫ (x : X) in s, f x ∂μ = ∫ (x : X) in s, g x ∂μ
source
theorem MeasureTheory.setIntegral_congr_ae {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : X → E} {s : Set X} {μ : Measure X} (hs : MeasurableSet s) (h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x = g x) :
∫ (x : X) in s, f x ∂μ = ∫ (x : X) in s, g x ∂μ
source
theorem MeasureTheory.setIntegral_congr_fun₀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : X → E} {s : Set X} {μ : Measure X} (hs : NullMeasurableSet s μ) (h : Set.EqOn f g s) :
∫ (x : X) in s, f x ∂μ = ∫ (x : X) in s, g x ∂μ
source
theorem MeasureTheory.setIntegral_congr_fun {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : X → E} {s : Set X} {μ : Measure X} (hs : MeasurableSet s) (h : Set.EqOn f g s) :
∫ (x : X) in s, f x ∂μ = ∫ (x : X) in s, g x ∂μ
source
theorem MeasureTheory.setIntegral_congr_set {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {s t : Set X} {μ : Measure X} (hst : s =ᶠ[ae μ] t) :
∫ (x : X) in s, f x ∂μ = ∫ (x : X) in t, f x ∂μ
source
theorem MeasureTheory.integral_union_ae {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {s t : Set X} {μ : Measure X} (hst : AEDisjoint μ s t) (ht : NullMeasurableSet t μ) (hfs : IntegrableOn f s μ) (hft : IntegrableOn f t μ) :
∫ (x : X) in s ∪ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ + ∫ (x : X) in t, f x ∂μ
source
theorem MeasureTheory.setIntegral_union {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {s t : Set X} {μ : Measure X} (hst : Disjoint s t) (ht : MeasurableSet t) (hfs : IntegrableOn f s μ) (hft : IntegrableOn f t μ) :
∫ (x : X) in s ∪ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ + ∫ (x : X) in t, f x ∂μ
source
theorem MeasureTheory.integral_diff {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {s t : Set X} {μ : Measure X} (ht : MeasurableSet t) (hfs : IntegrableOn f s μ) (hts : t ⊆ s) :
∫ (x : X) in s \ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ - ∫ (x : X) in t, f x ∂μ
source
theorem MeasureTheory.integral_inter_add_diff₀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {s t : Set X} {μ : Measure X} (ht : NullMeasurableSet t μ) (hfs : IntegrableOn f s μ) :
∫ (x : X) in s ∩ t, f x ∂μ + ∫ (x : X) in s \ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
source
theorem MeasureTheory.integral_inter_add_diff {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {s t : Set X} {μ : Measure X} (ht : MeasurableSet t) (hfs : IntegrableOn f s μ) :
∫ (x : X) in s ∩ t, f x ∂μ + ∫ (x : X) in s \ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
source
theorem MeasureTheory.integral_biUnion_finset {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {μ : Measure X} {ι : Type u_5} (t : Finset ι) {s : ι → Set X} (hs : ∀ i ∈ t, MeasurableSet (s i)) (h's : (↑t).Pairwise (Function.onFun Disjoint s)) (hf : ∀ i ∈ t, IntegrableOn f (s i) μ) :
∫ (x : X) in ⋃ i ∈ t, s i, f x ∂μ = ∑ i ∈ t, ∫ (x : X) in s i, f x ∂μ
source
@[deprecated MeasureTheory.integral_biUnion_finset (since := "2025-08-28")]
theorem MeasureTheory.integral_finset_biUnion {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {μ : Measure X} {ι : Type u_5} (t : Finset ι) {s : ι → Set X} (hs : ∀ i ∈ t, MeasurableSet (s i)) (h's : (↑t).Pairwise (Function.onFun Disjoint s)) (hf : ∀ i ∈ t, IntegrableOn f (s i) μ) :
∫ (x : X) in ⋃ i ∈ t, s i, f x ∂μ = ∑ i ∈ t, ∫ (x : X) in s i, f x ∂μ

Alias of `MeasureTheory.integral_biUnion_finset`.

source
theorem MeasureTheory.integral_iUnion_fintype {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {μ : Measure X} {ι : Type u_5} [Fintype ι] {s : ι → Set X} (hs : ∀ (i : ι), MeasurableSet (s i)) (h's : Pairwise (Function.onFun Disjoint s)) (hf : ∀ (i : ι), IntegrableOn f (s i) μ) :
∫ (x : X) in ⋃ (i : ι), s i, f x ∂μ = ∑ i : ι, ∫ (x : X) in s i, f x ∂μ
source
@[deprecated MeasureTheory.integral_iUnion_fintype (since := "2025-08-28")]
theorem MeasureTheory.integral_fintype_iUnion {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {μ : Measure X} {ι : Type u_5} [Fintype ι] {s : ι → Set X} (hs : ∀ (i : ι), MeasurableSet (s i)) (h's : Pairwise (Function.onFun Disjoint s)) (hf : ∀ (i : ι), IntegrableOn f (s i) μ) :
∫ (x : X) in ⋃ (i : ι), s i, f x ∂μ = ∑ i : ι, ∫ (x : X) in s i, f x ∂μ

Alias of `MeasureTheory.integral_iUnion_fintype`.

source
theorem MeasureTheory.setIntegral_empty {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {μ : Measure X} :
∫ (x : X) in ∅, f x ∂μ = 0
source
theorem MeasureTheory.setIntegral_univ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {μ : Measure X} :
∫ (x : X) in Set.univ, f x ∂μ = ∫ (x : X), f x ∂μ
source
theorem MeasureTheory.integral_add_compl₀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {s : Set X} {μ : Measure X} (hs : NullMeasurableSet s μ) (hfi : Integrable f μ) :
∫ (x : X) in s, f x ∂μ + ∫ (x : X) in s ᶜ, f x ∂μ = ∫ (x : X), f x ∂μ
source
theorem MeasureTheory.integral_add_compl {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {s : Set X} {μ : Measure X} (hs : MeasurableSet s) (hfi : Integrable f μ) :
∫ (x : X) in s, f x ∂μ + ∫ (x : X) in s ᶜ, f x ∂μ = ∫ (x : X), f x ∂μ
source
theorem MeasureTheory.setIntegral_compl {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {s : Set X} {μ : Measure X} (hs : MeasurableSet s) (hfi : Integrable f μ) :
∫ (x : X) in s ᶜ, f x ∂μ = ∫ (x : X), f x ∂μ - ∫ (x : X) in s, f x ∂μ
source
theorem MeasureTheory.integral_indicator {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {s : Set X} {μ : Measure X} (hs : MeasurableSet s) :
∫ (x : X), s.indicator f x ∂μ = ∫ (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)`.

source
theorem MeasureTheory.integral_indicator₀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {s : Set X} {μ : Measure X} (hs : NullMeasurableSet s μ) :
∫ (x : X), s.indicator f x ∂μ = ∫ (x : X) in s, f x ∂μ
source
theorem MeasureTheory.integral_integral_indicator {X : Type u_1} {Y : Type u_2} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : Measure X} {mY : MeasurableSpace Y} {ν : Measure Y} (f : X → Y → E) {s : Set X} (hs : MeasurableSet s) :
∫ (x : X), ∫ (y : Y), s.indicator (fun (x : X) => f x y) x ∂ν ∂μ = ∫ (x : X) in s, ∫ (y : Y), f x y ∂ν ∂μ
source
theorem MeasureTheory.setIntegral_indicator {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {s t : Set X} {μ : Measure X} (ht : MeasurableSet t) :
∫ (x : X) in s, t.indicator f x ∂μ = ∫ (x : X) in s ∩ t, f x ∂μ
source
theorem MeasureTheory.integral_biUnion_eq_sum_powerset {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {μ : Measure X} {ι : Type u_5} {t : Finset ι} {s : ι → Set X} (hs : ∀ i ∈ t, MeasurableSet (s i)) (hf : ∀ i ∈ t, IntegrableOn f (s i) μ) :
∫ (x : X) in ⋃ i ∈ t, s i, f x ∂μ = ∑ u ∈ t.powerset with u.Nonempty, (-1) ^ (u.card + 1) • ∫ (x : X) in ⋂ i ∈ u, s i, f x ∂μ

Inclusion-exclusion principle for the integral of a function over a union.

The integral of a function `f` over the union of the `s i` over `i ∈ t` is the alternating sum of the integrals of `f` over the intersections of the `s i`.

source
theorem MeasureTheory.ofReal_setIntegral_one_of_measure_ne_top {X : Type u_5} {m : MeasurableSpace X} {μ : Measure X} {s : Set X} (hs : μ s ≠ ⊤ := by finiteness) :
ENNReal.ofReal (∫ (x : X) in s, 1 ∂μ) = μ s
source
theorem MeasureTheory.ofReal_setIntegral_one {X : Type u_5} {x✝ : MeasurableSpace X} (μ : Measure X) [IsFiniteMeasure μ] (s : Set X) :
ENNReal.ofReal (∫ (x : X) in s, 1 ∂μ) = μ s
source
theorem MeasureTheory.setIntegral_one_eq_measureReal {X : Type u_5} {m : MeasurableSpace X} {μ : Measure X} {s : Set X} :
∫ (x : X) in s, 1 ∂μ = μ.real s
source
theorem MeasureTheory.measureReal_biUnion_eq_sum_powerset {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {ι : Type u_5} {t : Finset ι} {s : ι → Set X} (hs : ∀ i ∈ t, MeasurableSet (s i)) (hf : ∀ i ∈ t, μ (s i) ≠ ⊤ := by finiteness) :
μ.real (⋃ i ∈ t, s i) = ∑ u ∈ t.powerset with u.Nonempty, (-1) ^ (u.card + 1) * μ.real (⋂ i ∈ u, s i)

Inclusion-exclusion principle for the measure of a union of sets of finite measure.

The measure of the union of the `s i` over `i ∈ t` is the alternating sum of the measures of the intersections of the `s i`.

source
theorem MeasureTheory.integral_piecewise {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : X → E} {s : Set X} {μ : Measure X} [DecidablePred fun (x : X) => x ∈ s] (hs : MeasurableSet s) (hf : IntegrableOn f s μ) (hg : IntegrableOn g s ᶜ μ) :
∫ (x : X), s.piecewise f g x ∂μ = ∫ (x : X) in s, f x ∂μ + ∫ (x : X) in s ᶜ, g x ∂μ
source
theorem MeasureTheory.tendsto_setIntegral_of_monotone {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {μ : Measure X} {ι : Type u_5} [Preorder ι] [Filter.atTop.IsCountablyGenerated] {s : ι → Set X} (hsm : ∀ (i : ι), MeasurableSet (s i)) (h_mono : Monotone s) (hfi : IntegrableOn f (⋃ (n : ι), s n) μ) :
Filter.Tendsto (fun (i : ι) => ∫ (x : X) in s i, f x ∂μ) Filter.atTop (nhds (∫ (x : X) in ⋃ (n : ι), s n, f x ∂μ))
source
theorem MeasureTheory.tendsto_setIntegral_of_antitone {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {μ : Measure X} {ι : Type u_5} [Preorder ι] [Filter.atTop.IsCountablyGenerated] {s : ι → Set X} (hsm : ∀ (i : ι), MeasurableSet (s i)) (h_anti : Antitone s) (hfi : ∃ (i : ι), IntegrableOn f (s i) μ) :
Filter.Tendsto (fun (i : ι) => ∫ (x : X) in s i, f x ∂μ) Filter.atTop (nhds (∫ (x : X) in ⋂ (n : ι), s n, f x ∂μ))
source
theorem MeasureTheory.hasSum_integral_iUnion_ae {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {μ : Measure X} {ι : Type u_5} [Countable ι] {s : ι → Set X} (hm : ∀ (i : ι), NullMeasurableSet (s i) μ) (hd : Pairwise (Function.onFun (AEDisjoint μ) s)) (hfi : IntegrableOn f (⋃ (i : ι), s i) μ) :
HasSum (fun (n : ι) => ∫ (x : X) in s n, f x ∂μ) (∫ (x : X) in ⋃ (n : ι), s n, f x ∂μ)
source
theorem MeasureTheory.hasSum_integral_iUnion {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {μ : Measure X} {ι : Type u_5} [Countable ι] {s : ι → Set X} (hm : ∀ (i : ι), MeasurableSet (s i)) (hd : Pairwise (Function.onFun Disjoint s)) (hfi : IntegrableOn f (⋃ (i : ι), s i) μ) :
HasSum (fun (n : ι) => ∫ (x : X) in s n, f x ∂μ) (∫ (x : X) in ⋃ (n : ι), s n, f x ∂μ)
source
theorem MeasureTheory.integral_iUnion {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {μ : Measure X} {ι : Type u_5} [Countable ι] {s : ι → Set X} (hm : ∀ (i : ι), MeasurableSet (s i)) (hd : Pairwise (Function.onFun Disjoint s)) (hfi : IntegrableOn f (⋃ (i : ι), s i) μ) :
∫ (x : X) in ⋃ (n : ι), s n, f x ∂μ = ∑' (n : ι), ∫ (x : X) in s n, f x ∂μ
source
theorem MeasureTheory.integral_iUnion_ae {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {μ : Measure X} {ι : Type u_5} [Countable ι] {s : ι → Set X} (hm : ∀ (i : ι), NullMeasurableSet (s i) μ) (hd : Pairwise (Function.onFun (AEDisjoint μ) s)) (hfi : IntegrableOn f (⋃ (i : ι), s i) μ) :
∫ (x : X) in ⋃ (n : ι), s n, f x ∂μ = ∑' (n : ι), ∫ (x : X) in s n, f x ∂μ
source
theorem MeasureTheory.setIntegral_eq_zero_of_ae_eq_zero {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {t : Set X} {μ : Measure X} (ht_eq : ∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0) :
∫ (x : X) in t, f x ∂μ = 0
source
theorem MeasureTheory.setIntegral_eq_zero_of_forall_eq_zero {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {t : Set X} {μ : Measure X} (ht_eq : ∀ x ∈ t, f x = 0) :
∫ (x : X) in t, f x ∂μ = 0
source
theorem MeasureTheory.integral_union_eq_left_of_ae_aux {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {s t : Set X} {μ : Measure X} (ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0) (haux : StronglyMeasurable f) (H : IntegrableOn f (s ∪ t) μ) :
∫ (x : X) in s ∪ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
source
theorem MeasureTheory.integral_union_eq_left_of_ae {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {s t : Set X} {μ : Measure X} (ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0) :
∫ (x : X) in s ∪ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
source
theorem MeasureTheory.integral_union_eq_left_of_forall₀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {s t : Set X} {μ : Measure X} {f : X → E} (ht : NullMeasurableSet t μ) (ht_eq : ∀ x ∈ t, f x = 0) :
∫ (x : X) in s ∪ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
source
theorem MeasureTheory.integral_union_eq_left_of_forall {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {s t : Set X} {μ : Measure X} {f : X → E} (ht : MeasurableSet t) (ht_eq : ∀ x ∈ t, f x = 0) :
∫ (x : X) in s ∪ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
source
theorem MeasureTheory.setIntegral_eq_of_subset_of_ae_diff_eq_zero_aux {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {s t : Set X} {μ : Measure X} (hts : s ⊆ t) (h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0) (haux : StronglyMeasurable f) (h'aux : IntegrableOn f t μ) :
∫ (x : X) in t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
source
theorem MeasureTheory.setIntegral_eq_of_subset_of_ae_diff_eq_zero {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {s t : Set X} {μ : Measure X} (ht : NullMeasurableSet t μ) (hts : s ⊆ t) (h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0) :
∫ (x : X) in t, f x ∂μ = ∫ (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.

source
theorem MeasureTheory.setIntegral_eq_of_subset_of_forall_diff_eq_zero {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {s t : Set X} {μ : Measure X} (ht : MeasurableSet t) (hts : s ⊆ t) (h't : ∀ x ∈ t \ s, f x = 0) :
∫ (x : X) in t, f x ∂μ = ∫ (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.

source
theorem MeasureTheory.setIntegral_eq_integral_of_ae_compl_eq_zero {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {s : Set X} {μ : Measure X} (h : ∀ᵐ (x : X) ∂μ, x ∉ s → f x = 0) :
∫ (x : X) in s, f x ∂μ = ∫ (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.

source
theorem MeasureTheory.setIntegral_eq_integral_of_forall_compl_eq_zero {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {s : Set X} {μ : Measure X} (h : ∀ x ∉ s, f x = 0) :
∫ (x : X) in s, f x ∂μ = ∫ (x : X), f x ∂μ

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

source
theorem MeasureTheory.setIntegral_neg_eq_setIntegral_nonpos {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : Measure X} [PartialOrder E] {f : X → E} (hf : AEStronglyMeasurable f μ) :
∫ (x : X) in {x : X | f x < 0}, f x ∂μ = ∫ (x : X) in {x : X | f x ≤ 0}, f x ∂μ
source
theorem MeasureTheory.integral_norm_eq_pos_sub_neg {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {f : X → ℝ} (hfi : Integrable f μ) :
∫ (x : X), ‖f x‖ ∂μ = ∫ (x : X) in {x : X | 0 ≤ f x}, f x ∂μ - ∫ (x : X) in {x : X | f x ≤ 0}, f x ∂μ
source
theorem MeasureTheory.setIntegral_const {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set X} {μ : Measure X} [CompleteSpace E] (c : E) :
∫ (x : X) in s, c ∂μ = μ.real s • c
source
@[simp]
theorem MeasureTheory.integral_indicator_const {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : Measure X} [CompleteSpace E] (e : E) ⦃s : Set X⦄ (s_meas : MeasurableSet s) :
∫ (x : X), s.indicator (fun (x : X) => e) x ∂μ = μ.real s • e
source
@[simp]
theorem MeasureTheory.integral_indicator_one {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} ⦃s : Set X⦄ (hs : MeasurableSet s) :
∫ (x : X), s.indicator 1 x ∂μ = μ.real s
source
theorem MeasureTheory.setIntegral_indicatorConstLp {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {s t : Set X} {μ : Measure X} [CompleteSpace E] {p : ENNReal} (hs : MeasurableSet s) (ht : MeasurableSet t) (hμt : μ t ≠ ⊤) (e : E) :
∫ (x : X) in s, ↑↑(indicatorConstLp p ht hμt e) x ∂μ = μ.real (t ∩ s) • e
source
theorem MeasureTheory.integral_indicatorConstLp {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {t : Set X} {μ : Measure X} [CompleteSpace E] {p : ENNReal} (ht : MeasurableSet t) (hμt : μ t ≠ ⊤) (e : E) :
∫ (x : X), ↑↑(indicatorConstLp p ht hμt e) x ∂μ = μ.real t • e
source
theorem MeasureTheory.setIntegral_map {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : Measure X} {Y : Type u_5} [MeasurableSpace Y] {g : X → Y} {f : Y → E} {s : Set Y} (hs : MeasurableSet s) (hf : AEStronglyMeasurable f (Measure.map g μ)) (hg : AEMeasurable g μ) :
∫ (y : Y) in s, f y ∂Measure.map g μ = ∫ (x : X) in g ⁻¹' s, f (g x) ∂μ
source
theorem MeasurableEmbedding.setIntegral_map {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : MeasureTheory.Measure X} {Y : Type u_5} {x✝ : MeasurableSpace Y} {f : X → Y} (hf : MeasurableEmbedding f) (g : Y → E) (s : Set Y) :
∫ (y : Y) in s, g y ∂MeasureTheory.Measure.map f μ = ∫ (x : X) in f ⁻¹' s, g (f x) ∂μ
source
theorem Topology.IsClosedEmbedding.setIntegral_map {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : MeasureTheory.Measure X} [TopologicalSpace X] [BorelSpace X] {Y : Type u_5} [MeasurableSpace Y] [TopologicalSpace Y] [BorelSpace Y] {g : X → Y} {f : Y → E} (s : Set Y) (hg : IsClosedEmbedding g) :
∫ (y : Y) in s, f y ∂MeasureTheory.Measure.map g μ = ∫ (x : X) in g ⁻¹' s, f (g x) ∂μ
source
theorem MeasureTheory.MeasurePreserving.setIntegral_preimage_emb {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : Measure X} {Y : Type u_5} {x✝ : MeasurableSpace Y} {f : X → Y} {ν : Measure Y} (h₁ : MeasurePreserving f μ ν) (h₂ : MeasurableEmbedding f) (g : Y → E) (s : Set Y) :
∫ (x : X) in f ⁻¹' s, g (f x) ∂μ = ∫ (y : Y) in s, g y ∂ν
source
theorem MeasureTheory.MeasurePreserving.setIntegral_image_emb {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : Measure X} {Y : Type u_5} {x✝ : MeasurableSpace Y} {f : X → Y} {ν : Measure Y} (h₁ : MeasurePreserving f μ ν) (h₂ : MeasurableEmbedding f) (g : Y → E) (s : Set X) :
∫ (y : Y) in f '' s, g y ∂ν = ∫ (x : X) in s, g (f x) ∂μ
source
theorem MeasureTheory.setIntegral_map_equiv {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : Measure X} {Y : Type u_5} [MeasurableSpace Y] (e : X ≃ᵐ Y) (f : Y → E) (s : Set Y) :
∫ (y : Y) in s, f y ∂Measure.map (⇑e) μ = ∫ (x : X) in ⇑e ⁻¹' s, f (e x) ∂μ
source
theorem MeasureTheory.norm_setIntegral_le_of_norm_le_const_ae {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {s : Set X} {μ : Measure X} {C : ℝ} (hs : μ s < ⊤) (hC : ∀ᵐ (x : X) ∂μ.restrict s, ‖f x‖ ≤ C) :
‖∫ (x : X) in s, f x ∂μ‖ ≤ C * μ.real s
source
theorem MeasureTheory.norm_setIntegral_le_of_norm_le_const_ae' {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {s : Set X} {μ : Measure X} {C : ℝ} (hs : μ s < ⊤) (hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C) :
‖∫ (x : X) in s, f x ∂μ‖ ≤ C * μ.real s
source
theorem MeasureTheory.norm_setIntegral_le_of_norm_le_const {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {s : Set X} {μ : Measure X} {C : ℝ} (hs : μ s < ⊤) (hC : ∀ x ∈ s, ‖f x‖ ≤ C) :
‖∫ (x : X) in s, f x ∂μ‖ ≤ C * μ.real s
source
theorem MeasureTheory.norm_integral_sub_setIntegral_le {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {μ : Measure X} [IsFiniteMeasure μ] {C : ℝ} (hf : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C) {s : Set X} (hs : MeasurableSet s) (hf1 : Integrable f μ) :
‖∫ (x : X), f x ∂μ - ∫ (x : X) in s, f x ∂μ‖ ≤ μ.real s ᶜ * C
source
theorem MeasureTheory.setIntegral_eq_zero_iff_of_nonneg_ae {X : Type u_1} {mX : MeasurableSpace X} {s : Set X} {μ : Measure X} {f : X → ℝ} (hf : 0 ≤ᶠ[ae (μ.restrict s)] f) (hfi : IntegrableOn f s μ) :
∫ (x : X) in s, f x ∂μ = 0 ↔ f =ᶠ[ae (μ.restrict s)] 0
source
theorem MeasureTheory.setIntegral_pos_iff_support_of_nonneg_ae {X : Type u_1} {mX : MeasurableSpace X} {s : Set X} {μ : Measure X} {f : X → ℝ} (hf : 0 ≤ᶠ[ae (μ.restrict s)] f) (hfi : IntegrableOn f s μ) :
0 < ∫ (x : X) in s, f x ∂μ ↔ 0 < μ (Function.support f ∩ s)
source
theorem MeasureTheory.setIntegral_gt_gt {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {R : ℝ} {f : X → ℝ} (hR : 0 ≤ R) (hfint : IntegrableOn f {x : X | R < f x} μ) (hμ : μ {x : X | R < f x} ≠ 0) :
μ.real {x : X | R < f x} * R < ∫ (x : X) in {x : X | R < f x}, f x ∂μ
source
theorem MeasureTheory.setIntegral_trim {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : Type u_5} {m m0 : MeasurableSpace X} {μ : Measure X} (hm : m ≤ m0) {f : X → E} (hf_meas : StronglyMeasurable f) {s : Set X} (hs : MeasurableSet s) :
∫ (x : X) in s, f x ∂μ = ∫ (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 `[NoAtoms μ]`.

source
theorem MeasureTheory.integral_Icc_eq_integral_Ioc' {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {μ : Measure X} [PartialOrder X] {x y : X} (hx : μ {x} = 0) :
∫ (t : X) in Set.Icc x y, f t ∂μ = ∫ (t : X) in Set.Ioc x y, f t ∂μ
source
theorem MeasureTheory.integral_Icc_eq_integral_Ico' {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {μ : Measure X} [PartialOrder X] {x y : X} (hy : μ {y} = 0) :
∫ (t : X) in Set.Icc x y, f t ∂μ = ∫ (t : X) in Set.Ico x y, f t ∂μ
source
theorem MeasureTheory.integral_Ioc_eq_integral_Ioo' {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {μ : Measure X} [PartialOrder X] {x y : X} (hy : μ {y} = 0) :
∫ (t : X) in Set.Ioc x y, f t ∂μ = ∫ (t : X) in Set.Ioo x y, f t ∂μ
source
theorem MeasureTheory.integral_Ico_eq_integral_Ioo' {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {μ : Measure X} [PartialOrder X] {x y : X} (hx : μ {x} = 0) :
∫ (t : X) in Set.Ico x y, f t ∂μ = ∫ (t : X) in Set.Ioo x y, f t ∂μ
source
theorem MeasureTheory.integral_Icc_eq_integral_Ioo' {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {μ : Measure X} [PartialOrder X] {x y : X} (hx : μ {x} = 0) (hy : μ {y} = 0) :
∫ (t : X) in Set.Icc x y, f t ∂μ = ∫ (t : X) in Set.Ioo x y, f t ∂μ
source
theorem MeasureTheory.integral_Iic_eq_integral_Iio' {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {μ : Measure X} [PartialOrder X] {x : X} (hx : μ {x} = 0) :
∫ (t : X) in Set.Iic x, f t ∂μ = ∫ (t : X) in Set.Iio x, f t ∂μ
source
theorem MeasureTheory.integral_Ici_eq_integral_Ioi' {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {μ : Measure X} [PartialOrder X] {x : X} (hx : μ {x} = 0) :
∫ (t : X) in Set.Ici x, f t ∂μ = ∫ (t : X) in Set.Ioi x, f t ∂μ
source
theorem MeasureTheory.integral_Icc_eq_integral_Ioc {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {μ : Measure X} [PartialOrder X] {x y : X} [NoAtoms μ] :
∫ (t : X) in Set.Icc x y, f t ∂μ = ∫ (t : X) in Set.Ioc x y, f t ∂μ
source
theorem MeasureTheory.integral_Icc_eq_integral_Ico {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {μ : Measure X} [PartialOrder X] {x y : X} [NoAtoms μ] :
∫ (t : X) in Set.Icc x y, f t ∂μ = ∫ (t : X) in Set.Ico x y, f t ∂μ
source
theorem MeasureTheory.integral_Ioc_eq_integral_Ioo {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {μ : Measure X} [PartialOrder X] {x y : X} [NoAtoms μ] :
∫ (t : X) in Set.Ioc x y, f t ∂μ = ∫ (t : X) in Set.Ioo x y, f t ∂μ
source
theorem MeasureTheory.integral_Ico_eq_integral_Ioo {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {μ : Measure X} [PartialOrder X] {x y : X} [NoAtoms μ] :
∫ (t : X) in Set.Ico x y, f t ∂μ = ∫ (t : X) in Set.Ioo x y, f t ∂μ
source
theorem MeasureTheory.integral_Icc_eq_integral_Ioo {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {μ : Measure X} [PartialOrder X] {x y : X} [NoAtoms μ] :
∫ (t : X) in Set.Icc x y, f t ∂μ = ∫ (t : X) in Set.Ioo x y, f t ∂μ
source
theorem MeasureTheory.integral_Iic_eq_integral_Iio {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {μ : Measure X} [PartialOrder X] {x : X} [NoAtoms μ] :
∫ (t : X) in Set.Iic x, f t ∂μ = ∫ (t : X) in Set.Iio x, f t ∂μ
source
theorem MeasureTheory.integral_Ici_eq_integral_Ioi {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {μ : Measure X} [PartialOrder X] {x : X} [NoAtoms μ] :
∫ (t : X) in Set.Ici x, f t ∂μ = ∫ (t : X) in Set.Ioi x, f t ∂μ
source
theorem MeasureTheory.setIntegral_mono_ae_restrict {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {f g : X → ℝ} {s : Set X} (hf : IntegrableOn f s μ) (hg : IntegrableOn g s μ) (h : f ≤ᶠ[ae (μ.restrict s)] g) :
∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ
source
theorem MeasureTheory.setIntegral_mono_ae {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {f g : X → ℝ} {s : Set X} (hf : IntegrableOn f s μ) (hg : IntegrableOn g s μ) (h : f ≤ᶠ[ae μ] g) :
∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ
source
theorem MeasureTheory.setIntegral_mono_on {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {f g : X → ℝ} {s : Set X} (hf : IntegrableOn f s μ) (hg : IntegrableOn g s μ) (hs : MeasurableSet s) (h : ∀ x ∈ s, f x ≤ g x) :
∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ
source
theorem MeasureTheory.setIntegral_mono_on_ae {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {f g : X → ℝ} {s : Set X} (hf : IntegrableOn f s μ) (hg : IntegrableOn g s μ) (hs : MeasurableSet s) (h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x) :
∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ
source
theorem MeasureTheory.setIntegral_mono_on_ae₀ {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {f g : X → ℝ} {s : Set X} (hf : IntegrableOn f s μ) (hg : IntegrableOn g s μ) (hs : NullMeasurableSet s μ) (h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x) :
∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ
source
theorem MeasureTheory.setIntegral_mono_on₀ {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {f g : X → ℝ} {s : Set X} (hf : IntegrableOn f s μ) (hg : IntegrableOn g s μ) (hs : NullMeasurableSet s μ) (h : ∀ x ∈ s, f x ≤ g x) :
∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ
source
theorem MeasureTheory.setIntegral_mono {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {f g : X → ℝ} {s : Set X} (hf : IntegrableOn f s μ) (hg : IntegrableOn g s μ) (h : f ≤ g) :
∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ
source
theorem MeasureTheory.setIntegral_mono_set {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {f : X → ℝ} {s t : Set X} (hfi : IntegrableOn f t μ) (hf : 0 ≤ᶠ[ae (μ.restrict t)] f) (hst : s ≤ᶠ[ae μ] t) :
∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in t, f x ∂μ
source
theorem MeasureTheory.setIntegral_le_integral {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {f : X → ℝ} {s : Set X} (hfi : Integrable f μ) (hf : 0 ≤ᶠ[ae μ] f) :
∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X), f x ∂μ
source
theorem MeasureTheory.setIntegral_ge_of_const_le {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {f : X → ℝ} {s : Set X} {c : ℝ} (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (hf : ∀ x ∈ s, c ≤ f x) (hfint : IntegrableOn (fun (x : X) => f x) s μ) :
c * μ.real s ≤ ∫ (x : X) in s, f x ∂μ
source
theorem MeasureTheory.setIntegral_nonneg_of_ae_restrict {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {f : X → ℝ} {s : Set X} (hf : 0 ≤ᶠ[ae (μ.restrict s)] f) :
0 ≤ ∫ (x : X) in s, f x ∂μ
source
theorem MeasureTheory.setIntegral_nonneg_of_ae {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {f : X → ℝ} {s : Set X} (hf : 0 ≤ᶠ[ae μ] f) :
0 ≤ ∫ (x : X) in s, f x ∂μ
source
theorem MeasureTheory.setIntegral_nonneg {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {f : X → ℝ} {s : Set X} (hs : MeasurableSet s) (hf : ∀ x ∈ s, 0 ≤ f x) :
0 ≤ ∫ (x : X) in s, f x ∂μ
source
theorem MeasureTheory.setIntegral_nonneg_ae {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {f : X → ℝ} {s : Set X} (hs : MeasurableSet s) (hf : ∀ᵐ (x : X) ∂μ, x ∈ s → 0 ≤ f x) :
0 ≤ ∫ (x : X) in s, f x ∂μ
source
theorem MeasureTheory.setIntegral_le_nonneg {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {f : X → ℝ} {s : Set X} (hs : MeasurableSet s) (hf : StronglyMeasurable f) (hfi : Integrable f μ) :
∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in {y : X | 0 ≤ f y}, f x ∂μ
source
theorem MeasureTheory.setIntegral_nonpos_of_ae_restrict {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {f : X → ℝ} {s : Set X} (hf : f ≤ᶠ[ae (μ.restrict s)] 0) :
∫ (x : X) in s, f x ∂μ ≤ 0
source
theorem MeasureTheory.setIntegral_nonpos_of_ae {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {f : X → ℝ} {s : Set X} (hf : f ≤ᶠ[ae μ] 0) :
∫ (x : X) in s, f x ∂μ ≤ 0
source
theorem MeasureTheory.setIntegral_nonpos_ae {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {f : X → ℝ} {s : Set X} (hs : MeasurableSet s) (hf : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ 0) :
∫ (x : X) in s, f x ∂μ ≤ 0
source
theorem MeasureTheory.setIntegral_nonpos {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {f : X → ℝ} {s : Set X} (hs : MeasurableSet s) (hf : ∀ x ∈ s, f x ≤ 0) :
∫ (x : X) in s, f x ∂μ ≤ 0
source
theorem MeasureTheory.setIntegral_nonpos_le {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {f : X → ℝ} {s : Set X} (hs : MeasurableSet s) (hf : StronglyMeasurable f) (hfi : Integrable f μ) :
∫ (x : X) in {y : X | f y ≤ 0}, f x ∂μ ≤ ∫ (x : X) in s, f x ∂μ
source
theorem MeasureTheory.Integrable.measure_le_integral {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {f : X → ℝ} (f_int : Integrable f μ) (f_nonneg : 0 ≤ᶠ[ae μ] f) {s : Set X} (hs : ∀ x ∈ s, 1 ≤ f x) :
μ s ≤ ENNReal.ofReal (∫ (x : X), f x ∂μ)
source
theorem MeasureTheory.integral_le_measure {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {f : X → ℝ} {s : Set X} (hs : ∀ x ∈ s, f x ≤ 1) (h's : ∀ x ∈ s ᶜ, f x ≤ 0) :
ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ μ s
source
theorem MeasureTheory.integrableOn_iUnion_of_summable_integral_norm {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} {ι : Type u_5} [Countable ι] {μ : Measure X} [NormedAddCommGroup E] {f : X → E} {s : ι → Set X} (hi : ∀ (i : ι), IntegrableOn f (s i) μ) (h : Summable fun (i : ι) => ∫ (x : X) in s i, ‖f x‖ ∂μ) :
IntegrableOn f (Set.iUnion s) μ
source
theorem MeasureTheory.integrableOn_iUnion_of_summable_norm_restrict {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} {ι : Type u_5} [Countable ι] {μ : Measure X} [NormedAddCommGroup E] [TopologicalSpace X] [BorelSpace X] [T2Space X] [IsLocallyFiniteMeasure μ] {f : C(X, E)} {s : ι → TopologicalSpace.Compacts X} (hf : Summable fun (i : ι) => ‖ContinuousMap.restrict (↑(s i)) f‖ * μ.real ↑(s i)) :
IntegrableOn (⇑f) (⋃ (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`.

source
theorem MeasureTheory.integrable_of_summable_norm_restrict {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} {ι : Type u_5} [Countable ι] {μ : Measure X} [NormedAddCommGroup E] [TopologicalSpace X] [BorelSpace X] [T2Space X] [IsLocallyFiniteMeasure μ] {f : C(X, E)} {s : ι → TopologicalSpace.Compacts X} (hf : Summable fun (i : ι) => ‖ContinuousMap.restrict (↑(s i)) f‖ * μ.real ↑(s i)) (hs : ⋃ (i : ι), ↑(s i) = Set.univ) :
Integrable (⇑f) μ

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

### Continuity of the set integral #

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

source
theorem MeasureTheory.Lp_toLp_restrict_add {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] {p : ENNReal} {μ : Measure X} (f g : ↥(Lp E p μ)) (s : Set X) :
MemLp.toLp ↑↑(f + g) ⋯ = MemLp.toLp ↑↑f ⋯ + MemLp.toLp ↑↑g ⋯

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

source
theorem MeasureTheory.Lp_toLp_restrict_smul {X : Type u_1} {F : Type u_4} {mX : MeasurableSpace X} {𝕜 : Type u_5} [NormedRing 𝕜] [NormedAddCommGroup F] [Module 𝕜 F] [IsBoundedSMul 𝕜 F] {p : ENNReal} {μ : Measure X} (c : 𝕜) (f : ↥(Lp F p μ)) (s : Set X) :
MemLp.toLp ↑↑(c • f) ⋯ = c • MemLp.toLp ↑↑f ⋯

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

source
theorem MeasureTheory.norm_Lp_toLp_restrict_le {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] {p : ENNReal} {μ : Measure X} (s : Set X) (f : ↥(Lp E p μ)) :
‖MemLp.toLp ↑↑f ⋯‖ ≤ ‖f‖

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

source
noncomputable def MeasureTheory.LpToLpRestrictCLM (X : Type u_1) (F : Type u_4) {mX : MeasurableSpace X} (𝕜 : Type u_5) [NormedRing 𝕜] [NormedAddCommGroup F] [Module 𝕜 F] [IsBoundedSMul 𝕜 F] (μ : Measure X) (p : ENNReal) [hp : Fact (1 ≤ p)] (s : Set X) :
↥(Lp F p μ) →L[𝕜] ↥(Lp F p (μ.restrict s))

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

Equations

- MeasureTheory.LpToLpRestrictCLM X F 𝕜 μ p s = { toFun := fun (f : ↥(MeasureTheory.Lp F p μ)) => MeasureTheory.MemLp.toLp ↑↑f ⋯, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous 1 ⋯

Instances For

source
theorem MeasureTheory.LpToLpRestrictCLM_coeFn {X : Type u_1} {F : Type u_4} {mX : MeasurableSpace X} (𝕜 : Type u_5) [NormedRing 𝕜] [NormedAddCommGroup F] [Module 𝕜 F] [IsBoundedSMul 𝕜 F] {p : ENNReal} {μ : Measure X} [Fact (1 ≤ p)] (s : Set X) (f : ↥(Lp F p μ)) :
↑↑((LpToLpRestrictCLM X F 𝕜 μ p s) f) =ᶠ[ae (μ.restrict s)] ↑↑f
source
theorem MeasureTheory.continuous_setIntegral {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] {μ : Measure X} [NormedSpace ℝ E] (s : Set X) :
Continuous fun (f : ↥(Lp E 1 μ)) => ∫ (x : X) in s, ↑↑f x ∂μ
source
theorem Continuous.integral_pos_of_hasCompactSupport_nonneg_nonzero {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [OpensMeasurableSpace X] {μ : MeasureTheory.Measure X} [μ.IsOpenPosMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ] {f : X → ℝ} {x : X} (f_cont : Continuous f) (f_comp : HasCompactSupport f) (f_nonneg : 0 ≤ f) (f_x : f x ≠ 0) :
0 < ∫ (x : X), f x ∂μ
source
theorem MeasureTheory.setIntegral_support {X : Type u_1} {M : Type u_5} [NormedAddCommGroup M] [NormedSpace ℝ M] {mX : MeasurableSpace X} {ν : Measure X} {F : X → M} :
∫ (x : X) in Function.support F, F x ∂ν = ∫ (x : X), F x ∂ν
source
theorem MeasureTheory.setIntegral_tsupport {X : Type u_1} {M : Type u_5} [NormedAddCommGroup M] [NormedSpace ℝ M] {mX : MeasurableSpace X} {ν : Measure X} {F : X → M} [TopologicalSpace X] :
∫ (x : X) in tsupport F, F x ∂ν = ∫ (x : X), F x ∂ν
source
theorem measure_le_lintegral_thickenedIndicatorAux {X : Type u_1} [MeasurableSpace X] [PseudoEMetricSpace X] (μ : MeasureTheory.Measure X) {E : Set X} (E_mble : MeasurableSet E) (δ : ℝ) :
μ E ≤ ∫⁻ (x : X), thickenedIndicatorAux δ E x ∂μ
source
theorem measure_le_lintegral_thickenedIndicator {X : Type u_1} [MeasurableSpace X] [PseudoEMetricSpace X] (μ : MeasureTheory.Measure X) {E : Set X} (E_mble : MeasurableSet E) {δ : ℝ} (δ_pos : 0 < δ) :
μ E ≤ ∫⁻ (x : X), ↑((thickenedIndicator δ_pos E) x) ∂μ
source
theorem MeasureTheory.Integrable.simpleFunc_mul {X : Type u_6} {f : X → ℝ} {m0 : MeasurableSpace X} {μ : Measure X} (g : SimpleFunc X ℝ) (hf : Integrable f μ) :
Integrable (⇑g * f) μ
source
theorem MeasureTheory.Integrable.simpleFunc_mul' {X : Type u_6} {f : X → ℝ} {m m0 : MeasurableSpace X} {μ : Measure X} (hm : m ≤ m0) (g : SimpleFunc X ℝ) (hf : Integrable f μ) :
Integrable (⇑g * f) μ
source
theorem continuous_parametric_integral_of_continuous {Y : Type u_2} {E : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [MeasurableSpace Y] [OpensMeasurableSpace Y] {μ : MeasureTheory.Measure Y} [NormedAddCommGroup E] [NormedSpace ℝ E] [FirstCountableTopology X] [LocallyCompactSpace X] [SecondCountableTopologyEither Y E] [MeasureTheory.IsLocallyFiniteMeasure μ] {f : X → Y → E} (hf : Continuous (Function.uncurry f)) {s : Set Y} (hs : IsCompact s) :
Continuous fun (x : X) => ∫ (y : Y) in s, f x y ∂μ

The parametric integral over a continuous function on a compact set is continuous, under mild assumptions on the topologies involved.

source
theorem continuousOn_integral_bilinear_of_locally_integrable_of_compact_support {Y : Type u_2} {E : Type u_3} {F : Type u_4} {X : Type u_5} {G : Type u_6} {𝕜 : Type u_7} [TopologicalSpace X] [TopologicalSpace Y] [MeasurableSpace Y] [OpensMeasurableSpace Y] {μ : MeasureTheory.Measure Y} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedSpace 𝕜 E] (L : F →L[𝕜] G →L[𝕜] E) {f : X → Y → G} {s : Set X} {k : Set Y} {g : Y → F} (hk : IsCompact k) (hf : ContinuousOn (Function.uncurry f) (s ×ˢ Set.univ)) (hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0) (hg : MeasureTheory.IntegrableOn g k μ) :
ContinuousOn (fun (x : X) => ∫ (y : Y), (L (g y)) (f x y) ∂μ) s

Consider a parameterized integral `x ↦ ∫ y, L (g y) (f x y)` where `L` is bilinear, `g` is locally integrable and `f` is continuous and uniformly compactly supported. Then the integral depends continuously on `x`.

source
theorem continuousOn_integral_of_compact_support {Y : Type u_2} {E : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [MeasurableSpace Y] [OpensMeasurableSpace Y] {μ : MeasureTheory.Measure Y} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → Y → E} {s : Set X} {k : Set Y} [MeasureTheory.IsFiniteMeasureOnCompacts μ] (hk : IsCompact k) (hf : ContinuousOn (Function.uncurry f) (s ×ˢ Set.univ)) (hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0) :
ContinuousOn (fun (x : X) => ∫ (y : Y), f x y ∂μ) s

Consider a parameterized integral `x ↦ ∫ y, f x y` where `f` is continuous and uniformly compactly supported. Then the integral depends continuously on `x`.