Measure spaces

The definition of a measure and a measure space are in MeasureTheory.MeasureSpaceDef, with only a few basic properties. This file provides many more properties of these objects related to set operations. This separation allows the measurability tactic to import only the file MeasureSpaceDef, and to be available in MeasureSpace (through MeasurableSpace).

Given a measurable space α, a measure on α is a function that sends measurable sets to the extended nonnegative reals that satisfies the following conditions:

1. μ ∅ = 0;
2. μ is countably additive. This means that the measure of a countable union of pairwise disjoint sets is equal to the measure of the individual sets.

Every measure can be canonically extended to an outer measure, so that it assigns values to all subsets, not just the measurable subsets. On the other hand, an outer measure that is countably additive on measurable sets can be restricted to measurable sets to obtain a measure. In this file a measure is defined to be an outer measure that is countably additive on measurable sets, with the additional assumption that the outer measure is the canonical extension of the restricted measure.

Implementation notes

Given μ : Measure α, μ s is the value of the outer measure applied to s. This conveniently allows us to apply the measure to sets without proving that they are measurable. We get countable subadditivity for all sets, but only countable additivity for measurable sets.

You often don't want to define a measure via its constructor. Two ways that are sometimes more convenient:

• Measure.ofMeasurable is a way to define a measure by only giving its value on measurable sets and proving the properties (1) and (2) mentioned above.
• OuterMeasure.toMeasure is a way of obtaining a measure from an outer measure by showing that all measurable sets in the measurable space are Carathéodory measurable.

To prove that two measures are equal, there are multiple options:

• ext: two measures are equal if they are equal on all measurable sets.
• ext_of_generateFrom_of_iUnion: two measures are equal if they are equal on a π-system generating the measurable sets, if the π-system contains a spanning increasing sequence of sets where the measures take finite value (in particular the measures are σ-finite). This is a special case of the more general ext_of_generateFrom_of_cover
• ext_of_generate_finite: two finite measures are equal if they are equal on a π-system generating the measurable sets. This is a special case of ext_of_generateFrom_of_iUnion using C ∪ {univ}, but is easier to work with.

A MeasureSpace is a class that is a measurable space with a canonical measure. The measure is denoted volume.

References

• https://en.wikipedia.org/wiki/Measure_(mathematics)
• https://en.wikipedia.org/wiki/Almost_everywhere

Tags

measure, almost everywhere, measure space

theorem MeasureTheory.measure_union {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s₁ s₂ : Set α} (hd : Disjoint s₁ s₂) (h : MeasurableSet s₂) : μ (s₁ ∪ s₂) = μ s₁ + μ s₂

theorem MeasureTheory.measure_union' {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s₁ s₂ : Set α} (hd : Disjoint s₁ s₂) (h : MeasurableSet s₁) : μ (s₁ ∪ s₂) = μ s₁ + μ s₂

