Documentation

Mathlib.MeasureTheory.Measure.MeasureSpace

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. 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, a 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.

Measures on α form a complete lattice, and are closed under scalar multiplication with ℝ≥0∞.

Given a measure, the null sets are the sets where μ s = 0, where μ denotes the corresponding outer measure (so s might not be measurable). We can then define the completion of μ as the measure on the least σ-algebra that also contains all null sets, by defining the measure to be 0 on the null sets.

Main statements #

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:

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

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

References #

Tags #

measure, almost everywhere, measure space, completion, null set, null measurable set

instance MeasureTheory.ae_isMeasurablyGenerated {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} :
(MeasureTheory.ae μ).IsMeasurablyGenerated
Equations
  • =
theorem MeasureTheory.ae_uIoc_iff {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [LinearOrder α] {a : α} {b : α} {P : αProp} :
(∀ᵐ (x : α) ∂μ, x Ι a bP x) (∀ᵐ (x : α) ∂μ, x Set.Ioc a bP x) ∀ᵐ (x : α) ∂μ, x Set.Ioc b aP x

See also MeasureTheory.ae_restrict_uIoc_iff.

theorem MeasureTheory.measure_union {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ : Set α} {s₂ : Set α} (hd : Disjoint s₁ s₂) (h : MeasurableSet s₂) :
μ (s₁ s₂) = μ s₁ + μ s₂
theorem MeasureTheory.measure_union' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ : Set α} {s₂ : Set α} (hd : Disjoint s₁ s₂) (h : MeasurableSet s₁) :
μ (s₁ s₂) = μ s₁ + μ s₂
theorem MeasureTheory.measure_inter_add_diff {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set α} (s : Set α) (ht : MeasurableSet t) :
μ (s t) + μ (s \ t) = μ s
theorem MeasureTheory.measure_diff_add_inter {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set α} (s : Set α) (ht : MeasurableSet t) :
μ (s \ t) + μ (s t) = μ s
theorem MeasureTheory.measure_union_add_inter {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.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 α} {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) (t : Set α) :
μ (s t) + μ (s t) = μ s + μ t
theorem MeasureTheory.measure_symmDiff_eq {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (hs : MeasureTheory.NullMeasurableSet s μ) (ht : MeasureTheory.NullMeasurableSet t μ) :
μ (symmDiff s t) = μ (s \ t) + μ (t \ s)
theorem MeasureTheory.measure_symmDiff_le {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Set α) (t : Set α) (u : Set α) :
μ (symmDiff s u) μ (symmDiff s t) + μ (symmDiff t u)
theorem MeasureTheory.measure_add_measure_compl {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (h : MeasurableSet s) :
μ s + μ s = μ Set.univ
theorem MeasureTheory.measure_biUnion₀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set β} {f : βSet α} (hs : s.Countable) (hd : s.Pairwise (MeasureTheory.AEDisjoint μ on f)) (h : bs, MeasureTheory.NullMeasurableSet (f b) μ) :
μ (⋃ bs, f b) = ∑' (p : s), μ (f p)
theorem MeasureTheory.measure_biUnion {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set β} {f : βSet α} (hs : s.Countable) (hd : s.PairwiseDisjoint f) (h : bs, MeasurableSet (f b)) :
μ (⋃ bs, f b) = ∑' (p : s), μ (f p)
theorem MeasureTheory.measure_sUnion₀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {S : Set (Set α)} (hs : S.Countable) (hd : S.Pairwise (MeasureTheory.AEDisjoint μ)) (h : sS, MeasureTheory.NullMeasurableSet s μ) :
μ (⋃₀ S) = ∑' (s : S), μ s
theorem MeasureTheory.measure_sUnion {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {S : Set (Set α)} (hs : S.Countable) (hd : S.Pairwise Disjoint) (h : sS, MeasurableSet s) :
μ (⋃₀ S) = ∑' (s : S), μ s
theorem MeasureTheory.measure_biUnion_finset₀ {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Finset ι} {f : ιSet α} (hd : (↑s).Pairwise (MeasureTheory.AEDisjoint μ on f)) (hm : bs, MeasureTheory.NullMeasurableSet (f b) μ) :
μ (⋃ bs, f b) = ps, μ (f p)
theorem MeasureTheory.measure_biUnion_finset {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Finset ι} {f : ιSet α} (hd : (↑s).PairwiseDisjoint f) (hm : bs, MeasurableSet (f b)) :
μ (⋃ bs, f b) = ps, μ (f p)
theorem MeasureTheory.tsum_meas_le_meas_iUnion_of_disjoint₀ {α : Type u_1} {ι : Type u_8} :
∀ {x : MeasurableSpace α} (μ : MeasureTheory.Measure α) {As : ιSet α}, (∀ (i : ι), MeasureTheory.NullMeasurableSet (As i) μ)Pairwise (MeasureTheory.AEDisjoint μ on 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_8} :
∀ {x : MeasurableSpace α} (μ : MeasureTheory.Measure α) {As : ιSet α}, (∀ (i : ι), MeasurableSet (As i))Pairwise (Disjoint on 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 α} {μ : MeasureTheory.Measure α} {s : Set β} (hs : s.Countable) {f : αβ} (hf : ys, 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 α} {μ : MeasureTheory.Measure α} {s : Set β} {f : αβ} (hs : s.Countable) :
μ (f ⁻¹' s) = 0 xs, μ (f ⁻¹' {x}) = 0
theorem MeasureTheory.sum_measure_preimage_singleton {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Finset β) {f : αβ} (hf : ys, MeasurableSet (f ⁻¹' {y})) :
bs, μ (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}.

theorem MeasureTheory.measure_diff_null' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ : Set α} {s₂ : Set α} (h : μ (s₁ s₂) = 0) :
μ (s₁ \ s₂) = μ s₁
theorem MeasureTheory.measure_add_diff {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasureTheory.NullMeasurableSet s μ) (t : Set α) :
μ s + μ (t \ s) = μ (s t)
theorem MeasureTheory.measure_diff' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set α} (s : Set α) (hm : MeasureTheory.NullMeasurableSet t μ) (h_fin : μ t ) :
μ (s \ t) = μ (s t) - μ t
theorem MeasureTheory.measure_diff {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ : Set α} {s₂ : Set α} (h : s₂ s₁) (h₂ : MeasureTheory.NullMeasurableSet s₂ μ) (h_fin : μ s₂ ) :
μ (s₁ \ s₂) = μ s₁ - μ s₂
theorem MeasureTheory.le_measure_diff {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ : Set α} {s₂ : Set α} :
μ s₁ - μ s₂ μ (s₁ \ s₂)
theorem MeasureTheory.measure_eq_top_iff_of_symmDiff {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {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 α} {μ : MeasureTheory.Measure α} {s : Set α} {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_diff_lt_of_lt_add {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (hs : MeasureTheory.NullMeasurableSet s μ) (hst : s t) (hs' : μ s ) {ε : ENNReal} (h : μ t < μ s + ε) :
μ (t \ s) < ε
theorem MeasureTheory.measure_diff_le_iff_le_add {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (hs : MeasureTheory.NullMeasurableSet s μ) (hst : s t) (hs' : μ s ) {ε : ENNReal} :
μ (t \ s) ε μ t μ s + ε
theorem MeasureTheory.measure_eq_measure_of_null_diff {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (hst : s t) (h_nulldiff : μ (t \ s) = 0) :
μ s = μ t
theorem MeasureTheory.measure_eq_measure_of_between_null_diff {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ : Set α} {s₂ : Set α} {s₃ : Set α} (h12 : s₁ s₂) (h23 : s₂ s₃) (h_nulldiff : μ (s₃ \ s₁) = 0) :
μ s₁ = μ s₂ μ s₂ = μ s₃
theorem MeasureTheory.measure_eq_measure_smaller_of_between_null_diff {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ : Set α} {s₂ : Set α} {s₃ : Set α} (h12 : s₁ s₂) (h23 : s₂ s₃) (h_nulldiff : μ (s₃ \ s₁) = 0) :
μ s₁ = μ s₂
theorem MeasureTheory.measure_eq_measure_larger_of_between_null_diff {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ : Set α} {s₂ : Set α} {s₃ : Set α} (h12 : s₁ s₂) (h23 : s₂ s₃) (h_nulldiff : μ (s₃ \ s₁) = 0) :
μ s₂ = μ s₃
theorem MeasureTheory.measure_compl₀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (h : MeasureTheory.NullMeasurableSet s μ) (hs : μ s ) :
μ s = μ Set.univ - μ s
theorem MeasureTheory.measure_compl {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (h₁ : MeasurableSet s) (h_fin : μ s ) :
μ s = μ Set.univ - μ s
theorem MeasureTheory.measure_inter_conull' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (ht : μ (s \ t) = 0) :
μ (s t) = μ s
theorem MeasureTheory.measure_inter_conull {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (ht : μ t = 0) :
μ (s t) = μ s
@[simp]
theorem MeasureTheory.union_ae_eq_left_iff_ae_subset {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} :
s t =ᵐ[μ] s t ≤ᵐ[μ] s
@[simp]
theorem MeasureTheory.union_ae_eq_right_iff_ae_subset {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} :
s t =ᵐ[μ] t s ≤ᵐ[μ] t
theorem MeasureTheory.ae_eq_of_ae_subset_of_measure_ge {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (h₁ : s ≤ᵐ[μ] t) (h₂ : μ t μ s) (hsm : MeasureTheory.NullMeasurableSet s μ) (ht : μ t ) :
s =ᵐ[μ] t
theorem MeasureTheory.ae_eq_of_subset_of_measure_ge {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (h₁ : s t) (h₂ : μ t μ s) (hsm : MeasureTheory.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 α} {μ : MeasureTheory.Measure α} {ι : Sort u_8} [Countable ι] {s : ιSet α} {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 α} {μ : MeasureTheory.Measure α} {s₁ : Set α} {s₂ : Set α} {t₁ : Set α} {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 α} {μ : MeasureTheory.Measure α} {ι : Sort u_8} [Countable ι] (s : ιSet α) :
μ (⋃ (i : ι), MeasureTheory.toMeasurable μ (s i)) = μ (⋃ (i : ι), s i)
theorem MeasureTheory.measure_biUnion_toMeasurable {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {I : Set β} (hc : I.Countable) (s : βSet α) :
μ (⋃ bI, MeasureTheory.toMeasurable μ (s b)) = μ (⋃ bI, s b)
@[simp]
theorem MeasureTheory.measure_toMeasurable_union {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} :
μ (MeasureTheory.toMeasurable μ s t) = μ (s t)
@[simp]
theorem MeasureTheory.measure_union_toMeasurable {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} :
μ (s MeasureTheory.toMeasurable μ t) = μ (s t)
theorem MeasureTheory.sum_measure_le_measure_univ {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Finset ι} {t : ιSet α} (h : is, MeasureTheory.NullMeasurableSet (t i) μ) (H : (↑s).Pairwise (MeasureTheory.AEDisjoint μ on t)) :
is, μ (t i) μ Set.univ
theorem MeasureTheory.tsum_measure_le_measure_univ {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : ιSet α} (hs : ∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ) (H : Pairwise (MeasureTheory.AEDisjoint μ on s)) :
∑' (i : ι), μ (s i) μ Set.univ
theorem MeasureTheory.exists_nonempty_inter_of_measure_univ_lt_tsum_measure {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) {s : ιSet α} (hs : ∀ (i : ι), MeasureTheory.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_5} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) {s : Finset ι} {t : ιSet α} (h : is, MeasureTheory.NullMeasurableSet (t i) μ) (H : μ Set.univ < is, μ (t i)) :
is, js, ∃ (_ : 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 α} (μ : MeasureTheory.Measure α) {s : Set α} {t : Set α} {u : Set α} (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 α} (μ : MeasureTheory.Measure α) {s : Set α} {t : Set α} {u : Set α} (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 Directed.measure_iUnion {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable ι] {s : ιSet α} (hd : Directed (fun (x1 x2 : Set α) => x1 x2) s) :
μ (⋃ (i : ι), s i) = ⨆ (i : ι), μ (s i)

Continuity from below: the measure of the union of a directed sequence of (not necessarily measurable) sets is the supremum of the measures.

@[deprecated Directed.measure_iUnion]
theorem MeasureTheory.measure_iUnion_eq_iSup {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable ι] {s : ιSet α} (hd : Directed (fun (x1 x2 : Set α) => x1 x2) s) :
μ (⋃ (i : ι), s i) = ⨆ (i : ι), μ (s i)

Alias of Directed.measure_iUnion.


Continuity from below: the measure of the union of a directed sequence of (not necessarily measurable) sets is the supremum of the measures.

theorem Monotone.measure_iUnion {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Preorder ι] [IsDirected ι fun (x1 x2 : ι) => x1 x2] [Filter.atTop.IsCountablyGenerated] {s : ιSet α} (hs : Monotone s) :
μ (⋃ (i : ι), s i) = ⨆ (i : ι), μ (s i)

Continuity from below: the measure of the union of a monotone family of sets is equal to the supremum of their measures. The theorem assumes that the atTop filter on the index set is countably generated, so it works for a family indexed by a countable type, as well as .

theorem Antitone.measure_iUnion {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Preorder ι] [IsDirected ι fun (x1 x2 : ι) => x1 x2] [Filter.atBot.IsCountablyGenerated] {s : ιSet α} (hs : Antitone s) :
μ (⋃ (i : ι), s i) = ⨆ (i : ι), μ (s i)
theorem MeasureTheory.measure_iUnion_eq_iSup_accumulate {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Preorder ι] [IsDirected ι fun (x1 x2 : ι) => x1 x2] [Filter.atTop.IsCountablyGenerated] {f : ιSet α} :
μ (⋃ (i : ι), f i) = ⨆ (i : ι), μ (Set.Accumulate f i)

Continuity from below: the measure of the union of a sequence of (not necessarily measurable) sets is the supremum of the measures of the partial unions.

@[deprecated MeasureTheory.measure_iUnion_eq_iSup_accumulate]
theorem MeasureTheory.measure_iUnion_eq_iSup' {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Preorder ι] [IsDirected ι fun (x1 x2 : ι) => x1 x2] [Filter.atTop.IsCountablyGenerated] {f : ιSet α} :
μ (⋃ (i : ι), f i) = ⨆ (i : ι), μ (Set.Accumulate f i)

Alias of MeasureTheory.measure_iUnion_eq_iSup_accumulate.


Continuity from below: the measure of the union of a sequence of (not necessarily measurable) sets is the supremum of the measures of the partial unions.

theorem MeasureTheory.measure_biUnion_eq_iSup {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : ιSet α} {t : Set ι} (ht : t.Countable) (hd : DirectedOn ((fun (x1 x2 : Set α) => x1 x2) on s) t) :
μ (⋃ it, s i) = it, μ (s i)
theorem MeasureTheory.measure_iInter_eq_iInf {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable ι] {s : ιSet α} (h : ∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ) (hd : Directed (fun (x1 x2 : Set α) => x1 x2) s) (hfin : ∃ (i : ι), μ (s i) ) :
μ (⋂ (i : ι), s i) = ⨅ (i : ι), μ (s i)

Continuity from above: the measure of the intersection of a decreasing sequence of measurable sets is the infimum of the measures.

theorem MeasureTheory.measure_iInter_eq_iInf' {α : Type u_8} {ι : Type u_9} :
∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : Countable ι] [inst : Preorder ι] [inst_1 : IsDirected ι fun (x1 x2 : ι) => x1 x2] {f : ιSet α}, (∀ (i : ι), MeasureTheory.NullMeasurableSet (f i) μ)(∃ (i : ι), μ (f i) )μ (⋂ (i : ι), f i) = ⨅ (i : ι), μ (⋂ (j : ι), ⋂ (_ : j i), f j)

Continuity from above: the measure of the intersection of a sequence of measurable sets is the infimum of the measures of the partial intersections.

theorem MeasureTheory.tendsto_measure_iUnion_atTop {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Preorder ι] [Filter.atTop.IsCountablyGenerated] {s : ιSet α} (hm : Monotone s) :
Filter.Tendsto (μ s) Filter.atTop (nhds (μ (⋃ (n : ι), s n)))

Continuity from below: the measure of the union of an increasing sequence of (not necessarily measurable) sets is the limit of the measures.

@[deprecated MeasureTheory.tendsto_measure_iUnion_atTop]
theorem MeasureTheory.tendsto_measure_iUnion {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Preorder ι] [Filter.atTop.IsCountablyGenerated] {s : ιSet α} (hm : Monotone s) :
Filter.Tendsto (μ s) Filter.atTop (nhds (μ (⋃ (n : ι), s n)))

Alias of MeasureTheory.tendsto_measure_iUnion_atTop.


Continuity from below: the measure of the union of an increasing sequence of (not necessarily measurable) sets is the limit of the measures.

theorem MeasureTheory.tendsto_measure_iUnion_atBot {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Preorder ι] [Filter.atBot.IsCountablyGenerated] {s : ιSet α} (hm : Antitone s) :
Filter.Tendsto (μ s) Filter.atBot (nhds (μ (⋃ (n : ι), s n)))
theorem MeasureTheory.tendsto_measure_iUnion_accumulate {α : Type u_8} {ι : Type u_9} [Preorder ι] [Filter.atTop.IsCountablyGenerated] :
∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ιSet α}, Filter.Tendsto (fun (i : ι) => μ (Set.Accumulate f i)) Filter.atTop (nhds (μ (⋃ (i : ι), f i)))

Continuity from below: the measure of the union of a sequence of (not necessarily measurable) sets is the limit of the measures of the partial unions.

@[deprecated MeasureTheory.tendsto_measure_iUnion_accumulate]
theorem MeasureTheory.tendsto_measure_iUnion' {α : Type u_8} {ι : Type u_9} [Preorder ι] [Filter.atTop.IsCountablyGenerated] :
∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ιSet α}, Filter.Tendsto (fun (i : ι) => μ (Set.Accumulate f i)) Filter.atTop (nhds (μ (⋃ (i : ι), f i)))

Alias of MeasureTheory.tendsto_measure_iUnion_accumulate.


Continuity from below: the measure of the union of a sequence of (not necessarily measurable) sets is the limit of the measures of the partial unions.

theorem MeasureTheory.tendsto_measure_iInter {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable ι] [Preorder ι] {s : ιSet α} (hs : ∀ (n : ι), MeasureTheory.NullMeasurableSet (s n) μ) (hm : Antitone s) (hf : ∃ (i : ι), μ (s i) ) :
Filter.Tendsto (μ s) Filter.atTop (nhds (μ (⋂ (n : ι), s n)))

Continuity from above: the measure of the intersection of a decreasing sequence of measurable sets is the limit of the measures.

theorem MeasureTheory.tendsto_measure_iInter' {α : Type u_8} {ι : Type u_9} :
∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : Countable ι] [inst : Preorder ι] [inst_1 : IsDirected ι fun (x1 x2 : ι) => x1 x2] {f : ιSet α}, (∀ (i : ι), MeasureTheory.NullMeasurableSet (f i) μ)(∃ (i : ι), μ (f i) )Filter.Tendsto (fun (i : ι) => μ (⋂ j{j : ι | j i}, f j)) Filter.atTop (nhds (μ (⋂ (i : ι), f i)))

Continuity from above: the measure of the intersection of a sequence of measurable sets such that one has finite measure is the limit of the measures of the partial intersections.

theorem MeasureTheory.tendsto_measure_biInter_gt {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Type u_8} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [DenselyOrdered ι] [FirstCountableTopology ι] {s : ιSet α} {a : ι} (hs : r > a, MeasureTheory.NullMeasurableSet (s r) μ) (hm : ∀ (i j : ι), a < ii js i s j) (hf : r > a, μ (s r) ) :
Filter.Tendsto (μ s) (nhdsWithin a (Set.Ioi a)) (nhds (μ (⋂ (r : ι), ⋂ (_ : r > a), s r)))

The measure of the intersection of a decreasing sequence of measurable sets indexed by a linear order with first countable topology is the limit of the measures.

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

Obtain a measure by giving an outer measure where all sets in the σ-algebra are Carathéodory measurable.

Equations
Instances For
    theorem MeasureTheory.le_toOuterMeasure_caratheodory {α : Type u_1} [ms : MeasurableSpace α] (μ : MeasureTheory.Measure α) :
    ms μ.caratheodory
    @[simp]
    theorem MeasureTheory.toMeasure_toOuterMeasure {α : Type u_1} [ms : MeasurableSpace α] (m : MeasureTheory.OuterMeasure α) (h : ms m.caratheodory) :
    (m.toMeasure h).toOuterMeasure = m.trim
    @[simp]
    theorem MeasureTheory.toMeasure_apply {α : Type u_1} [ms : MeasurableSpace α] (m : MeasureTheory.OuterMeasure α) (h : ms m.caratheodory) {s : Set α} (hs : MeasurableSet s) :
    (m.toMeasure h) s = m s
    theorem MeasureTheory.le_toMeasure_apply {α : Type u_1} [ms : MeasurableSpace α] (m : MeasureTheory.OuterMeasure α) (h : ms m.caratheodory) (s : Set α) :
    m s (m.toMeasure h) s
    theorem MeasureTheory.toMeasure_apply₀ {α : Type u_1} [ms : MeasurableSpace α] (m : MeasureTheory.OuterMeasure α) (h : ms m.caratheodory) {s : Set α} (hs : MeasureTheory.NullMeasurableSet s (m.toMeasure h)) :
    (m.toMeasure h) s = m s
    @[simp]
    theorem MeasureTheory.toOuterMeasure_toMeasure {α : Type u_1} [ms : MeasurableSpace α] {μ : MeasureTheory.Measure α} :
    μ.toMeasure = μ
    @[simp]
    theorem MeasureTheory.Measure.measure_inter_eq_of_measure_eq {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} {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_toMeasurable_inter {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (hs : MeasurableSet s) (ht : μ t ) :
    μ (MeasureTheory.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.

    The ℝ≥0∞-module of measures #

    Equations
    • MeasureTheory.Measure.instZero = { zero := { toOuterMeasure := 0, m_iUnion := , trim_le := } }
    @[simp]
    theorem MeasureTheory.Measure.coe_zero {α : Type u_1} {_m : MeasurableSpace α} :
    0 = 0
    theorem MeasureTheory.Measure.apply_eq_zero_of_isEmpty {α : Type u_1} [IsEmpty α] :
    ∀ {x : MeasurableSpace α} (μ : MeasureTheory.Measure α) (s : Set α), μ s = 0
    Equations
    • MeasureTheory.Measure.instInhabited = { default := 0 }
    Equations
    • MeasureTheory.Measure.instAdd = { add := fun (μ₁ μ₂ : MeasureTheory.Measure α) => { toOuterMeasure := μ₁.toOuterMeasure + μ₂.toOuterMeasure, m_iUnion := , trim_le := } }
    @[simp]
    theorem MeasureTheory.Measure.add_toOuterMeasure {α : Type u_1} {_m : MeasurableSpace α} (μ₁ : MeasureTheory.Measure α) (μ₂ : MeasureTheory.Measure α) :
    (μ₁ + μ₂).toOuterMeasure = μ₁.toOuterMeasure + μ₂.toOuterMeasure
    @[simp]
    theorem MeasureTheory.Measure.coe_add {α : Type u_1} {_m : MeasurableSpace α} (μ₁ : MeasureTheory.Measure α) (μ₂ : MeasureTheory.Measure α) :
    (μ₁ + μ₂) = μ₁ + μ₂
    theorem MeasureTheory.Measure.add_apply {α : Type u_1} {_m : MeasurableSpace α} (μ₁ : MeasureTheory.Measure α) (μ₂ : MeasureTheory.Measure α) (s : Set α) :
    (μ₁ + μ₂) s = μ₁ s + μ₂ s
    Equations
    • MeasureTheory.Measure.instSMul = { smul := fun (c : R) (μ : MeasureTheory.Measure α) => { toOuterMeasure := c μ.toOuterMeasure, m_iUnion := , trim_le := } }
    @[simp]
    theorem MeasureTheory.Measure.smul_toOuterMeasure {α : Type u_1} {R : Type u_6} [SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] {_m : MeasurableSpace α} (c : R) (μ : MeasureTheory.Measure α) :
    (c μ).toOuterMeasure = c μ.toOuterMeasure
    @[simp]
    theorem MeasureTheory.Measure.coe_smul {α : Type u_1} {R : Type u_6} [SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] {_m : MeasurableSpace α} (c : R) (μ : MeasureTheory.Measure α) :
    (c μ) = c μ
    @[simp]
    theorem MeasureTheory.Measure.smul_apply {α : Type u_1} {R : Type u_6} [SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] {_m : MeasurableSpace α} (c : R) (μ : MeasureTheory.Measure α) (s : Set α) :
    (c μ) s = c μ s
    Equations
    Equations

    Coercion to function as an additive monoid homomorphism.

    Equations
    • MeasureTheory.Measure.coeAddHom = { toFun := DFunLike.coe, map_zero' := , map_add' := }
    Instances For
      @[simp]
      theorem MeasureTheory.Measure.coe_finset_sum {α : Type u_1} {ι : Type u_5} {_m : MeasurableSpace α} (I : Finset ι) (μ : ιMeasureTheory.Measure α) :
      (∑ iI, μ i) = iI, (μ i)
      theorem MeasureTheory.Measure.finset_sum_apply {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} (I : Finset ι) (μ : ιMeasureTheory.Measure α) (s : Set α) :
      (∑ iI, μ i) s = iI, (μ i) s
      Equations
      Equations
      • MeasureTheory.Measure.instModule = Function.Injective.module R { toFun := MeasureTheory.Measure.toOuterMeasure, map_zero' := , map_add' := }
      @[simp]
      theorem MeasureTheory.Measure.coe_nnreal_smul_apply {α : Type u_1} {_m : MeasurableSpace α} (c : NNReal) (μ : MeasureTheory.Measure α) (s : Set α) :
      (c μ) s = c * μ s
      @[simp]
      theorem MeasureTheory.Measure.nnreal_smul_coe_apply {α : Type u_1} {_m : MeasurableSpace α} (c : NNReal) (μ : MeasureTheory.Measure α) (s : Set α) :
      c μ s = c * μ s
      theorem MeasureTheory.Measure.ae_smul_measure_iff {α : Type u_1} {m0 : MeasurableSpace α} {R : Type u_8} [Zero R] [SMulWithZero R ENNReal] [IsScalarTower R ENNReal ENNReal] [NoZeroSMulDivisors R ENNReal] {c : R} {p : αProp} (hc : c 0) {μ : MeasureTheory.Measure α} :
      (∀ᵐ (x : α) ∂c μ, p x) ∀ᵐ (x : α) ∂μ, p x
      theorem MeasureTheory.Measure.measure_eq_left_of_subset_of_measure_add_eq {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {s : Set α} {t : Set α} (h : (μ + ν) t ) (h' : s t) (h'' : (μ + ν) s = (μ + ν) t) :
      μ s = μ t
      theorem MeasureTheory.Measure.measure_eq_right_of_subset_of_measure_add_eq {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {s : Set α} {t : Set α} (h : (μ + ν) t ) (h' : s t) (h'' : (μ + ν) s = (μ + ν) t) :
      ν s = ν t
      theorem MeasureTheory.Measure.measure_toMeasurable_add_inter_left {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {s : Set α} {t : Set α} (hs : MeasurableSet s) (ht : (μ + ν) t ) :
      μ (MeasureTheory.toMeasurable (μ + ν) t s) = μ (t s)
      theorem MeasureTheory.Measure.measure_toMeasurable_add_inter_right {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {s : Set α} {t : Set α} (hs : MeasurableSet s) (ht : (μ + ν) t ) :
      ν (MeasureTheory.toMeasurable (μ + ν) t s) = ν (t s)

      The complete lattice of measures #

      Measures are partially ordered.

      Equations
      theorem MeasureTheory.Measure.toOuterMeasure_le {α : Type u_1} {m0 : MeasurableSpace α} {μ₁ : MeasureTheory.Measure α} {μ₂ : MeasureTheory.Measure α} :
      μ₁.toOuterMeasure μ₂.toOuterMeasure μ₁ μ₂
      theorem MeasureTheory.Measure.le_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ₁ : MeasureTheory.Measure α} {μ₂ : MeasureTheory.Measure α} :
      μ₁ μ₂ ∀ (s : Set α), MeasurableSet sμ₁ s μ₂ s
      theorem MeasureTheory.Measure.le_intro {α : Type u_1} {m0 : MeasurableSpace α} {μ₁ : MeasureTheory.Measure α} {μ₂ : MeasureTheory.Measure α} (h : ∀ (s : Set α), MeasurableSet ss.Nonemptyμ₁ s μ₂ s) :
      μ₁ μ₂
      theorem MeasureTheory.Measure.le_iff' {α : Type u_1} {m0 : MeasurableSpace α} {μ₁ : MeasureTheory.Measure α} {μ₂ : MeasureTheory.Measure α} :
      μ₁ μ₂ ∀ (s : Set α), μ₁ s μ₂ s
      theorem MeasureTheory.Measure.lt_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} :
      μ < ν μ ν ∃ (s : Set α), MeasurableSet s μ s < ν s
      theorem MeasureTheory.Measure.lt_iff' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} :
      μ < ν μ ν ∃ (s : Set α), μ s < ν s
      theorem MeasureTheory.Measure.le_add_left {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {ν' : MeasureTheory.Measure α} (h : μ ν) :
      μ ν' + ν
      theorem MeasureTheory.Measure.le_add_right {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {ν' : MeasureTheory.Measure α} (h : μ ν) :
      μ ν + ν'
      Equations
      • MeasureTheory.Measure.instInfSet = { sInf := fun (m : Set (MeasureTheory.Measure α)) => (sInf (MeasureTheory.Measure.toOuterMeasure '' m)).toMeasure }
      theorem MeasureTheory.Measure.sInf_apply {α : Type u_1} {m0 : MeasurableSpace α} {s : Set α} {m : Set (MeasureTheory.Measure α)} (hs : MeasurableSet s) :
      (sInf m) s = (sInf (MeasureTheory.Measure.toOuterMeasure '' m)) s
      Equations
      Equations
      @[simp]
      theorem MeasureTheory.OuterMeasure.toMeasure_top {α : Type u_1} {m0 : MeasurableSpace α} :
      .toMeasure =
      @[simp]
      theorem MeasureTheory.Measure.toOuterMeasure_top {α : Type u_1} :
      ∀ {x : MeasurableSpace α}, .toOuterMeasure =
      @[simp]
      @[simp]
      @[simp]
      theorem MeasureTheory.Measure.measure_univ_eq_zero {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} :
      μ Set.univ = 0 μ = 0
      theorem MeasureTheory.Measure.measure_univ_ne_zero {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} :
      μ Set.univ 0 μ 0
      Equations
      • =
      @[simp]
      theorem MeasureTheory.Measure.measure_univ_pos {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} :
      0 < μ Set.univ μ 0

      Pushforward and pullback #

      Lift a linear map between OuterMeasure spaces such that for each measure μ every measurable set is caratheodory-measurable w.r.t. f μ to a linear map between Measure spaces.

      Equations
      Instances For
        theorem MeasureTheory.Measure.liftLinear_apply₀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : MeasureTheory.OuterMeasure α →ₗ[ENNReal] MeasureTheory.OuterMeasure β} (hf : ∀ (μ : MeasureTheory.Measure α), inst✝ (f μ.toOuterMeasure).caratheodory) {s : Set β} (hs : MeasureTheory.NullMeasurableSet s ((MeasureTheory.Measure.liftLinear f hf) μ)) :
        ((MeasureTheory.Measure.liftLinear f hf) μ) s = (f μ.toOuterMeasure) s
        @[simp]
        theorem MeasureTheory.Measure.liftLinear_apply {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : MeasureTheory.OuterMeasure α →ₗ[ENNReal] MeasureTheory.OuterMeasure β} (hf : ∀ (μ : MeasureTheory.Measure α), inst✝ (f μ.toOuterMeasure).caratheodory) {s : Set β} (hs : MeasurableSet s) :
        ((MeasureTheory.Measure.liftLinear f hf) μ) s = (f μ.toOuterMeasure) s
        theorem MeasureTheory.Measure.le_liftLinear_apply {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : MeasureTheory.OuterMeasure α →ₗ[ENNReal] MeasureTheory.OuterMeasure β} (hf : ∀ (μ : MeasureTheory.Measure α), inst✝ (f μ.toOuterMeasure).caratheodory) (s : Set β) :
        (f μ.toOuterMeasure) s ((MeasureTheory.Measure.liftLinear f hf) μ) s

        The pushforward of a measure as a linear map. It is defined to be 0 if f is not a measurable function.

        Equations
        Instances For
          theorem MeasureTheory.Measure.mapₗ_congr {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : αβ} {g : αβ} (hf : Measurable f) (hg : Measurable g) (h : f =ᵐ[μ] g) :
          @[irreducible]
          def MeasureTheory.Measure.map {α : Type u_8} {β : Type u_9} [MeasurableSpace β] [MeasurableSpace α] (f : αβ) (μ : MeasureTheory.Measure α) :

          The pushforward of a measure. It is defined to be 0 if f is not an almost everywhere measurable function.

          Equations
          Instances For
            theorem MeasureTheory.Measure.map_def {α : Type u_8} {β : Type u_9} [MeasurableSpace β] [MeasurableSpace α] (f : αβ) (μ : MeasureTheory.Measure α) :
            @[simp]
            theorem MeasureTheory.Measure.map_zero {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] (f : αβ) :
            @[simp]
            theorem MeasureTheory.Measure.map_of_not_aemeasurable {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : αβ} {μ : MeasureTheory.Measure α} (hf : ¬AEMeasurable f μ) :
            theorem MeasureTheory.Measure.map_congr {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : αβ} {g : αβ} (h : f =ᵐ[μ] g) :
            @[simp]
            theorem MeasureTheory.Measure.map_smul {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] (c : ENNReal) (μ : MeasureTheory.Measure α) (f : αβ) :
            @[simp]
            theorem MeasureTheory.Measure.map_apply₀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : αβ} (hf : AEMeasurable f μ) {s : Set β} (hs : MeasureTheory.NullMeasurableSet s (MeasureTheory.Measure.map f μ)) :
            @[simp]
            theorem MeasureTheory.Measure.map_apply_of_aemeasurable {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : αβ} (hf : AEMeasurable f μ) {s : Set β} (hs : MeasurableSet s) :

            We can evaluate the pushforward on measurable sets. For non-measurable sets, see MeasureTheory.Measure.le_map_apply and MeasurableEquiv.map_apply.

            @[simp]
            theorem MeasureTheory.Measure.map_apply {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : αβ} (hf : Measurable f) {s : Set β} (hs : MeasurableSet s) :
            theorem MeasureTheory.Measure.map_toOuterMeasure {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : αβ} (hf : AEMeasurable f μ) :
            (MeasureTheory.Measure.map f μ).toOuterMeasure = ((MeasureTheory.OuterMeasure.map f) μ.toOuterMeasure).trim
            @[simp]
            theorem MeasureTheory.Measure.map_eq_zero_iff {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : αβ} (hf : AEMeasurable f μ) :
            @[simp]
            theorem MeasureTheory.Measure.mapₗ_eq_zero_iff {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : αβ} (hf : Measurable f) :
            theorem MeasureTheory.Measure.measure_preimage_of_map_eq_self {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αα} (hf : MeasureTheory.Measure.map f μ = μ) {s : Set α} (hs : MeasureTheory.NullMeasurableSet s μ) :
            μ (f ⁻¹' s) = μ s

            If map f μ = μ, then the measure of the preimage of any null measurable set s is equal to the measure of s. Note that this lemma does not assume (a.e.) measurability of f.

            theorem MeasureTheory.Measure.map_ne_zero_iff {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : αβ} (hf : AEMeasurable f μ) :
            theorem MeasureTheory.Measure.mapₗ_ne_zero_iff {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : αβ} (hf : Measurable f) :
            @[simp]
            theorem MeasureTheory.Measure.map_id' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} :
            MeasureTheory.Measure.map (fun (x : α) => x) μ = μ
            theorem MeasureTheory.Measure.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] [MeasurableSpace γ] {μ : MeasureTheory.Measure α} {g : βγ} {f : αβ} (hg : Measurable g) (hf : Measurable f) :
            theorem MeasureTheory.Measure.map_mono {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : αβ} (h : μ ν) (hf : Measurable f) :
            theorem MeasureTheory.Measure.le_map_apply {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : αβ} (hf : AEMeasurable f μ) (s : Set β) :

            Even if s is not measurable, we can bound map f μ s from below. See also MeasurableEquiv.map_apply.

            theorem MeasureTheory.Measure.le_map_apply_image {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : αβ} (hf : AEMeasurable f μ) (s : Set α) :
            μ s (MeasureTheory.Measure.map f μ) (f '' s)
            theorem MeasureTheory.Measure.preimage_null_of_map_null {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : αβ} (hf : AEMeasurable f μ) {s : Set β} (hs : (MeasureTheory.Measure.map f μ) s = 0) :
            μ (f ⁻¹' s) = 0

            Even if s is not measurable, map f μ s = 0 implies that μ (f ⁻¹' s) = 0.

            Pullback of a Measure as a linear map. If f sends each measurable set to a measurable set, then for each measurable set s we have comapₗ f μ s = μ (f '' s).

            Note that if f is not injective, this definition assigns Set.univ measure zero.

            If the linearity is not needed, please use comap instead, which works for a larger class of functions. comapₗ is an auxiliary definition and most lemmas deal with comap.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              theorem MeasureTheory.Measure.comapₗ_apply {α : Type u_1} {s : Set α} {β : Type u_8} :
              ∀ {x : MeasurableSpace α} { : MeasurableSpace β} (f : αβ), Function.Injective f(∀ (s : Set α), MeasurableSet sMeasurableSet (f '' s))∀ (μ : MeasureTheory.Measure β), MeasurableSet s((MeasureTheory.Measure.comapₗ f) μ) s = μ (f '' s)
              def MeasureTheory.Measure.comap {α : Type u_1} {β : Type u_2} [MeasurableSpace β] [MeasurableSpace α] (f : αβ) (μ : MeasureTheory.Measure β) :

              Pullback of a Measure. If f sends each measurable set to a null-measurable set, then for each measurable set s we have comap f μ s = μ (f '' s).

              Note that if f is not injective, this definition assigns Set.univ measure zero.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                theorem MeasureTheory.Measure.comap_apply₀ {α : Type u_1} {β : Type u_2} [MeasurableSpace β] {s : Set α} :
                theorem MeasureTheory.Measure.le_comap_apply {α : Type u_1} {β : Type u_8} :
                ∀ {x : MeasurableSpace α} { : MeasurableSpace β} (f : αβ) (μ : MeasureTheory.Measure β), Function.Injective f(∀ (s : Set α), MeasurableSet sMeasureTheory.NullMeasurableSet (f '' s) μ)∀ (s : Set α), μ (f '' s) (MeasureTheory.Measure.comap f μ) s
                theorem MeasureTheory.Measure.comap_apply {α : Type u_1} {s : Set α} {β : Type u_8} :
                ∀ {x : MeasurableSpace α} {_mβ : MeasurableSpace β} (f : αβ), Function.Injective f(∀ (s : Set α), MeasurableSet sMeasurableSet (f '' s))∀ (μ : MeasureTheory.Measure β), MeasurableSet s(MeasureTheory.Measure.comap f μ) s = μ (f '' s)
                theorem MeasureTheory.Measure.comapₗ_eq_comap {α : Type u_1} {s : Set α} {β : Type u_8} :
                ∀ {x : MeasurableSpace α} {_mβ : MeasurableSpace β} (f : αβ), Function.Injective f(∀ (s : Set α), MeasurableSet sMeasurableSet (f '' s))∀ (μ : MeasureTheory.Measure β), MeasurableSet s((MeasureTheory.Measure.comapₗ f) μ) s = (MeasureTheory.Measure.comap f μ) s
                theorem MeasureTheory.Measure.measure_image_eq_zero_of_comap_eq_zero {α : Type u_1} {β : Type u_8} :
                ∀ {x : MeasurableSpace α} {_mβ : MeasurableSpace β} (f : αβ) (μ : MeasureTheory.Measure β), Function.Injective f(∀ (s : Set α), MeasurableSet sMeasureTheory.NullMeasurableSet (f '' s) μ)∀ {s : Set α}, (MeasureTheory.Measure.comap f μ) s = 0μ (f '' s) = 0
                theorem MeasureTheory.Measure.ae_eq_image_of_ae_eq_comap {α : Type u_1} {β : Type u_8} :
                ∀ {x : MeasurableSpace α} { : MeasurableSpace β} (f : αβ) (μ : MeasureTheory.Measure β), Function.Injective f(∀ (s : Set α), MeasurableSet sMeasureTheory.NullMeasurableSet (f '' s) μ)∀ {s t : Set α}, s =ᵐ[MeasureTheory.Measure.comap f μ] tf '' s =ᵐ[μ] f '' t
                theorem MeasureTheory.Measure.comap_preimage {α : Type u_1} {β : Type u_8} :
                ∀ {x : MeasurableSpace α} { : MeasurableSpace β} (f : αβ) (μ : MeasureTheory.Measure β) {s : Set β}, Function.Injective fMeasurable f(∀ (t : Set α), MeasurableSet tMeasureTheory.NullMeasurableSet (f '' t) μ)MeasurableSet s(MeasureTheory.Measure.comap f μ) (f ⁻¹' s) = μ (s Set.range f)
                @[simp]
                theorem MeasureTheory.Measure.comap_zero {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : αβ} :
                noncomputable def MeasureTheory.Measure.sum {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} (f : ιMeasureTheory.Measure α) :

                Sum of an indexed family of measures.

                Equations
                Instances For
                  theorem MeasureTheory.Measure.le_sum_apply {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} (f : ιMeasureTheory.Measure α) (s : Set α) :
                  ∑' (i : ι), (f i) s (MeasureTheory.Measure.sum f) s
                  @[simp]
                  theorem MeasureTheory.Measure.sum_apply {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} (f : ιMeasureTheory.Measure α) {s : Set α} (hs : MeasurableSet s) :
                  (MeasureTheory.Measure.sum f) s = ∑' (i : ι), (f i) s
                  theorem MeasureTheory.Measure.sum_apply₀ {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} (f : ιMeasureTheory.Measure α) {s : Set α} (hs : MeasureTheory.NullMeasurableSet s (MeasureTheory.Measure.sum f)) :
                  (MeasureTheory.Measure.sum f) s = ∑' (i : ι), (f i) s

                  For the next theorem, the countability assumption is necessary. For a counterexample, consider an uncountable space, with a distinguished point x₀, and the sigma-algebra made of countable sets not containing x₀, and their complements. All points but x₀ are measurable. Consider the sum of the Dirac masses at points different from x₀, and s = x₀. For any Dirac mass δ_x, we have δ_x (x₀) = 0, so ∑' x, δ_x (x₀) = 0. On the other hand, the measure sum δ_x gives mass one to each point different from x₀, so it gives infinite mass to any measurable set containing x₀ (as such a set is uncountable), and by outer regularity one get sum δ_x {x₀} = ∞.

                  theorem MeasureTheory.Measure.sum_apply_of_countable {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} [Countable ι] (f : ιMeasureTheory.Measure α) (s : Set α) :
                  (MeasureTheory.Measure.sum f) s = ∑' (i : ι), (f i) s
                  theorem MeasureTheory.Measure.le_sum {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} (μ : ιMeasureTheory.Measure α) (i : ι) :
                  @[simp]
                  theorem MeasureTheory.Measure.sum_apply_eq_zero {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} [Countable ι] {μ : ιMeasureTheory.Measure α} {s : Set α} :
                  (MeasureTheory.Measure.sum μ) s = 0 ∀ (i : ι), (μ i) s = 0
                  theorem MeasureTheory.Measure.sum_apply_eq_zero' {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} {μ : ιMeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) :
                  (MeasureTheory.Measure.sum μ) s = 0 ∀ (i : ι), (μ i) s = 0
                  @[simp]
                  theorem MeasureTheory.Measure.sum_eq_zero {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} {f : ιMeasureTheory.Measure α} :
                  MeasureTheory.Measure.sum f = 0 ∀ (i : ι), f i = 0
                  @[simp]
                  theorem MeasureTheory.Measure.sum_zero {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} :
                  (MeasureTheory.Measure.sum fun (x : ι) => 0) = 0
                  theorem MeasureTheory.Measure.sum_sum {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} {ι' : Type u_8} (μ : ιι'MeasureTheory.Measure α) :
                  (MeasureTheory.Measure.sum fun (n : ι) => MeasureTheory.Measure.sum (μ n)) = MeasureTheory.Measure.sum fun (p : ι × ι') => μ p.1 p.2
                  theorem MeasureTheory.Measure.sum_comm {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} {ι' : Type u_8} (μ : ιι'MeasureTheory.Measure α) :
                  (MeasureTheory.Measure.sum fun (n : ι) => MeasureTheory.Measure.sum (μ n)) = MeasureTheory.Measure.sum fun (m : ι') => MeasureTheory.Measure.sum fun (n : ι) => μ n m
                  theorem MeasureTheory.Measure.ae_sum_iff {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} [Countable ι] {μ : ιMeasureTheory.Measure α} {p : αProp} :
                  (∀ᵐ (x : α) ∂MeasureTheory.Measure.sum μ, p x) ∀ (i : ι), ∀ᵐ (x : α) ∂μ i, p x
                  theorem MeasureTheory.Measure.ae_sum_iff' {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} {μ : ιMeasureTheory.Measure α} {p : αProp} (h : MeasurableSet {x : α | p x}) :
                  (∀ᵐ (x : α) ∂MeasureTheory.Measure.sum μ, p x) ∀ (i : ι), ∀ᵐ (x : α) ∂μ i, p x
                  @[simp]
                  theorem MeasureTheory.Measure.sum_fintype {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} [Fintype ι] (μ : ιMeasureTheory.Measure α) :
                  MeasureTheory.Measure.sum μ = i : ι, μ i
                  theorem MeasureTheory.Measure.sum_coe_finset {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} (s : Finset ι) (μ : ιMeasureTheory.Measure α) :
                  (MeasureTheory.Measure.sum fun (i : { x : ι // x s }) => μ i) = is, μ i
                  @[simp]
                  theorem MeasureTheory.Measure.ae_sum_eq {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} [Countable ι] (μ : ιMeasureTheory.Measure α) :
                  theorem MeasureTheory.Measure.sum_cond {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) :
                  (MeasureTheory.Measure.sum fun (b : Bool) => bif b then μ else ν) = μ + ν
                  @[simp]
                  @[deprecated MeasureTheory.Measure.sum_of_isEmpty]
                  theorem MeasureTheory.Measure.sum_of_empty {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} [IsEmpty ι] (μ : ιMeasureTheory.Measure α) :

                  Alias of MeasureTheory.Measure.sum_of_isEmpty.

                  theorem MeasureTheory.Measure.sum_add_sum_compl {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} (s : Set ι) (μ : ιMeasureTheory.Measure α) :
                  ((MeasureTheory.Measure.sum fun (i : s) => μ i) + MeasureTheory.Measure.sum fun (i : s) => μ i) = MeasureTheory.Measure.sum μ
                  @[simp]
                  theorem MeasureTheory.Measure.sum_comp_equiv {α : Type u_1} {m0 : MeasurableSpace α} {ι : Type u_8} {ι' : Type u_9} (e : ι' ι) (m : ιMeasureTheory.Measure α) :
                  @[simp]
                  theorem MeasureTheory.Measure.sum_extend_zero {α : Type u_1} {m0 : MeasurableSpace α} {ι : Type u_8} {ι' : Type u_9} {f : ιι'} (hf : Function.Injective f) (m : ιMeasureTheory.Measure α) :

                  Absolute continuity #

                  We say that μ is absolutely continuous with respect to ν, or that μ is dominated by ν, if ν(A) = 0 implies that μ(A) = 0.

                  Equations
                  • μ.AbsolutelyContinuous ν = ∀ ⦃s : Set α⦄, ν s = 0μ s = 0
                  Instances For

                    We say that μ is absolutely continuous with respect to ν, or that μ is dominated by ν, if ν(A) = 0 implies that μ(A) = 0.

                    Equations
                    Instances For
                      theorem MeasureTheory.Measure.absolutelyContinuous_of_le {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} (h : μ ν) :
                      μ.AbsolutelyContinuous ν
                      theorem LE.le.absolutelyContinuous {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} (h : μ ν) :
                      μ.AbsolutelyContinuous ν

                      Alias of MeasureTheory.Measure.absolutelyContinuous_of_le.

                      theorem MeasureTheory.Measure.absolutelyContinuous_of_eq {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} (h : μ = ν) :
                      μ.AbsolutelyContinuous ν
                      theorem Eq.absolutelyContinuous {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} (h : μ = ν) :
                      μ.AbsolutelyContinuous ν

                      Alias of MeasureTheory.Measure.absolutelyContinuous_of_eq.

                      theorem MeasureTheory.Measure.AbsolutelyContinuous.mk {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} (h : ∀ ⦃s : Set α⦄, MeasurableSet sν s = 0μ s = 0) :
                      μ.AbsolutelyContinuous ν
                      theorem MeasureTheory.Measure.AbsolutelyContinuous.refl {α : Type u_1} {_m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) :
                      μ.AbsolutelyContinuous μ
                      theorem MeasureTheory.Measure.AbsolutelyContinuous.rfl {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} :
                      μ.AbsolutelyContinuous μ
                      instance MeasureTheory.Measure.AbsolutelyContinuous.instIsRefl {α : Type u_1} :
                      ∀ {x : MeasurableSpace α}, IsRefl (MeasureTheory.Measure α) fun (x1 x2 : MeasureTheory.Measure α) => x1.AbsolutelyContinuous x2
                      Equations
                      • =
                      theorem MeasureTheory.Measure.AbsolutelyContinuous.trans {α : Type u_1} {m0 : MeasurableSpace α} {μ₁ : MeasureTheory.Measure α} {μ₂ : MeasureTheory.Measure α} {μ₃ : MeasureTheory.Measure α} (h1 : μ₁.AbsolutelyContinuous μ₂) (h2 : μ₂.AbsolutelyContinuous μ₃) :
                      μ₁.AbsolutelyContinuous μ₃
                      theorem MeasureTheory.Measure.AbsolutelyContinuous.map {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} (h : μ.AbsolutelyContinuous ν) {f : αβ} (hf : Measurable f) :
                      (MeasureTheory.Measure.map f μ).AbsolutelyContinuous (MeasureTheory.Measure.map f ν)
                      theorem MeasureTheory.Measure.AbsolutelyContinuous.smul {α : Type u_1} {R : Type u_6} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [Monoid R] [DistribMulAction R ENNReal] [IsScalarTower R ENNReal ENNReal] (h : μ.AbsolutelyContinuous ν) (c : R) :
                      (c μ).AbsolutelyContinuous ν
                      theorem MeasureTheory.Measure.AbsolutelyContinuous.add {α : Type u_1} {m0 : MeasurableSpace α} {μ₁ : MeasureTheory.Measure α} {μ₂ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {ν' : MeasureTheory.Measure α} (h1 : μ₁.AbsolutelyContinuous ν) (h2 : μ₂.AbsolutelyContinuous ν') :
                      (μ₁ + μ₂).AbsolutelyContinuous (ν + ν')
                      theorem MeasureTheory.Measure.AbsolutelyContinuous.add_left_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ₁ : MeasureTheory.Measure α} {μ₂ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} :
                      (μ₁ + μ₂).AbsolutelyContinuous ν μ₁.AbsolutelyContinuous ν μ₂.AbsolutelyContinuous ν
                      theorem MeasureTheory.Measure.AbsolutelyContinuous.add_left {α : Type u_1} {m0 : MeasurableSpace α} {μ₁ : MeasureTheory.Measure α} {μ₂ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} (h₁ : μ₁.AbsolutelyContinuous ν) (h₂ : μ₂.AbsolutelyContinuous ν) :
                      (μ₁ + μ₂).AbsolutelyContinuous ν
                      theorem MeasureTheory.Measure.AbsolutelyContinuous.add_right {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} (h1 : μ.AbsolutelyContinuous ν) (ν' : MeasureTheory.Measure α) :
                      μ.AbsolutelyContinuous (ν + ν')
                      @[simp]
                      theorem MeasureTheory.Measure.absolutelyContinuous_zero_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} :
                      μ.AbsolutelyContinuous 0 μ = 0
                      theorem MeasureTheory.Measure.absolutelyContinuous_sum_left {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} {ν : MeasureTheory.Measure α} {μs : ιMeasureTheory.Measure α} (hμs : ∀ (i : ι), (μs i).AbsolutelyContinuous ν) :
                      (MeasureTheory.Measure.sum μs).AbsolutelyContinuous ν
                      theorem MeasureTheory.Measure.absolutelyContinuous_sum_right {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} {ν : MeasureTheory.Measure α} {μs : ιMeasureTheory.Measure α} (i : ι) (hνμ : ν.AbsolutelyContinuous (μs i)) :
                      ν.AbsolutelyContinuous (MeasureTheory.Measure.sum μs)
                      theorem MeasureTheory.Measure.absolutelyContinuous_of_le_smul {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {μ' : MeasureTheory.Measure α} {c : ENNReal} (hμ'_le : μ' c μ) :
                      μ'.AbsolutelyContinuous μ
                      theorem MeasureTheory.Measure.smul_absolutelyContinuous {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {c : ENNReal} :
                      (c μ).AbsolutelyContinuous μ
                      theorem MeasureTheory.Measure.absolutelyContinuous_smul {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {c : ENNReal} (hc : c 0) :
                      μ.AbsolutelyContinuous (c μ)
                      theorem LE.le.absolutelyContinuous_of_ae {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} :
                      MeasureTheory.ae μ MeasureTheory.ae νμ.AbsolutelyContinuous ν

                      Alias of the forward direction of MeasureTheory.Measure.ae_le_iff_absolutelyContinuous.

                      theorem MeasureTheory.Measure.ae_mono' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} :
                      μ.AbsolutelyContinuous νMeasureTheory.ae μ MeasureTheory.ae ν

                      Alias of the reverse direction of MeasureTheory.Measure.ae_le_iff_absolutelyContinuous.


                      Alias of the reverse direction of MeasureTheory.Measure.ae_le_iff_absolutelyContinuous.

                      theorem MeasureTheory.Measure.AbsolutelyContinuous.ae_eq {α : Type u_1} {δ : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} (h : μ.AbsolutelyContinuous ν) {f : αδ} {g : αδ} (h' : f =ᵐ[ν] g) :
                      f =ᵐ[μ] g
                      theorem MeasureTheory.AEDisjoint.of_absolutelyContinuous {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (h : MeasureTheory.AEDisjoint μ s t) {ν : MeasureTheory.Measure α} (h' : ν.AbsolutelyContinuous μ) :
                      theorem MeasureTheory.AEDisjoint.of_le {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (h : MeasureTheory.AEDisjoint μ s t) {ν : MeasureTheory.Measure α} (h' : ν μ) :

                      Quasi measure preserving maps (a.k.a. non-singular maps) #

                      A map f : α → β is said to be quasi measure preserving (a.k.a. non-singular) w.r.t. measures μa and μb if it is measurable and μb s = 0 implies μa (f ⁻¹' s) = 0.

                      Instances For
                        theorem MeasureTheory.Measure.QuasiMeasurePreserving.mono_left {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μa : MeasureTheory.Measure α} {μa' : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β} {f : αβ} (h : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb) (ha : μa'.AbsolutelyContinuous μa) :
                        theorem MeasureTheory.Measure.QuasiMeasurePreserving.mono_right {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μa : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β} {μb' : MeasureTheory.Measure β} {f : αβ} (h : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb) (ha : μb.AbsolutelyContinuous μb') :
                        theorem MeasureTheory.Measure.QuasiMeasurePreserving.mono {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μa : MeasureTheory.Measure α} {μa' : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β} {μb' : MeasureTheory.Measure β} {f : αβ} (ha : μa'.AbsolutelyContinuous μa) (hb : μb.AbsolutelyContinuous μb') (h : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb) :
                        theorem MeasureTheory.Measure.QuasiMeasurePreserving.ae {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μa : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β} {f : αβ} (h : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb) {p : βProp} (hg : ∀ᵐ (x : β) ∂μb, p x) :
                        ∀ᵐ (x : α) ∂μa, p (f x)
                        theorem MeasureTheory.Measure.QuasiMeasurePreserving.ae_eq {α : Type u_1} {β : Type u_2} {δ : Type u_4} {m0 : MeasurableSpace α} [MeasurableSpace β] {μa : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β} {f : αβ} (h : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb) {g₁ : βδ} {g₂ : βδ} (hg : g₁ =ᵐ[μb] g₂) :
                        g₁ f =ᵐ[μa] g₂ f
                        theorem MeasureTheory.Measure.QuasiMeasurePreserving.preimage_null {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μa : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β} {f : αβ} (h : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb) {s : Set β} (hs : μb s = 0) :
                        μa (f ⁻¹' s) = 0
                        theorem MeasureTheory.Measure.QuasiMeasurePreserving.preimage_mono_ae {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μa : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β} {f : αβ} {s : Set β} {t : Set β} (hf : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb) (h : s ≤ᵐ[μb] t) :
                        theorem MeasureTheory.Measure.QuasiMeasurePreserving.preimage_ae_eq {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μa : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β} {f : αβ} {s : Set β} {t : Set β} (hf : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb) (h : s =ᵐ[μb] t) :
                        f ⁻¹' s =ᵐ[μa] f ⁻¹' t

                        The preimage of a null measurable set under a (quasi) measure preserving map is a null measurable set.

                        theorem MeasureTheory.Measure.QuasiMeasurePreserving.image_zpow_ae_eq {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {e : α α} (he : MeasureTheory.Measure.QuasiMeasurePreserving (⇑e) μ μ) (he' : MeasureTheory.Measure.QuasiMeasurePreserving (⇑e.symm) μ μ) (k : ) (hs : e '' s =ᵐ[μ] s) :
                        (e ^ k) '' s =ᵐ[μ] s
                        theorem MeasureTheory.Measure.QuasiMeasurePreserving.limsup_preimage_iterate_ae_eq {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : αα} (hf : MeasureTheory.Measure.QuasiMeasurePreserving f μ μ) (hs : f ⁻¹' s =ᵐ[μ] s) :
                        Filter.limsup (fun (n : ) => (Set.preimage f)^[n] s) Filter.atTop =ᵐ[μ] s
                        theorem MeasureTheory.Measure.QuasiMeasurePreserving.liminf_preimage_iterate_ae_eq {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : αα} (hf : MeasureTheory.Measure.QuasiMeasurePreserving f μ μ) (hs : f ⁻¹' s =ᵐ[μ] s) :
                        Filter.liminf (fun (n : ) => (Set.preimage f)^[n] s) Filter.atTop =ᵐ[μ] s

                        For a quasi measure preserving self-map f, if a null measurable set s is a.e. invariant, then it is a.e. equal to a measurable invariant set.

                        theorem MeasureTheory.Measure.QuasiMeasurePreserving.vadd_ae_eq_of_ae_eq {G : Type u_8} {α : Type u_9} [AddGroup G] [AddAction G α] :
                        ∀ {x : MeasurableSpace α} {s t : Set α} {μ : MeasureTheory.Measure α} (g : G), MeasureTheory.Measure.QuasiMeasurePreserving (fun (x : α) => -g +ᵥ x) μ μs =ᵐ[μ] tg +ᵥ s =ᵐ[μ] g +ᵥ t
                        theorem MeasureTheory.Measure.QuasiMeasurePreserving.smul_ae_eq_of_ae_eq {G : Type u_8} {α : Type u_9} [Group G] [MulAction G α] :
                        ∀ {x : MeasurableSpace α} {s t : Set α} {μ : MeasureTheory.Measure α} (g : G), MeasureTheory.Measure.QuasiMeasurePreserving (fun (x : α) => g⁻¹ x) μ μs =ᵐ[μ] tg s =ᵐ[μ] g t
                        theorem MeasureTheory.Measure.pairwise_aedisjoint_of_aedisjoint_forall_ne_zero {G : Type u_8} {α : Type u_9} [AddGroup G] [AddAction G α] :
                        ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}, (∀ (g : G), g 0MeasureTheory.AEDisjoint μ (g +ᵥ s) s)(∀ (g : G), MeasureTheory.Measure.QuasiMeasurePreserving (fun (x : α) => g +ᵥ x) μ μ)Pairwise (MeasureTheory.AEDisjoint μ on fun (g : G) => g +ᵥ s)
                        theorem MeasureTheory.Measure.pairwise_aedisjoint_of_aedisjoint_forall_ne_one {G : Type u_8} {α : Type u_9} [Group G] [MulAction G α] :
                        ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}, (∀ (g : G), g 1MeasureTheory.AEDisjoint μ (g s) s)(∀ (g : G), MeasureTheory.Measure.QuasiMeasurePreserving (fun (x : α) => g x) μ μ)Pairwise (MeasureTheory.AEDisjoint μ on fun (g : G) => g s)

                        The cofinite filter #

                        The filter of sets s such that sᶜ has finite measure.

                        Equations
                        Instances For
                          theorem MeasureTheory.Measure.mem_cofinite {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} :
                          s μ.cofinite μ s <
                          theorem MeasureTheory.Measure.compl_mem_cofinite {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} :
                          s μ.cofinite μ s <
                          theorem MeasureTheory.Measure.eventually_cofinite {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : αProp} :
                          (∀ᶠ (x : α) in μ.cofinite, p x) μ {x : α | ¬p x} <
                          instance MeasureTheory.Measure.cofinite.instIsMeasurablyGenerated {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} :
                          μ.cofinite.IsMeasurablyGenerated
                          Equations
                          • =
                          theorem AEMeasurable.nullMeasurable {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : αβ} (h : AEMeasurable f μ) :
                          theorem AEMeasurable.nullMeasurableSet_preimage {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : αβ} {s : Set β} (hf : AEMeasurable f μ) (hs : MeasurableSet s) :
                          theorem MeasureTheory.NullMeasurableSet.mono_ac {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {s : Set α} (h : MeasureTheory.NullMeasurableSet s μ) (hle : ν.AbsolutelyContinuous μ) :
                          theorem MeasureTheory.AEDisjoint.preimage {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : αβ} {s : Set β} {t : Set β} (ht : MeasureTheory.AEDisjoint ν s t) (hf : MeasureTheory.Measure.QuasiMeasurePreserving f μ ν) :
                          @[simp]
                          @[simp]
                          theorem MeasureTheory.ae_neBot {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} :
                          (MeasureTheory.ae μ).NeBot μ 0
                          instance MeasureTheory.Measure.ae.neBot {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NeZero μ] :
                          (MeasureTheory.ae μ).NeBot
                          Equations
                          • =
                          @[simp]
                          theorem MeasureTheory.mem_ae_map_iff {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : αβ} (hf : AEMeasurable f μ) {s : Set β} (hs : MeasurableSet s) :
                          theorem MeasureTheory.mem_ae_of_mem_ae_map {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : αβ} (hf : AEMeasurable f μ) {s : Set β} (hs : s MeasureTheory.ae (MeasureTheory.Measure.map f μ)) :
                          theorem MeasureTheory.ae_map_iff {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : αβ} (hf : AEMeasurable f μ) {p : βProp} (hp : MeasurableSet {x : β | p x}) :
                          (∀ᵐ (y : β) ∂MeasureTheory.Measure.map f μ, p y) ∀ᵐ (x : α) ∂μ, p (f x)
                          theorem MeasureTheory.ae_of_ae_map {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : αβ} (hf : AEMeasurable f μ) {p : βProp} (h : ∀ᵐ (y : β) ∂MeasureTheory.Measure.map f μ, p y) :
                          ∀ᵐ (x : α) ∂μ, p (f x)
                          theorem MeasureTheory.ae_map_mem_range {α : Type u_1} {β : Type u_2} [MeasurableSpace β] {m0 : MeasurableSpace α} (f : αβ) (hf : MeasurableSet (Set.range f)) (μ : MeasureTheory.Measure α) :
                          ∀ᵐ (x : β) ∂MeasureTheory.Measure.map f μ, x Set.range f
                          theorem MeasureTheory.biSup_measure_Iic {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Preorder α] {s : Set α} (hsc : s.Countable) (hst : ∀ (x : α), ys, x y) (hdir : DirectedOn (fun (x1 x2 : α) => x1 x2) s) :
                          xs, μ (Set.Iic x) = μ Set.univ
                          theorem MeasureTheory.tendsto_measure_Ico_atTop {α : Type u_1} {m0 : MeasurableSpace α} [Preorder α] [NoMaxOrder α] [Filter.atTop.IsCountablyGenerated] (μ : MeasureTheory.Measure α) (a : α) :
                          Filter.Tendsto (fun (x : α) => μ (Set.Ico a x)) Filter.atTop (nhds (μ (Set.Ici a)))
                          theorem MeasureTheory.tendsto_measure_Ioc_atBot {α : Type u_1} {m0 : MeasurableSpace α} [Preorder α] [NoMinOrder α] [Filter.atBot.IsCountablyGenerated] (μ : MeasureTheory.Measure α) (a : α) :
                          Filter.Tendsto (fun (x : α) => μ (Set.Ioc x a)) Filter.atBot (nhds (μ (Set.Iic a)))
                          theorem MeasureTheory.tendsto_measure_Iic_atTop {α : Type u_1} {m0 : MeasurableSpace α} [Preorder α] [Filter.atTop.IsCountablyGenerated] (μ : MeasureTheory.Measure α) :
                          Filter.Tendsto (fun (x : α) => μ (Set.Iic x)) Filter.atTop (nhds (μ Set.univ))
                          theorem MeasureTheory.tendsto_measure_Ici_atBot {α : Type u_1} {m0 : MeasurableSpace α} [Preorder α] [Filter.atBot.IsCountablyGenerated] (μ : MeasureTheory.Measure α) :
                          Filter.Tendsto (fun (x : α) => μ (Set.Ici x)) Filter.atBot (nhds (μ Set.univ))
                          theorem MeasureTheory.Iio_ae_eq_Iic' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [PartialOrder α] {a : α} (ha : μ {a} = 0) :
                          theorem MeasureTheory.Ioi_ae_eq_Ici' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [PartialOrder α] {a : α} (ha : μ {a} = 0) :
                          theorem MeasureTheory.Ioo_ae_eq_Ioc' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [PartialOrder α] {a : α} {b : α} (hb : μ {b} = 0) :
                          theorem MeasureTheory.Ioc_ae_eq_Icc' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [PartialOrder α] {a : α} {b : α} (ha : μ {a} = 0) :
                          theorem MeasureTheory.Ioo_ae_eq_Ico' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [PartialOrder α] {a : α} {b : α} (ha : μ {a} = 0) :
                          theorem MeasureTheory.Ioo_ae_eq_Icc' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [PartialOrder α] {a : α} {b : α} (ha : μ {a} = 0) (hb : μ {b} = 0) :
                          theorem MeasureTheory.Ico_ae_eq_Icc' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [PartialOrder α] {a : α} {b : α} (hb : μ {b} = 0) :
                          theorem MeasureTheory.Ico_ae_eq_Ioc' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [PartialOrder α] {a : α} {b : α} (ha : μ {a} = 0) (hb : μ {b} = 0) :
                          theorem MeasurableEmbedding.map_apply {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {m1 : MeasurableSpace β} {f : αβ} (hf : MeasurableEmbedding f) (μ : MeasureTheory.Measure α) (s : Set β) :
                          theorem MeasurableEmbedding.absolutelyContinuous_map {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {m1 : MeasurableSpace β} {f : αβ} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} (hf : MeasurableEmbedding f) (hμν : μ.AbsolutelyContinuous ν) :
                          (MeasureTheory.Measure.map f μ).AbsolutelyContinuous (MeasureTheory.Measure.map f ν)

                          Interactions of measurable equivalences and measures

                          theorem MeasurableEquiv.map_apply {α : Type u_1} {β : Type u_2} :
                          ∀ {x : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α} (f : α ≃ᵐ β) (s : Set β), (MeasureTheory.Measure.map (⇑f) μ) s = μ (f ⁻¹' s)

                          If we map a measure along a measurable equivalence, we can compute the measure on all sets (not just the measurable ones).

                          theorem MeasurableEquiv.comap_symm {α : Type u_1} {β : Type u_2} :
                          ∀ {x : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α} (e : α ≃ᵐ β), MeasureTheory.Measure.comap (⇑e.symm) μ = MeasureTheory.Measure.map (⇑e) μ
                          theorem MeasurableEquiv.map_symm {α : Type u_1} {β : Type u_2} :
                          ∀ {x : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α} (e : β ≃ᵐ α), MeasureTheory.Measure.map (⇑e.symm) μ = MeasureTheory.Measure.comap (⇑e) μ
                          @[simp]
                          theorem MeasurableEquiv.map_symm_map {α : Type u_1} {β : Type u_2} :
                          ∀ {x : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α} (e : α ≃ᵐ β), MeasureTheory.Measure.map (⇑e.symm) (MeasureTheory.Measure.map (⇑e) μ) = μ
                          @[simp]
                          theorem MeasurableEquiv.map_map_symm {α : Type u_1} {β : Type u_2} :
                          ∀ {x : MeasurableSpace α} [inst : MeasurableSpace β] {ν : MeasureTheory.Measure β} (e : α ≃ᵐ β), MeasureTheory.Measure.map (⇑e) (MeasureTheory.Measure.map (⇑e.symm) ν) = ν
                          theorem MeasurableEquiv.map_apply_eq_iff_map_symm_apply_eq {α : Type u_1} {β : Type u_2} :
                          ∀ {x : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} (e : α ≃ᵐ β), MeasureTheory.Measure.map (⇑e) μ = ν MeasureTheory.Measure.map (⇑e.symm) ν = μ
                          theorem MeasurableEquiv.map_ae {α : Type u_1} {β : Type u_2} :
                          theorem MeasureTheory.Measure.comap_swap {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μ : MeasureTheory.Measure (α × β)) :