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.

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 ∂μ

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 ∂μ

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 ∂μ

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 ∂μ

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 ∂μ

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 : 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 ∂μ

@[deprecated MeasureTheory.setIntegral_union₀ (since := "2026-03-04")]

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 ∂μ

Alias of MeasureTheory.setIntegral_union₀.

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 ∂μ

theorem MeasureTheory.setIntegral_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 μ) (hts : t ⊆ s) : ∫ (x : X) in s \ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ - ∫ (x : X) in t, f x ∂μ

theorem MeasureTheory.setIntegral_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 ∂μ

@[deprecated MeasureTheory.setIntegral_diff (since := "2026-03-04")]

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 ∂μ

Alias of MeasureTheory.setIntegral_diff.

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 ∂μ

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 ∂μ

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 ∂μ

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

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 ∂μ

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

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

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 ∂μ

theorem MeasureTheory.integral_eq_setIntegral {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set X} {μ : Measure X} (hs : ∀ᵐ (x : X) ∂μ, x ∈ s) (f : X → E) : ∫ (x : X), f x ∂μ = ∫ (x : X) in s, f x ∂μ

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 ∂μ

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 ∂μ

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 : NullMeasurableSet s μ) (hfi : Integrable f μ) : ∫ (x : X) in sᶜ, f x ∂μ = ∫ (x : X), f x ∂μ - ∫ (x : X) in s, f x ∂μ

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 ∂μ

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

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 ∂μ

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 ∂ν ∂μ

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 ∂μ

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.

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

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

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

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.

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 ∂μ

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 : ι), NullMeasurableSet (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 ∂μ))

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 ∂μ))

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 ∂μ))

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 ∂μ)

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 ∂μ)

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 ∂μ

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 ∂μ

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

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

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 ∂μ

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 ∂μ

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 ∂μ

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 ∂μ

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 ∂μ

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.

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.

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.

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.

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 ∂μ

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 ∂μ

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

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

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

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

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

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) ∂μ

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) ∂μ

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) ∂μ

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 ∂ν

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) ∂μ

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) ∂μ

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

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

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

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

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

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)

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 ∂μ

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

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 ∂μ

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 ∂μ

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 ∂μ

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 ∂μ

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 ∂μ

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 ∂μ

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 ∂μ

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 ∂μ

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 ∂μ

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 ∂μ

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 ∂μ

theorem MeasureTheory.integral_Ico_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.Ico x y, f t ∂μ = ∫ (t : X) in Set.Ioc x y, f t ∂μ

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 ∂μ

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 ∂μ

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 ∂μ

theorem MeasureTheory.setIntegral_mono_set {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E] {μ : Measure X} {f : X → E} {s t : Set X} [OrderClosedTopology E] (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 ∂μ

theorem MeasureTheory.setIntegral_le_integral {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E] {μ : Measure X} {f : X → E} {s : Set X} [OrderClosedTopology E] (hfi : Integrable f μ) (hf : 0 ≤ᶠ[ae μ] f) : ∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X), f x ∂μ

theorem MeasureTheory.setIntegral_mono_ae_restrict {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E] {μ : Measure X} {f g : X → E} {s : Set X} [ClosedIciTopology E] (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 ∂μ

theorem MeasureTheory.setIntegral_mono_ae {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E] {μ : Measure X} {f g : X → E} {s : Set X} [ClosedIciTopology E] (hf : IntegrableOn f s μ) (hg : IntegrableOn g s μ) (h : f ≤ᶠ[ae μ] g) : ∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ

theorem MeasureTheory.setIntegral_mono_on {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E] {μ : Measure X} {f g : X → E} {s : Set X} [ClosedIciTopology E] (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 ∂μ

theorem MeasureTheory.setIntegral_mono_on_ae {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E] {μ : Measure X} {f g : X → E} {s : Set X} [ClosedIciTopology E] (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 ∂μ

theorem MeasureTheory.setIntegral_mono_on_ae₀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E] {μ : Measure X} {f g : X → E} {s : Set X} [ClosedIciTopology E] (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 ∂μ

theorem MeasureTheory.setIntegral_mono_on₀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E] {μ : Measure X} {f g : X → E} {s : Set X} [ClosedIciTopology E] (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 ∂μ

theorem MeasureTheory.setIntegral_mono {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E] {μ : Measure X} {f g : X → E} {s : Set X} [ClosedIciTopology E] (hf : IntegrableOn f s μ) (hg : IntegrableOn g s μ) (h : f ≤ g) : ∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ

theorem MeasureTheory.setIntegral_ge_of_const_le {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E] {μ : Measure X} {f : X → E} {s : Set X} [ClosedIciTopology E] [CompleteSpace E] {c : E} (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (hf : ∀ x ∈ s, c ≤ f x) (hfint : IntegrableOn (fun (x : X) => f x) s μ) : μ.real s • c ≤ ∫ (x : X) in s, f x ∂μ

theorem MeasureTheory.setIntegral_ge_of_const_le_real {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {s : Set X} {f : 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 ∂μ

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 ∂μ

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 ∂μ

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 ∂μ

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 ∂μ

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 ∂μ

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

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

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

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

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 ∂μ

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 ∂μ)

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

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

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.

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.

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.

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.

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.

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 ⋯

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

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 ∂μ

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 ∂μ

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 ∂ν

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 ∂ν

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 ∂μ

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) ∂μ

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

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

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.

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.

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.