theorem MeasureTheory.measure_inter_add_sdiff {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {t : Set α} (s : Set α) (ht : MeasurableSet t) : μ (s ∩ t) + μ (s \ t) = μ s

@[deprecated MeasureTheory.measure_inter_add_sdiff (since := "2026-06-03")]

theorem MeasureTheory.measure_inter_add_diff {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {t : Set α} (s : Set α) (ht : MeasurableSet t) : μ (s ∩ t) + μ (s \ t) = μ s

Alias of MeasureTheory.measure_inter_add_sdiff.

theorem MeasureTheory.measure_sdiff_add_inter {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {t : Set α} (s : Set α) (ht : MeasurableSet t) : μ (s \ t) + μ (s ∩ t) = μ s

@[deprecated MeasureTheory.measure_sdiff_add_inter (since := "2026-06-03")]

theorem MeasureTheory.measure_diff_add_inter {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {t : Set α} (s : Set α) (ht : MeasurableSet t) : μ (s \ t) + μ (s ∩ t) = μ s

Alias of MeasureTheory.measure_sdiff_add_inter.

theorem MeasureTheory.measure_sdiff_eq_top {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s t : Set α} (hs : μ s = ⊤) (ht : μ t ≠ ⊤) : μ (s \ t) = ⊤

@[deprecated MeasureTheory.measure_sdiff_eq_top (since := "2026-06-03")]

theorem MeasureTheory.measure_diff_eq_top {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s t : Set α} (hs : μ s = ⊤) (ht : μ t ≠ ⊤) : μ (s \ t) = ⊤

Alias of MeasureTheory.measure_sdiff_eq_top.

theorem MeasureTheory.measure_union_add_inter {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {t : Set α} (s : Set α) (ht : MeasurableSet t) : μ (s ∪ t) + μ (s ∩ t) = μ s + μ t

theorem MeasureTheory.measure_union_add_inter' {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s : Set α} (hs : MeasurableSet s) (t : Set α) : μ (s ∪ t) + μ (s ∩ t) = μ s + μ t

theorem MeasureTheory.measure_symmDiff_eq {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s t : Set α} (hs : NullMeasurableSet s μ) (ht : NullMeasurableSet t μ) : μ (symmDiff s t) = μ (s \ t) + μ (t \ s)

theorem MeasureTheory.measure_symmDiff_le {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} (s t u : Set α) : μ (symmDiff s u) ≤ μ (symmDiff s t) + μ (symmDiff t u)

theorem MeasureTheory.measure_symmDiff_eq_top {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s t : Set α} (hs : μ s ≠ ⊤) (ht : μ t = ⊤) : μ (symmDiff s t) = ⊤

theorem MeasureTheory.measure_add_measure_compl {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s : Set α} (h : MeasurableSet s) : μ s + μ sᶜ = μ Set.univ

theorem MeasureTheory.measure_biUnion₀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {s : Set β} {f : β → Set α} (hs : s.Countable) (hd : s.Pairwise (Function.onFun (AEDisjoint μ) f)) (h : ∀ b ∈ s, NullMeasurableSet (f b) μ) : μ (⋃ b ∈ s, f b) = ∑' (p : ↑s), μ (f ↑p)

theorem MeasureTheory.measure_biUnion {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {s : Set β} {f : β → Set α} (hs : s.Countable) (hd : s.PairwiseDisjoint f) (h : ∀ b ∈ s, MeasurableSet (f b)) : μ (⋃ b ∈ s, f b) = ∑' (p : ↑s), μ (f ↑p)

theorem MeasureTheory.measure_sUnion₀ {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {S : Set (Set α)} (hs : S.Countable) (hd : S.Pairwise (AEDisjoint μ)) (h : ∀ s ∈ S, NullMeasurableSet s μ) : μ (⋃₀ S) = ∑' (s : ↑S), μ ↑s

theorem MeasureTheory.measure_sUnion {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {S : Set (Set α)} (hs : S.Countable) (hd : S.Pairwise Disjoint) (h : ∀ s ∈ S, MeasurableSet s) : μ (⋃₀ S) = ∑' (s : ↑S), μ ↑s

theorem MeasureTheory.measure_biUnion_finset₀ {α : Type u_1} {ι : Type u_3} {m : MeasurableSpace α} {μ : Measure α} {s : Finset ι} {f : ι → Set α} (hd : (↑s).Pairwise (Function.onFun (AEDisjoint μ) f)) (hm : ∀ b ∈ s, NullMeasurableSet (f b) μ) : μ (⋃ b ∈ s, f b) = ∑ p ∈ s, μ (f p)

theorem MeasureTheory.measure_biUnion_finset {α : Type u_1} {ι : Type u_3} {m : MeasurableSpace α} {μ : Measure α} {s : Finset ι} {f : ι → Set α} (hd : (↑s).PairwiseDisjoint f) (hm : ∀ b ∈ s, MeasurableSet (f b)) : μ (⋃ b ∈ s, f b) = ∑ p ∈ s, μ (f p)

theorem MeasureTheory.tsum_meas_le_meas_iUnion_of_disjoint₀ {α : Type u_1} {ι : Type u_3} {m : MeasurableSpace α} (μ : Measure α) {As : ι → Set α} (As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ) (As_disj : Pairwise (Function.onFun (AEDisjoint μ) As)) : ∑' (i : ι), μ (As i) ≤ μ (⋃ (i : ι), As i)

The measure of an a.e. disjoint union (even uncountable) of null-measurable sets is at least the sum of the measures of the sets.

theorem MeasureTheory.tsum_meas_le_meas_iUnion_of_disjoint {α : Type u_1} {ι : Type u_3} {m : MeasurableSpace α} (μ : Measure α) {As : ι → Set α} (As_mble : ∀ (i : ι), MeasurableSet (As i)) (As_disj : Pairwise (Function.onFun Disjoint As)) : ∑' (i : ι), μ (As i) ≤ μ (⋃ (i : ι), As i)

The measure of a disjoint union (even uncountable) of measurable sets is at least the sum of the measures of the sets.

theorem MeasureTheory.tsum_measure_preimage_singleton {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {s : Set β} (hs : s.Countable) {f : α → β} (hf : ∀ y ∈ s, MeasurableSet (f ⁻¹' {y})) : ∑' (b : ↑s), μ (f ⁻¹' {↑b}) = μ (f ⁻¹' s)

If s is a countable set, then the measure of its preimage can be found as the sum of measures of the fibers f ⁻¹' {y}.

theorem MeasureTheory.measure_preimage_eq_zero_iff_of_countable {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {s : Set β} {f : α → β} (hs : s.Countable) : μ (f ⁻¹' s) = 0 ↔ ∀ x ∈ s, μ (f ⁻¹' {x}) = 0

theorem MeasureTheory.sum_measure_preimage_singleton {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} (s : Finset β) {f : α → β} (hf : ∀ y ∈ s, MeasurableSet (f ⁻¹' {y})) : ∑ b ∈ s, μ (f ⁻¹' {b}) = μ (f ⁻¹' ↑s)

If s is a Finset, then the measure of its preimage can be found as the sum of measures of the fibers f ⁻¹' {y}.

@[simp]

theorem MeasureTheory.sum_measure_singleton {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s : Finset α} [MeasurableSingletonClass α] : ∑ x ∈ s, μ {x} = μ ↑s

theorem MeasureTheory.measure_sdiff_null' {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s₁ s₂ : Set α} (h : μ (s₁ ∩ s₂) = 0) : μ (s₁ \ s₂) = μ s₁

@[deprecated MeasureTheory.measure_sdiff_null' (since := "2026-06-03")]

theorem MeasureTheory.measure_diff_null' {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s₁ s₂ : Set α} (h : μ (s₁ ∩ s₂) = 0) : μ (s₁ \ s₂) = μ s₁

Alias of MeasureTheory.measure_sdiff_null'.

theorem MeasureTheory.measure_add_sdiff {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s : Set α} (hs : NullMeasurableSet s μ) (t : Set α) : μ s + μ (t \ s) = μ (s ∪ t)

@[deprecated MeasureTheory.measure_add_sdiff (since := "2026-06-03")]

theorem MeasureTheory.measure_add_diff {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s : Set α} (hs : NullMeasurableSet s μ) (t : Set α) : μ s + μ (t \ s) = μ (s ∪ t)

Alias of MeasureTheory.measure_add_sdiff.

theorem MeasureTheory.measure_sdiff' {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {t : Set α} (s : Set α) (hm : NullMeasurableSet t μ) (h_fin : μ t ≠ ⊤) : μ (s \ t) = μ (s ∪ t) - μ t

@[deprecated MeasureTheory.measure_sdiff' (since := "2026-06-03")]

theorem MeasureTheory.measure_diff' {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {t : Set α} (s : Set α) (hm : NullMeasurableSet t μ) (h_fin : μ t ≠ ⊤) : μ (s \ t) = μ (s ∪ t) - μ t

Alias of MeasureTheory.measure_sdiff'.

theorem MeasureTheory.measure_sdiff {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s₁ s₂ : Set α} (h : s₂ ⊆ s₁) (h₂ : NullMeasurableSet s₂ μ) (h_fin : μ s₂ ≠ ⊤) : μ (s₁ \ s₂) = μ s₁ - μ s₂

@[deprecated MeasureTheory.measure_sdiff (since := "2026-06-03")]

theorem MeasureTheory.measure_diff {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s₁ s₂ : Set α} (h : s₂ ⊆ s₁) (h₂ : NullMeasurableSet s₂ μ) (h_fin : μ s₂ ≠ ⊤) : μ (s₁ \ s₂) = μ s₁ - μ s₂

Alias of MeasureTheory.measure_sdiff.

theorem MeasureTheory.le_measure_sdiff {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s₁ s₂ : Set α} : μ s₁ - μ s₂ ≤ μ (s₁ \ s₂)

@[deprecated MeasureTheory.le_measure_sdiff (since := "2026-06-03")]

theorem MeasureTheory.le_measure_diff {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s₁ s₂ : Set α} : μ s₁ - μ s₂ ≤ μ (s₁ \ s₂)

Alias of MeasureTheory.le_measure_sdiff.

theorem MeasureTheory.le_measure_symmDiff {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s₁ s₂ : Set α} : μ s₁ - μ s₂ ≤ μ (symmDiff s₁ s₂)

theorem MeasureTheory.measure_eq_top_iff_of_symmDiff {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s t : Set α} (hμst : μ (symmDiff s t) ≠ ⊤) : μ s = ⊤ ↔ μ t = ⊤

If the measure of the symmetric difference of two sets is finite, then one has infinite measure if and only if the other one does.

theorem MeasureTheory.measure_ne_top_iff_of_symmDiff {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s t : Set α} (hμst : μ (symmDiff s t) ≠ ⊤) : μ s ≠ ⊤ ↔ μ t ≠ ⊤

If the measure of the symmetric difference of two sets is finite, then one has finite measure if and only if the other one does.

theorem MeasureTheory.measure_sdiff_lt_of_lt_add {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s t : Set α} (hs : NullMeasurableSet s μ) (hst : s ⊆ t) (hs' : μ s ≠ ⊤) {ε : ENNReal} (h : μ t < μ s + ε) : μ (t \ s) < ε

@[deprecated MeasureTheory.measure_sdiff_lt_of_lt_add (since := "2026-06-03")]

theorem MeasureTheory.measure_diff_lt_of_lt_add {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s t : Set α} (hs : NullMeasurableSet s μ) (hst : s ⊆ t) (hs' : μ s ≠ ⊤) {ε : ENNReal} (h : μ t < μ s + ε) : μ (t \ s) < ε

Alias of MeasureTheory.measure_sdiff_lt_of_lt_add.

theorem MeasureTheory.measure_sdiff_le_iff_le_add {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s t : Set α} (hs : NullMeasurableSet s μ) (hst : s ⊆ t) (hs' : μ s ≠ ⊤) {ε : ENNReal} : μ (t \ s) ≤ ε ↔ μ t ≤ μ s + ε

@[deprecated MeasureTheory.measure_sdiff_le_iff_le_add (since := "2026-06-03")]

theorem MeasureTheory.measure_diff_le_iff_le_add {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s t : Set α} (hs : NullMeasurableSet s μ) (hst : s ⊆ t) (hs' : μ s ≠ ⊤) {ε : ENNReal} : μ (t \ s) ≤ ε ↔ μ t ≤ μ s + ε

Alias of MeasureTheory.measure_sdiff_le_iff_le_add.

theorem MeasureTheory.measure_eq_measure_of_null_sdiff {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s t : Set α} (hst : s ⊆ t) (h_nullsdiff : μ (t \ s) = 0) : μ s = μ t

@[deprecated MeasureTheory.measure_eq_measure_of_null_sdiff (since := "2026-06-03")]

theorem MeasureTheory.measure_eq_measure_of_null_diff {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s t : Set α} (hst : s ⊆ t) (h_nullsdiff : μ (t \ s) = 0) : μ s = μ t

Alias of MeasureTheory.measure_eq_measure_of_null_sdiff.

theorem MeasureTheory.measure_eq_measure_of_between_null_sdiff {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s₁ s₂ s₃ : Set α} (h12 : s₁ ⊆ s₂) (h23 : s₂ ⊆ s₃) (h_nullsdiff : μ (s₃ \ s₁) = 0) : μ s₁ = μ s₂ ∧ μ s₂ = μ s₃

@[deprecated MeasureTheory.measure_eq_measure_of_between_null_sdiff (since := "2026-06-03")]

theorem MeasureTheory.measure_eq_measure_of_between_null_diff {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s₁ s₂ s₃ : Set α} (h12 : s₁ ⊆ s₂) (h23 : s₂ ⊆ s₃) (h_nullsdiff : μ (s₃ \ s₁) = 0) : μ s₁ = μ s₂ ∧ μ s₂ = μ s₃

Alias of MeasureTheory.measure_eq_measure_of_between_null_sdiff.

theorem MeasureTheory.measure_eq_measure_smaller_of_between_null_sdiff {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s₁ s₂ s₃ : Set α} (h12 : s₁ ⊆ s₂) (h23 : s₂ ⊆ s₃) (h_nullsdiff : μ (s₃ \ s₁) = 0) : μ s₁ = μ s₂

@[deprecated MeasureTheory.measure_eq_measure_smaller_of_between_null_sdiff (since := "2026-06-03")]

theorem MeasureTheory.measure_eq_measure_smaller_of_between_null_diff {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s₁ s₂ s₃ : Set α} (h12 : s₁ ⊆ s₂) (h23 : s₂ ⊆ s₃) (h_nullsdiff : μ (s₃ \ s₁) = 0) : μ s₁ = μ s₂

Alias of MeasureTheory.measure_eq_measure_smaller_of_between_null_sdiff.

theorem MeasureTheory.measure_eq_measure_larger_of_between_null_sdiff {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s₁ s₂ s₃ : Set α} (h12 : s₁ ⊆ s₂) (h23 : s₂ ⊆ s₃) (h_nullsdiff : μ (s₃ \ s₁) = 0) : μ s₂ = μ s₃

@[deprecated MeasureTheory.measure_eq_measure_larger_of_between_null_sdiff (since := "2026-06-03")]

theorem MeasureTheory.measure_eq_measure_larger_of_between_null_diff {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s₁ s₂ s₃ : Set α} (h12 : s₁ ⊆ s₂) (h23 : s₂ ⊆ s₃) (h_nullsdiff : μ (s₃ \ s₁) = 0) : μ s₂ = μ s₃

Alias of MeasureTheory.measure_eq_measure_larger_of_between_null_sdiff.

theorem MeasureTheory.measure_compl₀ {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s : Set α} (h : NullMeasurableSet s μ) (hs : μ s ≠ ⊤) : μ sᶜ = μ Set.univ - μ s

theorem MeasureTheory.measure_compl {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s : Set α} (h₁ : MeasurableSet s) (h_fin : μ s ≠ ⊤) : μ sᶜ = μ Set.univ - μ s

theorem MeasureTheory.measure_inter_conull' {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s t : Set α} (ht : μ (s \ t) = 0) : μ (s ∩ t) = μ s

theorem MeasureTheory.measure_inter_conull {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s t : Set α} (ht : μ tᶜ = 0) : μ (s ∩ t) = μ s

@[simp]

theorem MeasureTheory.union_ae_eq_left_iff_ae_subset {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s t : Set α} : s ∪ t =ᵐ[μ] s ↔ t ≤ᵐ[μ] s

@[simp]

theorem MeasureTheory.union_ae_eq_right_iff_ae_subset {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s t : Set α} : s ∪ t =ᵐ[μ] t ↔ s ≤ᵐ[μ] t

theorem MeasureTheory.ae_eq_of_ae_subset_of_measure_ge {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s t : Set α} (h₁ : s ≤ᵐ[μ] t) (h₂ : μ t ≤ μ s) (hsm : NullMeasurableSet s μ) (ht : μ t ≠ ⊤) : s =ᵐ[μ] t

theorem MeasureTheory.ae_eq_of_subset_of_measure_ge {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s t : Set α} (h₁ : s ⊆ t) (h₂ : μ t ≤ μ s) (hsm : NullMeasurableSet s μ) (ht : μ t ≠ ⊤) : s =ᵐ[μ] t

If s ⊆ t, μ t ≤ μ s, μ t ≠ ∞, and s is measurable, then s =ᵐ[μ] t.

theorem MeasureTheory.measure_iUnion_congr_of_subset {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ι : Sort u_4} [Countable ι] {s t : ι → Set α} (hsub : ∀ (i : ι), s i ⊆ t i) (h_le : ∀ (i : ι), μ (t i) ≤ μ (s i)) : μ (⋃ (i : ι), s i) = μ (⋃ (i : ι), t i)

theorem MeasureTheory.measure_union_congr_of_subset {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s₁ s₂ t₁ t₂ : Set α} (hs : s₁ ⊆ s₂) (hsμ : μ s₂ ≤ μ s₁) (ht : t₁ ⊆ t₂) (htμ : μ t₂ ≤ μ t₁) : μ (s₁ ∪ t₁) = μ (s₂ ∪ t₂)

@[simp]

theorem MeasureTheory.measure_iUnion_toMeasurable {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ι : Sort u_4} [Countable ι] (s : ι → Set α) : μ (⋃ (i : ι), toMeasurable μ (s i)) = μ (⋃ (i : ι), s i)

theorem MeasureTheory.measure_biUnion_toMeasurable {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {I : Set β} (hc : I.Countable) (s : β → Set α) : μ (⋃ b ∈ I, toMeasurable μ (s b)) = μ (⋃ b ∈ I, s b)

@[simp]

theorem MeasureTheory.measure_toMeasurable_union {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s t : Set α} : μ (toMeasurable μ s ∪ t) = μ (s ∪ t)

@[simp]

theorem MeasureTheory.measure_union_toMeasurable {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s t : Set α} : μ (s ∪ toMeasurable μ t) = μ (s ∪ t)

theorem MeasureTheory.sum_measure_le_measure_univ {α : Type u_1} {ι : Type u_3} {m : MeasurableSpace α} {μ : Measure α} {s : Finset ι} {t : ι → Set α} (h : ∀ i ∈ s, NullMeasurableSet (t i) μ) (H : (↑s).Pairwise (Function.onFun (AEDisjoint μ) t)) : ∑ i ∈ s, μ (t i) ≤ μ Set.univ

theorem MeasureTheory.tsum_measure_le_measure_univ {α : Type u_1} {ι : Type u_3} {m : MeasurableSpace α} {μ : Measure α} {s : ι → Set α} (hs : ∀ (i : ι), NullMeasurableSet (s i) μ) (H : Pairwise (Function.onFun (AEDisjoint μ) s)) : ∑' (i : ι), μ (s i) ≤ μ Set.univ

theorem MeasureTheory.exists_nonempty_inter_of_measure_univ_lt_tsum_measure {α : Type u_1} {ι : Type u_3} {m : MeasurableSpace α} (μ : Measure α) {s : ι → Set α} (hs : ∀ (i : ι), NullMeasurableSet (s i) μ) (H : μ Set.univ < ∑' (i : ι), μ (s i)) : ∃ (i : ι) (j : ι), i ≠ j ∧ (s i ∩ s j).Nonempty

Pigeonhole principle for measure spaces: if ∑' i, μ (s i) > μ univ, then one of the intersections s i ∩ s j is not empty.

theorem MeasureTheory.exists_nonempty_inter_of_measure_univ_lt_sum_measure {α : Type u_1} {ι : Type u_3} {m : MeasurableSpace α} (μ : Measure α) {s : Finset ι} {t : ι → Set α} (h : ∀ i ∈ s, NullMeasurableSet (t i) μ) (H : μ Set.univ < ∑ i ∈ s, μ (t i)) : ∃ i ∈ s, ∃ j ∈ s, ∃ (_ : i ≠ j), (t i ∩ t j).Nonempty

Pigeonhole principle for measure spaces: if s is a Finset and ∑ i ∈ s, μ (t i) > μ univ, then one of the intersections t i ∩ t j is not empty.

theorem MeasureTheory.nonempty_inter_of_measure_lt_add {α : Type u_1} {m : MeasurableSpace α} {s t u : Set α} (μ : Measure α) (ht : MeasurableSet t) (h's : s ⊆ u) (h't : t ⊆ u) (h : μ u < μ s + μ t) : (s ∩ t).Nonempty

If two sets s and t are included in a set u, and μ s + μ t > μ u, then s intersects t. Version assuming that t is measurable.

theorem MeasureTheory.nonempty_inter_of_measure_lt_add' {α : Type u_1} {m : MeasurableSpace α} {s t u : Set α} (μ : Measure α) (hs : MeasurableSet s) (h's : s ⊆ u) (h't : t ⊆ u) (h : μ u < μ s + μ t) : (s ∩ t).Nonempty

If two sets s and t are included in a set u, and μ s + μ t > μ u, then s intersects t. Version assuming that s is measurable.

theorem MeasureTheory.Measure.measure_inter_eq_of_measure_eq {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s t u : Set α} (hs : MeasurableSet s) (h : μ t = μ u) (htu : t ⊆ u) (ht_ne_top : μ t ≠ ⊤) : μ (t ∩ s) = μ (u ∩ s)

If u is a superset of t with the same (finite) measure (both sets possibly non-measurable), then for any measurable set s one also has μ (t ∩ s) = μ (u ∩ s).

theorem MeasureTheory.Measure.measure_inter_eq_of_ae {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s t : Set α} (h : ∀ᵐ (a : α) ∂μ, a ∈ t) : μ (t ∩ s) = μ s

theorem MeasureTheory.Measure.measure_toMeasurable_inter {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s t : Set α} (hs : MeasurableSet s) (ht : μ t ≠ ⊤) : μ (toMeasurable μ t ∩ s) = μ (t ∩ s)

The measurable superset toMeasurable μ t of t (which has the same measure as t) satisfies, for any measurable set s, the equality μ (toMeasurable μ t ∩ s) = μ (u ∩ s). Here, we require that the measure of t is finite. The conclusion holds without this assumption when the measure is s-finite (for example when it is σ-finite), see measure_toMeasurable_inter_of_sFinite.

theorem MeasureTheory.measure_if {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {s : Set α} {x : β} {t : Set β} [Decidable (x ∈ t)] : μ (if x ∈ t then s else ∅) = t.indicator (fun (x : β) => μ s) x

theorem MeasureTheory.ext_of_measurableAtoms {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} [Countable α] {ν : Measure α} (h : ∀ (x : α), μ (measurableAtom x) = ν (measurableAtom x)) : μ = ν

On a countable space, two measures are equal if they agree on measurable atoms.