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

We introduce the following typeclasses for measures:

• IsProbabilityMeasure μ: μ univ = 1;
• IsFiniteMeasure μ: μ univ < ∞;
• SigmaFinite μ: there exists a countable collection of sets that cover univ where μ is finite;
• IsLocallyFiniteMeasure μ : ∀ x, ∃ s ∈ 𝓝 x, μ s < ∞;
• NoAtoms μ : ∀ x, μ {x} = 0; possibly should be redefined as ∀ s, 0 < μ s → ∃ t ⊆ s, 0 < μ t ∧ μ t < μ s.

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

• completion is the completion of a measure to all null measurable sets.
• Measure.ofMeasurable and OuterMeasure.toMeasure are two important ways to define a 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/Complete_measure
• https://en.wikipedia.org/wiki/Almost_everywhere

Tags

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

instance MeasureTheory.ae_isMeasurablyGenerated {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} : Filter.IsMeasurablyGenerated (MeasureTheory.Measure.ae μ)

Equations

• @MeasureTheory.ae_isMeasurablyGenerated = @MeasureTheory.ae_isMeasurablyGenerated.proof_1

theorem MeasureTheory.ae_uIoc_iff {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [LinearOrder α] {a : α} {b : α} {P : α → Prop} : (∀ᵐ (x : α) ∂μ, x ∈ Ι a b → P x) ↔ (∀ᵐ (x : α) ∂μ, x ∈ Set.Ioc a b → P x) ∧ ∀ᵐ (x : α) ∂μ, x ∈ Set.Ioc b a → P 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 : MeasurableSet s) (ht : MeasurableSet t) : ↑↑μ (s ∆ t) = ↑↑μ (s \ t) + ↑↑μ (t \ s)

theorem MeasureTheory.measure_symmDiff_le {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Set α) (t : Set α) (u : Set α) : ↑↑μ (s ∆ u) ≤ ↑↑μ (s ∆ t) + ↑↑μ (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 : Set.Countable s) (hd : Set.Pairwise s (MeasureTheory.AEDisjoint μ on f)) (h : ∀ (b : β), b ∈ s → MeasureTheory.NullMeasurableSet (f b)) : ↑↑μ (⋃ (b : β) (_ : b ∈ s), 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 : Set.Countable s) (hd : Set.PairwiseDisjoint s f) (h : ∀ (b : β), b ∈ s → MeasurableSet (f b)) : ↑↑μ (⋃ (b : β) (_ : b ∈ s), f b) = ∑' (p : ↑s), ↑↑μ (f ↑p)

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

theorem MeasureTheory.measure_sUnion {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {S : Set (Set α)} (hs : Set.Countable S) (hd : Set.Pairwise S Disjoint) (h : ∀ (s : Set α), s ∈ S → 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 : Set.Pairwise (↑s) (MeasureTheory.AEDisjoint μ on f)) (hm : ∀ (b : ι), b ∈ s → MeasureTheory.NullMeasurableSet (f b)) : ↑↑μ (⋃ (b : ι) (_ : b ∈ s), f b) = Finset.sum s fun p => ↑↑μ (f p)

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

theorem MeasureTheory.tsum_meas_le_meas_iUnion_of_disjoint₀ {α : Type u_1} {ι : Type u_8} [MeasurableSpace α] (μ : MeasureTheory.Measure α) {As : ι → Set α} (As_mble : ∀ (i : ι), MeasureTheory.NullMeasurableSet (As i)) (As_disj : 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} [MeasurableSpace α] (μ : MeasureTheory.Measure α) {As : ι → Set α} (As_mble : ∀ (i : ι), MeasurableSet (As i)) (As_disj : 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 : Set.Countable s) {f : α → β} (hf : ∀ (y : β), 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.sum_measure_preimage_singleton {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Finset β) {f : α → β} (hf : ∀ (y : β), y ∈ s → MeasurableSet (f ⁻¹' {y})) : (Finset.sum s fun b => ↑↑μ (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_diff_null {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ : Set α} {s₂ : Set α} (h : ↑↑μ s₂ = 0) : ↑↑μ (s₁ \ s₂) = ↑↑μ s₁

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

theorem MeasureTheory.measure_diff' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set α} (s : Set α) (hm : MeasurableSet 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₂ : MeasurableSet 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_diff_lt_of_lt_add {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (hs : MeasurableSet 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 : MeasurableSet 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₁ : MeasurableSet s) (h_fin : ↑↑μ s ≠ ⊤) : ↑↑μ sᶜ = ↑↑μ Set.univ - ↑↑μ s

@[simp]

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

@[simp]

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

theorem MeasureTheory.ae_eq_of_ae_subset_of_measure_ge {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (h₁ : s ≤ᶠ[MeasureTheory.Measure.ae μ] t) (h₂ : ↑↑μ t ≤ ↑↑μ s) (hsm : MeasurableSet s) (ht : ↑↑μ t ≠ ⊤) : s =ᶠ[MeasureTheory.Measure.ae μ] 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 : MeasurableSet s) (ht : ↑↑μ t ≠ ⊤) : s =ᶠ[MeasureTheory.Measure.ae μ] t

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

theorem MeasureTheory.measure_iUnion_congr_of_subset {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable β] {s : β → Set α} {t : β → Set α} (hsub : ∀ (b : β), s b ⊆ t b) (h_le : ∀ (b : β), ↑↑μ (t b) ≤ ↑↑μ (s b)) : ↑↑μ (⋃ (b : β), s b) = ↑↑μ (⋃ (b : β), t b)

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} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable β] (s : β → Set α) : ↑↑μ (⋃ (b : β), MeasureTheory.toMeasurable μ (s b)) = ↑↑μ (⋃ (b : β), s b)

theorem MeasureTheory.measure_biUnion_toMeasurable {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {I : Set β} (hc : Set.Countable I) (s : β → Set α) : ↑↑μ (⋃ (b : β) (_ : b ∈ I), MeasureTheory.toMeasurable μ (s b)) = ↑↑μ (⋃ (b : β) (_ : b ∈ I), 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 : ∀ (i : ι), i ∈ s → MeasurableSet (t i)) (H : Set.PairwiseDisjoint (↑s) t) : (Finset.sum s fun i => ↑↑μ (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 : ι), MeasurableSet (s i)) (H : Pairwise (Disjoint 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 : ι), MeasurableSet (s i)) (H : ↑↑μ Set.univ < ∑' (i : ι), ↑↑μ (s i)) : ∃ i j _h, Set.Nonempty (s i ∩ s j)

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 : ∀ (i : ι), i ∈ s → MeasurableSet (t i)) (H : ↑↑μ Set.univ < Finset.sum s fun i => ↑↑μ (t i)) : ∃ i, i ∈ s ∧ ∃ j, j ∈ s ∧ ∃ _h, Set.Nonempty (t i ∩ t j)

Pigeonhole principle for measure spaces: if s is a Finset and ∑ i in 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) : Set.Nonempty (s ∩ t)

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) : Set.Nonempty (s ∩ t)

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_iUnion_eq_iSup {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable ι] {s : ι → Set α} (hd : Directed (fun x x_1 => x ⊆ x_1) 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.

theorem MeasureTheory.measure_biUnion_eq_iSup {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : ι → Set α} {t : Set ι} (ht : Set.Countable t) (hd : DirectedOn ((fun x x_1 => x ⊆ x_1) on s) t) : ↑↑μ (⋃ (i : ι) (_ : i ∈ t), s i) = ⨆ (i : ι) (_ : i ∈ t), ↑↑μ (s i)

theorem MeasureTheory.measure_iInter_eq_iInf {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable ι] {s : ι → Set α} (h : ∀ (i : ι), MeasurableSet (s i)) (hd : Directed (fun x x_1 => x ⊇ x_1) 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.tendsto_measure_iUnion {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [SemilatticeSup ι] [Countable ι] {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 measurable sets is the limit of the measures.

theorem MeasureTheory.tendsto_measure_iInter {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable ι] [SemilatticeSup ι] {s : ι → Set α} (hs : ∀ (n : ι), MeasurableSet (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_biInter_gt {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Type u_8} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [DenselyOrdered ι] [TopologicalSpace.FirstCountableTopology ι] {s : ι → Set α} {a : ι} (hs : ∀ (r : ι), r > a → MeasurableSet (s r)) (hm : ∀ (i j : ι), a < i → i ≤ j → s i ⊆ s j) (hf : ∃ r, 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_limsup_eq_zero {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : ℕ → Set α} (hs : ∑' (i : ℕ), ↑↑μ (s i) ≠ ⊤) : ↑↑μ (Filter.limsup s Filter.atTop) = 0

One direction of the Borel-Cantelli lemma: if (sᵢ) is a sequence of sets such that ∑ μ sᵢ is finite, then the limit superior of the sᵢ is a null set.

theorem MeasureTheory.measure_liminf_eq_zero {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : ℕ → Set α} (h : ∑' (i : ℕ), ↑↑μ (s i) ≠ ⊤) : ↑↑μ (Filter.liminf s Filter.atTop) = 0

theorem MeasureTheory.limsup_ae_eq_of_forall_ae_eq {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : ℕ → Set α) {t : Set α} (h : ∀ (n : ℕ), s n =ᶠ[MeasureTheory.Measure.ae μ] t) : Filter.limsup s Filter.atTop =ᶠ[MeasureTheory.Measure.ae μ] t

theorem MeasureTheory.liminf_ae_eq_of_forall_ae_eq {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : ℕ → Set α) {t : Set α} (h : ∀ (n : ℕ), s n =ᶠ[MeasureTheory.Measure.ae μ] t) : Filter.liminf s Filter.atTop =ᶠ[MeasureTheory.Measure.ae μ] t

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

def MeasureTheory.OuterMeasure.toMeasure {α : Type u_1} [ms : MeasurableSpace α] (m : MeasureTheory.OuterMeasure α) (h : ms ≤ MeasureTheory.OuterMeasure.caratheodory m) : MeasureTheory.Measure α

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

Equations

• One or more equations did not get rendered due to their size.

theorem MeasureTheory.le_toOuterMeasure_caratheodory {α : Type u_1} [ms : MeasurableSpace α] (μ : MeasureTheory.Measure α) : ms ≤ MeasureTheory.OuterMeasure.caratheodory ↑μ

@[simp]

theorem MeasureTheory.toMeasure_toOuterMeasure {α : Type u_1} [ms : MeasurableSpace α] (m : MeasureTheory.OuterMeasure α) (h : ms ≤ MeasureTheory.OuterMeasure.caratheodory m) : ↑(MeasureTheory.OuterMeasure.toMeasure m h) = MeasureTheory.OuterMeasure.trim m

theorem MeasureTheory.toMeasure_apply {α : Type u_1} [ms : MeasurableSpace α] (m : MeasureTheory.OuterMeasure α) (h : ms ≤ MeasureTheory.OuterMeasure.caratheodory m) {s : Set α} (hs : MeasurableSet s) : ↑↑(MeasureTheory.OuterMeasure.toMeasure m h) s = ↑m s

theorem MeasureTheory.le_toMeasure_apply {α : Type u_1} [ms : MeasurableSpace α] (m : MeasureTheory.OuterMeasure α) (h : ms ≤ MeasureTheory.OuterMeasure.caratheodory m) (s : Set α) : ↑m s ≤ ↑↑(MeasureTheory.OuterMeasure.toMeasure m h) s

theorem MeasureTheory.toMeasure_apply₀ {α : Type u_1} [ms : MeasurableSpace α] (m : MeasureTheory.OuterMeasure α) (h : ms ≤ MeasureTheory.OuterMeasure.caratheodory m) {s : Set α} (hs : MeasureTheory.NullMeasurableSet s) : ↑↑(MeasureTheory.OuterMeasure.toMeasure m h) s = ↑m s

@[simp]

theorem MeasureTheory.toOuterMeasure_toMeasure {α : Type u_1} [ms : MeasurableSpace α] {μ : MeasureTheory.Measure α} : MeasureTheory.OuterMeasure.toMeasure ↑μ (_ : ms ≤ MeasureTheory.OuterMeasure.caratheodory ↑μ) = μ

theorem MeasureTheory.boundedBy_measure {α : Type u_1} [ms : MeasurableSpace α] (μ : MeasureTheory.Measure α) : MeasureTheory.OuterMeasure.boundedBy ↑↑μ = ↑μ

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 sigma_finite, see measure_toMeasurable_inter_of_sigmaFinite.

The ℝ≥0∞-module of measures

instance MeasureTheory.Measure.instZero {α : Type u_1} [MeasurableSpace α] : Zero (MeasureTheory.Measure α)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MeasureTheory.Measure.zero_toOuterMeasure {α : Type u_1} {_m : MeasurableSpace α} : ↑0 = 0

@[simp]

theorem MeasureTheory.Measure.coe_zero {α : Type u_1} {_m : MeasurableSpace α} : ↑↑0 = 0

instance MeasureTheory.Measure.instSubsingleton {α : Type u_1} [IsEmpty α] {m : MeasurableSpace α} : Subsingleton (MeasureTheory.Measure α)

Equations

• @MeasureTheory.Measure.instSubsingleton = @MeasureTheory.Measure.instSubsingleton.proof_1

theorem MeasureTheory.Measure.eq_zero_of_isEmpty {α : Type u_1} [IsEmpty α] {_m : MeasurableSpace α} (μ : MeasureTheory.Measure α) : μ = 0

instance MeasureTheory.Measure.instInhabited {α : Type u_1} [MeasurableSpace α] : Inhabited (MeasureTheory.Measure α)

Equations

• MeasureTheory.Measure.instInhabited = { default := 0 }

instance MeasureTheory.Measure.instAdd {α : Type u_1} [MeasurableSpace α] : Add (MeasureTheory.Measure α)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MeasureTheory.Measure.add_toOuterMeasure {α : Type u_1} {_m : MeasurableSpace α} (μ₁ : MeasureTheory.Measure α) (μ₂ : MeasureTheory.Measure α) : ↑(μ₁ + μ₂) = ↑μ₁ + ↑μ₂

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

instance MeasureTheory.Measure.instSMul {α : Type u_1} {R : Type u_6} [SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] [MeasurableSpace α] : SMul R (MeasureTheory.Measure α)

Equations

• One or more equations did not get rendered due to their size.

@[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 • μ) = c • ↑μ

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

instance MeasureTheory.Measure.instSMulCommClass {α : Type u_1} {R : Type u_6} {R' : Type u_7} [SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] [SMul R' ENNReal] [IsScalarTower R' ENNReal ENNReal] [SMulCommClass R R' ENNReal] [MeasurableSpace α] : SMulCommClass R R' (MeasureTheory.Measure α)

Equations

• @MeasureTheory.Measure.instSMulCommClass = @MeasureTheory.Measure.instSMulCommClass.proof_1

instance MeasureTheory.Measure.instIsScalarTower {α : Type u_1} {R : Type u_6} {R' : Type u_7} [SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] [SMul R' ENNReal] [IsScalarTower R' ENNReal ENNReal] [SMul R R'] [IsScalarTower R R' ENNReal] [MeasurableSpace α] : IsScalarTower R R' (MeasureTheory.Measure α)

Equations

• @MeasureTheory.Measure.instIsScalarTower = @MeasureTheory.Measure.instIsScalarTower.proof_1

instance MeasureTheory.Measure.instIsCentralScalar {α : Type u_1} {R : Type u_6} [SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] [SMul Rᵐᵒᵖ ENNReal] [IsCentralScalar R ENNReal] [MeasurableSpace α] : IsCentralScalar R (MeasureTheory.Measure α)

Equations

• @MeasureTheory.Measure.instIsCentralScalar = @MeasureTheory.Measure.instIsCentralScalar.proof_1

instance MeasureTheory.Measure.instMulAction {α : Type u_1} {R : Type u_6} [Monoid R] [MulAction R ENNReal] [IsScalarTower R ENNReal ENNReal] [MeasurableSpace α] : MulAction R (MeasureTheory.Measure α)

Equations

• One or more equations did not get rendered due to their size.

instance MeasureTheory.Measure.instAddCommMonoid {α : Type u_1} [MeasurableSpace α] : AddCommMonoid (MeasureTheory.Measure α)

Equations

• One or more equations did not get rendered due to their size.

def MeasureTheory.Measure.coeAddHom {α : Type u_1} : {x : MeasurableSpace α} → MeasureTheory.Measure α →+ Set α → ENNReal

Coercion to function as an additive monoid homomorphism.

Equations

• MeasureTheory.Measure.coeAddHom = { toZeroHom := { toFun := fun x => ↑↑x, map_zero' := (_ : ↑↑0 = 0) }, map_add' := (_ : ∀ (μ₁ μ₂ : MeasureTheory.Measure α), ↑↑(μ₁ + μ₂) = ↑↑μ₁ + ↑↑μ₂) }

@[simp]

theorem MeasureTheory.Measure.coe_finset_sum {α : Type u_1} {ι : Type u_5} {_m : MeasurableSpace α} (I : Finset ι) (μ : ι → MeasureTheory.Measure α) : ↑↑(Finset.sum I fun i => μ i) = Finset.sum I fun i => ↑↑(μ i)

theorem MeasureTheory.Measure.finset_sum_apply {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} (I : Finset ι) (μ : ι → MeasureTheory.Measure α) (s : Set α) : ↑↑(Finset.sum I fun i => μ i) s = Finset.sum I fun i => ↑↑(μ i) s

instance MeasureTheory.Measure.instDistribMulAction {α : Type u_1} {R : Type u_6} [Monoid R] [DistribMulAction R ENNReal] [IsScalarTower R ENNReal ENNReal] [MeasurableSpace α] : DistribMulAction R (MeasureTheory.Measure α)

Equations

• One or more equations did not get rendered due to their size.

instance MeasureTheory.Measure.instModule {α : Type u_1} {R : Type u_6} [Semiring R] [Module R ENNReal] [IsScalarTower R ENNReal ENNReal] [MeasurableSpace α] : Module R (MeasureTheory.Measure α)

Equations

• One or more equations did not get rendered due to their size.

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 α} {μ : MeasureTheory.Measure α} {p : α → Prop} {c : ENNReal} (hc : c ≠ 0) : (∀ᵐ (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

instance MeasureTheory.Measure.instPartialOrder {α : Type u_1} [MeasurableSpace α] : PartialOrder (MeasureTheory.Measure α)

Measures are partially ordered.

The definition of less equal here is equivalent to the definition without the measurable set condition, and this is shown by Measure.le_iff'. It is defined this way since, to prove μ ≤ ν, we may simply intros s hs instead of rewriting followed by intros s hs.

Equations

• MeasureTheory.Measure.instPartialOrder = PartialOrder.mk (_ : ∀ (m₁ m₂ : MeasureTheory.Measure α), m₁ ≤ m₂ → m₂ ≤ m₁ → m₁ = m₂)

theorem MeasureTheory.Measure.le_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ₁ : MeasureTheory.Measure α} {μ₂ : MeasureTheory.Measure α} : μ₁ ≤ μ₂ ↔ ∀ (s : Set α), MeasurableSet s → ↑↑μ₁ s ≤ ↑↑μ₂ s

theorem MeasureTheory.Measure.toOuterMeasure_le {α : Type u_1} {m0 : MeasurableSpace α} {μ₁ : MeasureTheory.Measure α} {μ₂ : MeasureTheory.Measure α} : ↑μ₁ ≤ ↑μ₂ ↔ μ₁ ≤ μ₂

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, MeasurableSet s ∧ ↑↑μ s < ↑↑ν s

theorem MeasureTheory.Measure.lt_iff' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} : μ < ν ↔ μ ≤ ν ∧ ∃ s, ↑↑μ s < ↑↑ν s

instance MeasureTheory.Measure.covariantAddLE {α : Type u_1} [MeasurableSpace α] : CovariantClass (MeasureTheory.Measure α) (MeasureTheory.Measure α) (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

Equations

• @MeasureTheory.Measure.covariantAddLE = @MeasureTheory.Measure.covariantAddLE.proof_1

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 : μ ≤ ν) : μ ≤ ν + ν'

theorem MeasureTheory.Measure.sInf_caratheodory {α : Type u_1} {m0 : MeasurableSpace α} {m : Set (MeasureTheory.Measure α)} (s : Set α) (hs : MeasurableSet s) : MeasurableSet s

instance MeasureTheory.Measure.instInfSetMeasure {α : Type u_1} [MeasurableSpace α] : InfSet (MeasureTheory.Measure α)

Equations

• One or more equations did not get rendered due to their size.

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

instance MeasureTheory.Measure.instCompleteSemilatticeInf {α : Type u_1} [MeasurableSpace α] : CompleteSemilatticeInf (MeasureTheory.Measure α)

Equations

• One or more equations did not get rendered due to their size.

instance MeasureTheory.Measure.instCompleteLattice {α : Type u_1} [MeasurableSpace α] : CompleteLattice (MeasureTheory.Measure α)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MeasureTheory.OuterMeasure.toMeasure_top {α : Type u_1} [MeasurableSpace α] : MeasureTheory.OuterMeasure.toMeasure ⊤ (_ : inst✝ ≤ MeasureTheory.OuterMeasure.caratheodory ⊤) = ⊤

@[simp]

theorem MeasureTheory.Measure.toOuterMeasure_top {α : Type u_1} [MeasurableSpace α] : ↑⊤ = ⊤

@[simp]

theorem MeasureTheory.Measure.top_add {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} : ⊤ + μ = ⊤

@[simp]

theorem MeasureTheory.Measure.add_top {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} : μ + ⊤ = ⊤

theorem MeasureTheory.Measure.zero_le {α : Type u_1} {_m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) : 0 ≤ μ

theorem MeasureTheory.Measure.nonpos_iff_eq_zero' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} : μ ≤ 0 ↔ μ = 0

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

instance MeasureTheory.Measure.instNeZeroENNRealInstENNRealZeroMeasureOfToOuterMeasureUniv {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NeZero μ] : NeZero (↑↑μ Set.univ)

Equations

• @MeasureTheory.Measure.instNeZeroENNRealInstENNRealZeroMeasureOfToOuterMeasureUniv = @MeasureTheory.Measure.instNeZeroENNRealInstENNRealZeroMeasureOfToOuterMeasureUniv.proof_1

@[simp]

theorem MeasureTheory.Measure.measure_univ_pos {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} : 0 < ↑↑μ Set.univ ↔ μ ≠ 0

Pushforward and pullback

def MeasureTheory.Measure.liftLinear {α : Type u_1} {β : Type u_2} [MeasurableSpace β] {m0 : MeasurableSpace α} (f : MeasureTheory.OuterMeasure α →ₗ[ENNReal] MeasureTheory.OuterMeasure β) (hf : ∀ (μ : MeasureTheory.Measure α), inst✝ ≤ MeasureTheory.OuterMeasure.caratheodory (↑f ↑μ)) : MeasureTheory.Measure α →ₗ[ENNReal] MeasureTheory.Measure β

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

• One or more equations did not get rendered due to their size.

@[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✝ ≤ MeasureTheory.OuterMeasure.caratheodory (↑f ↑μ)) {s : Set β} (hs : MeasurableSet s) : ↑↑(↑(MeasureTheory.Measure.liftLinear f hf) μ) s = ↑(↑f ↑μ) 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✝ ≤ MeasureTheory.OuterMeasure.caratheodory (↑f ↑μ)) (s : Set β) : ↑(↑f ↑μ) s ≤ ↑↑(↑(MeasureTheory.Measure.liftLinear f hf) μ) s

def MeasureTheory.Measure.mapₗ {α : Type u_1} {β : Type u_2} [MeasurableSpace β] [MeasurableSpace α] (f : α → β) : MeasureTheory.Measure α →ₗ[ENNReal] MeasureTheory.Measure β

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

Equations

• One or more equations did not get rendered due to their size.

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 =ᶠ[MeasureTheory.Measure.ae μ] g) : ↑(MeasureTheory.Measure.mapₗ f) μ = ↑(MeasureTheory.Measure.mapₗ g) μ

@[irreducible]

def MeasureTheory.Measure.map {α : Type u_8} {β : Type u_9} [MeasurableSpace β] [MeasurableSpace α] (f : α → β) (μ : MeasureTheory.Measure α) : MeasureTheory.Measure β

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

Equations

• @MeasureTheory.Measure.map = MeasureTheory.Measure.wrapped✝.1

theorem MeasureTheory.Measure.map_def {α : Type u_8} {β : Type u_9} [MeasurableSpace β] [MeasurableSpace α] (f : α → β) (μ : MeasureTheory.Measure α) : MeasureTheory.Measure.map f μ = if hf : AEMeasurable f then ↑(MeasureTheory.Measure.mapₗ (AEMeasurable.mk f hf)) μ else 0

theorem MeasureTheory.Measure.mapₗ_mk_apply_of_aemeasurable {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : α → β} (hf : AEMeasurable f) : ↑(MeasureTheory.Measure.mapₗ (AEMeasurable.mk f hf)) μ = MeasureTheory.Measure.map f μ

theorem MeasureTheory.Measure.mapₗ_apply_of_measurable {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : α → β} (hf : Measurable f) (μ : MeasureTheory.Measure α) : ↑(MeasureTheory.Measure.mapₗ f) μ = MeasureTheory.Measure.map f μ

@[simp]

theorem MeasureTheory.Measure.map_add {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) {f : α → β} (hf : Measurable f) : MeasureTheory.Measure.map f (μ + ν) = MeasureTheory.Measure.map f μ + MeasureTheory.Measure.map f ν

@[simp]

theorem MeasureTheory.Measure.map_zero {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] (f : α → β) : MeasureTheory.Measure.map f 0 = 0

theorem MeasureTheory.Measure.map_of_not_aemeasurable {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {f : α → β} {μ : MeasureTheory.Measure α} (hf : ¬AEMeasurable f) : MeasureTheory.Measure.map f μ = 0

theorem MeasureTheory.Measure.map_congr {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : α → β} {g : α → β} (h : f =ᶠ[MeasureTheory.Measure.ae μ] g) : MeasureTheory.Measure.map f μ = MeasureTheory.Measure.map g μ

@[simp]

theorem MeasureTheory.Measure.map_smul {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] (c : ENNReal) (μ : MeasureTheory.Measure α) (f : α → β) : MeasureTheory.Measure.map f (c • μ) = c • MeasureTheory.Measure.map f μ

@[simp]

theorem MeasureTheory.Measure.map_smul_nnreal {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] (c : NNReal) (μ : MeasureTheory.Measure α) (f : α → β) : MeasureTheory.Measure.map f (c • μ) = c • 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) : ↑↑(MeasureTheory.Measure.map f μ) s = ↑↑μ (f ⁻¹' 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) : ↑↑(MeasureTheory.Measure.map f μ) s = ↑↑μ (f ⁻¹' 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 μ) = MeasureTheory.OuterMeasure.trim (↑(MeasureTheory.OuterMeasure.map f) ↑μ)

@[simp]

theorem MeasureTheory.Measure.map_id {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} : MeasureTheory.Measure.map id μ = μ

@[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) : MeasureTheory.Measure.map g (MeasureTheory.Measure.map f μ) = MeasureTheory.Measure.map (g ∘ f) μ

theorem MeasureTheory.Measure.map_mono {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : α → β} (h : μ ≤ ν) (hf : Measurable f) : MeasureTheory.Measure.map f μ ≤ MeasureTheory.Measure.map f ν

theorem MeasureTheory.Measure.le_map_apply {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : α → β} (hf : AEMeasurable f) (s : Set β) : ↑↑μ (f ⁻¹' s) ≤ ↑↑(MeasureTheory.Measure.map f μ) s

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

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.

theorem MeasureTheory.Measure.tendsto_ae_map {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : α → β} (hf : AEMeasurable f) : Filter.Tendsto f (MeasureTheory.Measure.ae μ) (MeasureTheory.Measure.ae (MeasureTheory.Measure.map f μ))

def MeasureTheory.Measure.comapₗ {α : Type u_1} {β : Type u_2} [MeasurableSpace β] [MeasurableSpace α] (f : α → β) : MeasureTheory.Measure β →ₗ[ENNReal] MeasureTheory.Measure α

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

If the linearity is not needed, please use comap instead, which works for a larger class of functions.

Equations

• One or more equations did not get rendered due to their size.

theorem MeasureTheory.Measure.comapₗ_apply {α : Type u_1} {s : Set α} {β : Type u_8} [MeasurableSpace α] {mβ : MeasurableSpace β} (f : α → β) (hfi : Function.Injective f) (hf : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)) (μ : MeasureTheory.Measure β) (hs : MeasurableSet s) : ↑↑(↑(MeasureTheory.Measure.comapₗ f) μ) s = ↑↑μ (f '' s)

def MeasureTheory.Measure.comap {α : Type u_1} {β : Type u_2} [MeasurableSpace β] [MeasurableSpace α] (f : α → β) (μ : MeasureTheory.Measure β) : 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).

Equations

• One or more equations did not get rendered due to their size.

theorem MeasureTheory.Measure.comap_apply₀ {α : Type u_1} {β : Type u_2} [MeasurableSpace β] {s : Set α} [MeasurableSpace α] (f : α → β) (μ : MeasureTheory.Measure β) (hfi : Function.Injective f) (hf : ∀ (s : Set α), MeasurableSet s → MeasureTheory.NullMeasurableSet (f '' s)) (hs : MeasureTheory.NullMeasurableSet s) : ↑↑(MeasureTheory.Measure.comap f μ) s = ↑↑μ (f '' s)

theorem MeasureTheory.Measure.le_comap_apply {α : Type u_1} {β : Type u_8} [MeasurableSpace α] {mβ : MeasurableSpace β} (f : α → β) (μ : MeasureTheory.Measure β) (hfi : Function.Injective f) (hf : ∀ (s : Set α), MeasurableSet s → MeasureTheory.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} [MeasurableSpace α] {_mβ : MeasurableSpace β} (f : α → β) (hfi : Function.Injective f) (hf : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)) (μ : MeasureTheory.Measure β) (hs : MeasurableSet s) : ↑↑(MeasureTheory.Measure.comap f μ) s = ↑↑μ (f '' s)

theorem MeasureTheory.Measure.comapₗ_eq_comap {α : Type u_1} {s : Set α} {β : Type u_8} [MeasurableSpace α] {_mβ : MeasurableSpace β} (f : α → β) (hfi : Function.Injective f) (hf : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)) (μ : MeasureTheory.Measure β) (hs : 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} [MeasurableSpace α] {_mβ : MeasurableSpace β} (f : α → β) (μ : MeasureTheory.Measure β) (hfi : Function.Injective f) (hf : ∀ (s : Set α), MeasurableSet s → MeasureTheory.NullMeasurableSet (f '' s)) {s : Set α} (hs : ↑↑(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} [MeasurableSpace α] {mβ : MeasurableSpace β} (f : α → β) (μ : MeasureTheory.Measure β) (hfi : Function.Injective f) (hf : ∀ (s : Set α), MeasurableSet s → MeasureTheory.NullMeasurableSet (f '' s)) {s : Set α} {t : Set α} (hst : s =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.comap f μ)] t) : f '' s =ᶠ[MeasureTheory.Measure.ae μ] f '' t

theorem MeasureTheory.Measure.NullMeasurableSet.image {α : Type u_1} {β : Type u_8} [MeasurableSpace α] {mβ : MeasurableSpace β} (f : α → β) (μ : MeasureTheory.Measure β) (hfi : Function.Injective f) (hf : ∀ (s : Set α), MeasurableSet s → MeasureTheory.NullMeasurableSet (f '' s)) {s : Set α} (hs : MeasureTheory.NullMeasurableSet s) : MeasureTheory.NullMeasurableSet (f '' s)

theorem MeasureTheory.Measure.comap_preimage {α : Type u_1} {β : Type u_8} [MeasurableSpace α] {mβ : MeasurableSpace β} (f : α → β) (μ : MeasureTheory.Measure β) {s : Set β} (hf : Function.Injective f) (hf' : Measurable f) (h : ∀ (t : Set α), MeasurableSet t → MeasureTheory.NullMeasurableSet (f '' t)) (hs : MeasurableSet s) : ↑↑(MeasureTheory.Measure.comap f μ) (f ⁻¹' s) = ↑↑μ (s ∩ Set.range f)

Subtype of a measure space

theorem MeasureTheory.Measure.MeasurableSet.nullMeasurableSet_subtype_coe {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set ↑s} (hs : MeasureTheory.NullMeasurableSet s) (ht : MeasurableSet t) : MeasureTheory.NullMeasurableSet (Subtype.val '' t)

theorem MeasureTheory.Measure.NullMeasurableSet.subtype_coe {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set ↑s} (hs : MeasureTheory.NullMeasurableSet s) (ht : MeasureTheory.NullMeasurableSet t) : MeasureTheory.NullMeasurableSet (Subtype.val '' t)

theorem MeasureTheory.Measure.measure_subtype_coe_le_comap {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasureTheory.NullMeasurableSet s) (t : Set ↑s) : ↑↑μ (Subtype.val '' t) ≤ ↑↑(MeasureTheory.Measure.comap Subtype.val μ) t

theorem MeasureTheory.Measure.measure_subtype_coe_eq_zero_of_comap_eq_zero {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasureTheory.NullMeasurableSet s) {t : Set ↑s} (ht : ↑↑(MeasureTheory.Measure.comap Subtype.val μ) t = 0) : ↑↑μ (Subtype.val '' t) = 0

instance MeasureTheory.Measure.Subtype.measureSpace {α : Type u_1} [MeasureTheory.MeasureSpace α] {p : α → Prop} : MeasureTheory.MeasureSpace (Subtype p)

Equations

• MeasureTheory.Measure.Subtype.measureSpace = let src := Subtype.instMeasurableSpace; MeasureTheory.MeasureSpace.mk (MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume)

theorem MeasureTheory.Measure.Subtype.volume_def {α : Type u_1} {s : Set α} [MeasureTheory.MeasureSpace α] : MeasureTheory.volume = MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume

theorem MeasureTheory.Measure.Subtype.volume_univ {α : Type u_1} {s : Set α} [MeasureTheory.MeasureSpace α] (hs : MeasureTheory.NullMeasurableSet s) : ↑↑MeasureTheory.volume Set.univ = ↑↑MeasureTheory.volume s

theorem MeasureTheory.Measure.volume_subtype_coe_le_volume {α : Type u_1} {s : Set α} [MeasureTheory.MeasureSpace α] (hs : MeasureTheory.NullMeasurableSet s) (t : Set ↑s) : ↑↑MeasureTheory.volume (Subtype.val '' t) ≤ ↑↑MeasureTheory.volume t

theorem MeasureTheory.Measure.volume_subtype_coe_eq_zero_of_volume_eq_zero {α : Type u_1} {s : Set α} [MeasureTheory.MeasureSpace α] (hs : MeasureTheory.NullMeasurableSet s) {t : Set ↑s} (ht : ↑↑MeasureTheory.volume t = 0) : ↑↑MeasureTheory.volume (Subtype.val '' t) = 0

Restricting a measure

def MeasureTheory.Measure.restrictₗ {α : Type u_1} {m0 : MeasurableSpace α} (s : Set α) : MeasureTheory.Measure α →ₗ[ENNReal] MeasureTheory.Measure α

Restrict a measure μ to a set s as an ℝ≥0∞-linear map.

Equations

• One or more equations did not get rendered due to their size.

def MeasureTheory.Measure.restrict {α : Type u_1} {_m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (s : Set α) : MeasureTheory.Measure α

Restrict a measure μ to a set s.

Equations

• MeasureTheory.Measure.restrict μ s = ↑(MeasureTheory.Measure.restrictₗ s) μ

@[simp]

theorem MeasureTheory.Measure.restrictₗ_apply {α : Type u_1} {_m0 : MeasurableSpace α} (s : Set α) (μ : MeasureTheory.Measure α) : ↑(MeasureTheory.Measure.restrictₗ s) μ = MeasureTheory.Measure.restrict μ s

theorem MeasureTheory.Measure.restrict_toOuterMeasure_eq_toOuterMeasure_restrict {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (h : MeasurableSet s) : ↑(MeasureTheory.Measure.restrict μ s) = ↑(MeasureTheory.OuterMeasure.restrict s) ↑μ

This lemma shows that restrict and toOuterMeasure commute. Note that the LHS has a restrict on measures and the RHS has a restrict on outer measures.

theorem MeasureTheory.Measure.restrict_apply₀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (ht : MeasureTheory.NullMeasurableSet t) : ↑↑(MeasureTheory.Measure.restrict μ s) t = ↑↑μ (t ∩ s)

@[simp]

theorem MeasureTheory.Measure.restrict_apply {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (ht : MeasurableSet t) : ↑↑(MeasureTheory.Measure.restrict μ s) t = ↑↑μ (t ∩ s)

If t is a measurable set, then the measure of t with respect to the restriction of the measure to s equals the outer measure of t ∩ s. An alternate version requiring that s be measurable instead of t exists as Measure.restrict_apply'.

theorem MeasureTheory.Measure.restrict_mono' {α : Type u_1} {_m0 : MeasurableSpace α} ⦃s : Set α⦄ ⦃s' : Set α⦄ ⦃μ : MeasureTheory.Measure α⦄ ⦃ν : MeasureTheory.Measure α⦄ (hs : s ≤ᶠ[MeasureTheory.Measure.ae μ] s') (hμν : μ ≤ ν) : MeasureTheory.Measure.restrict μ s ≤ MeasureTheory.Measure.restrict ν s'

Restriction of a measure to a subset is monotone both in set and in measure.

theorem MeasureTheory.Measure.restrict_mono {α : Type u_1} {_m0 : MeasurableSpace α} ⦃s : Set α⦄ ⦃s' : Set α⦄ (hs : s ⊆ s') ⦃μ : MeasureTheory.Measure α⦄ ⦃ν : MeasureTheory.Measure α⦄ (hμν : μ ≤ ν) : MeasureTheory.Measure.restrict μ s ≤ MeasureTheory.Measure.restrict ν s'

Restriction of a measure to a subset is monotone both in set and in measure.

theorem MeasureTheory.Measure.restrict_mono_ae {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (h : s ≤ᶠ[MeasureTheory.Measure.ae μ] t) : MeasureTheory.Measure.restrict μ s ≤ MeasureTheory.Measure.restrict μ t

theorem MeasureTheory.Measure.restrict_congr_set {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (h : s =ᶠ[MeasureTheory.Measure.ae μ] t) : MeasureTheory.Measure.restrict μ s = MeasureTheory.Measure.restrict μ t

@[simp]

theorem MeasureTheory.Measure.restrict_apply' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (hs : MeasurableSet s) : ↑↑(MeasureTheory.Measure.restrict μ s) t = ↑↑μ (t ∩ s)

If s is a measurable set, then the outer measure of t with respect to the restriction of the measure to s equals the outer measure of t ∩ s. This is an alternate version of Measure.restrict_apply, requiring that s is measurable instead of t.

theorem MeasureTheory.Measure.restrict_apply₀' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (hs : MeasureTheory.NullMeasurableSet s) : ↑↑(MeasureTheory.Measure.restrict μ s) t = ↑↑μ (t ∩ s)

theorem MeasureTheory.Measure.restrict_le_self {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} : MeasureTheory.Measure.restrict μ s ≤ μ

theorem MeasureTheory.Measure.restrict_eq_self {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) {s : Set α} {t : Set α} (h : s ⊆ t) : ↑↑(MeasureTheory.Measure.restrict μ t) s = ↑↑μ s

@[simp]

theorem MeasureTheory.Measure.restrict_apply_self {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (s : Set α) : ↑↑(MeasureTheory.Measure.restrict μ s) s = ↑↑μ s

theorem MeasureTheory.Measure.restrict_apply_univ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Set α) : ↑↑(MeasureTheory.Measure.restrict μ s) Set.univ = ↑↑μ s

theorem MeasureTheory.Measure.le_restrict_apply {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Set α) (t : Set α) : ↑↑μ (t ∩ s) ≤ ↑↑(MeasureTheory.Measure.restrict μ s) t

theorem MeasureTheory.Measure.restrict_apply_superset {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (h : s ⊆ t) : ↑↑(MeasureTheory.Measure.restrict μ s) t = ↑↑μ s

@[simp]

theorem MeasureTheory.Measure.restrict_add {α : Type u_1} {_m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) (s : Set α) : MeasureTheory.Measure.restrict (μ + ν) s = MeasureTheory.Measure.restrict μ s + MeasureTheory.Measure.restrict ν s

@[simp]

theorem MeasureTheory.Measure.restrict_zero {α : Type u_1} {_m0 : MeasurableSpace α} (s : Set α) : MeasureTheory.Measure.restrict 0 s = 0

@[simp]

theorem MeasureTheory.Measure.restrict_smul {α : Type u_1} {_m0 : MeasurableSpace α} (c : ENNReal) (μ : MeasureTheory.Measure α) (s : Set α) : MeasureTheory.Measure.restrict (c • μ) s = c • MeasureTheory.Measure.restrict μ s

theorem MeasureTheory.Measure.restrict_restrict₀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (hs : MeasureTheory.NullMeasurableSet s) : MeasureTheory.Measure.restrict (MeasureTheory.Measure.restrict μ t) s = MeasureTheory.Measure.restrict μ (s ∩ t)

@[simp]

theorem MeasureTheory.Measure.restrict_restrict {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (hs : MeasurableSet s) : MeasureTheory.Measure.restrict (MeasureTheory.Measure.restrict μ t) s = MeasureTheory.Measure.restrict μ (s ∩ t)

theorem MeasureTheory.Measure.restrict_restrict_of_subset {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (h : s ⊆ t) : MeasureTheory.Measure.restrict (MeasureTheory.Measure.restrict μ t) s = MeasureTheory.Measure.restrict μ s

theorem MeasureTheory.Measure.restrict_restrict₀' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (ht : MeasureTheory.NullMeasurableSet t) : MeasureTheory.Measure.restrict (MeasureTheory.Measure.restrict μ t) s = MeasureTheory.Measure.restrict μ (s ∩ t)

theorem MeasureTheory.Measure.restrict_restrict' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (ht : MeasurableSet t) : MeasureTheory.Measure.restrict (MeasureTheory.Measure.restrict μ t) s = MeasureTheory.Measure.restrict μ (s ∩ t)

theorem MeasureTheory.Measure.restrict_comm {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (hs : MeasurableSet s) : MeasureTheory.Measure.restrict (MeasureTheory.Measure.restrict μ t) s = MeasureTheory.Measure.restrict (MeasureTheory.Measure.restrict μ s) t

theorem MeasureTheory.Measure.restrict_apply_eq_zero {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (ht : MeasurableSet t) : ↑↑(MeasureTheory.Measure.restrict μ s) t = 0 ↔ ↑↑μ (t ∩ s) = 0

theorem MeasureTheory.Measure.measure_inter_eq_zero_of_restrict {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (h : ↑↑(MeasureTheory.Measure.restrict μ s) t = 0) : ↑↑μ (t ∩ s) = 0

theorem MeasureTheory.Measure.restrict_apply_eq_zero' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (hs : MeasurableSet s) : ↑↑(MeasureTheory.Measure.restrict μ s) t = 0 ↔ ↑↑μ (t ∩ s) = 0

@[simp]

theorem MeasureTheory.Measure.restrict_eq_zero {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} : MeasureTheory.Measure.restrict μ s = 0 ↔ ↑↑μ s = 0

instance MeasureTheory.Measure.restrict.neZero {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [NeZero (↑↑μ s)] : NeZero (MeasureTheory.Measure.restrict μ s)

If μ s ≠ 0, then μ.restrict s ≠ 0, in terms of NeZero instances.

Equations

• @MeasureTheory.Measure.restrict.neZero = @MeasureTheory.Measure.restrict.neZero.proof_1

theorem MeasureTheory.Measure.restrict_zero_set {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (h : ↑↑μ s = 0) : MeasureTheory.Measure.restrict μ s = 0

@[simp]

theorem MeasureTheory.Measure.restrict_empty {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} : MeasureTheory.Measure.restrict μ ∅ = 0

@[simp]

theorem MeasureTheory.Measure.restrict_univ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} : MeasureTheory.Measure.restrict μ Set.univ = μ

theorem MeasureTheory.Measure.restrict_inter_add_diff₀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set α} (s : Set α) (ht : MeasureTheory.NullMeasurableSet t) : MeasureTheory.Measure.restrict μ (s ∩ t) + MeasureTheory.Measure.restrict μ (s \ t) = MeasureTheory.Measure.restrict μ s

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

theorem MeasureTheory.Measure.restrict_union_add_inter₀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set α} (s : Set α) (ht : MeasureTheory.NullMeasurableSet t) : MeasureTheory.Measure.restrict μ (s ∪ t) + MeasureTheory.Measure.restrict μ (s ∩ t) = MeasureTheory.Measure.restrict μ s + MeasureTheory.Measure.restrict μ t

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

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

theorem MeasureTheory.Measure.restrict_union₀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (h : MeasureTheory.AEDisjoint μ s t) (ht : MeasureTheory.NullMeasurableSet t) : MeasureTheory.Measure.restrict μ (s ∪ t) = MeasureTheory.Measure.restrict μ s + MeasureTheory.Measure.restrict μ t

theorem MeasureTheory.Measure.restrict_union {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (h : Disjoint s t) (ht : MeasurableSet t) : MeasureTheory.Measure.restrict μ (s ∪ t) = MeasureTheory.Measure.restrict μ s + MeasureTheory.Measure.restrict μ t

theorem MeasureTheory.Measure.restrict_union' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (h : Disjoint s t) (hs : MeasurableSet s) : MeasureTheory.Measure.restrict μ (s ∪ t) = MeasureTheory.Measure.restrict μ s + MeasureTheory.Measure.restrict μ t

@[simp]

theorem MeasureTheory.Measure.restrict_add_restrict_compl {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) : MeasureTheory.Measure.restrict μ s + MeasureTheory.Measure.restrict μ sᶜ = μ

@[simp]

theorem MeasureTheory.Measure.restrict_compl_add_restrict {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) : MeasureTheory.Measure.restrict μ sᶜ + MeasureTheory.Measure.restrict μ s = μ

theorem MeasureTheory.Measure.restrict_union_le {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Set α) (s' : Set α) : MeasureTheory.Measure.restrict μ (s ∪ s') ≤ MeasureTheory.Measure.restrict μ s + MeasureTheory.Measure.restrict μ s'

theorem MeasureTheory.Measure.restrict_iUnion_apply_ae {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable ι] {s : ι → Set α} (hd : Pairwise (MeasureTheory.AEDisjoint μ on s)) (hm : ∀ (i : ι), MeasureTheory.NullMeasurableSet (s i)) {t : Set α} (ht : MeasurableSet t) : ↑↑(MeasureTheory.Measure.restrict μ (⋃ (i : ι), s i)) t = ∑' (i : ι), ↑↑(MeasureTheory.Measure.restrict μ (s i)) t

theorem MeasureTheory.Measure.restrict_iUnion_apply {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable ι] {s : ι → Set α} (hd : Pairwise (Disjoint on s)) (hm : ∀ (i : ι), MeasurableSet (s i)) {t : Set α} (ht : MeasurableSet t) : ↑↑(MeasureTheory.Measure.restrict μ (⋃ (i : ι), s i)) t = ∑' (i : ι), ↑↑(MeasureTheory.Measure.restrict μ (s i)) t

theorem MeasureTheory.Measure.restrict_iUnion_apply_eq_iSup {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable ι] {s : ι → Set α} (hd : Directed (fun x x_1 => x ⊆ x_1) s) {t : Set α} (ht : MeasurableSet t) : ↑↑(MeasureTheory.Measure.restrict μ (⋃ (i : ι), s i)) t = ⨆ (i : ι), ↑↑(MeasureTheory.Measure.restrict μ (s i)) t

theorem MeasureTheory.Measure.restrict_map {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : α → β} (hf : Measurable f) {s : Set β} (hs : MeasurableSet s) : MeasureTheory.Measure.restrict (MeasureTheory.Measure.map f μ) s = MeasureTheory.Measure.map f (MeasureTheory.Measure.restrict μ (f ⁻¹' s))

The restriction of the pushforward measure is the pushforward of the restriction. For a version assuming only AEMeasurable, see restrict_map_of_aemeasurable.

theorem MeasureTheory.Measure.restrict_toMeasurable {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (h : ↑↑μ s ≠ ⊤) : MeasureTheory.Measure.restrict μ (MeasureTheory.toMeasurable μ s) = MeasureTheory.Measure.restrict μ s

theorem MeasureTheory.Measure.restrict_eq_self_of_ae_mem {α : Type u_1} {_m0 : MeasurableSpace α} ⦃s : Set α⦄ ⦃μ : MeasureTheory.Measure α⦄ (hs : ∀ᵐ (x : α) ∂μ, x ∈ s) : MeasureTheory.Measure.restrict μ s = μ

theorem MeasureTheory.Measure.restrict_congr_meas {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) : MeasureTheory.Measure.restrict μ s = MeasureTheory.Measure.restrict ν s ↔ ∀ (t : Set α), t ⊆ s → MeasurableSet t → ↑↑μ t = ↑↑ν t

theorem MeasureTheory.Measure.restrict_congr_mono {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {s : Set α} {t : Set α} (hs : s ⊆ t) (h : MeasureTheory.Measure.restrict μ t = MeasureTheory.Measure.restrict ν t) : MeasureTheory.Measure.restrict μ s = MeasureTheory.Measure.restrict ν s

theorem MeasureTheory.Measure.restrict_union_congr {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {s : Set α} {t : Set α} : MeasureTheory.Measure.restrict μ (s ∪ t) = MeasureTheory.Measure.restrict ν (s ∪ t) ↔ MeasureTheory.Measure.restrict μ s = MeasureTheory.Measure.restrict ν s ∧ MeasureTheory.Measure.restrict μ t = MeasureTheory.Measure.restrict ν t

If two measures agree on all measurable subsets of s and t, then they agree on all measurable subsets of s ∪ t.

theorem MeasureTheory.Measure.restrict_finset_biUnion_congr {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {s : Finset ι} {t : ι → Set α} : MeasureTheory.Measure.restrict μ (⋃ (i : ι) (_ : i ∈ s), t i) = MeasureTheory.Measure.restrict ν (⋃ (i : ι) (_ : i ∈ s), t i) ↔ ∀ (i : ι), i ∈ s → MeasureTheory.Measure.restrict μ (t i) = MeasureTheory.Measure.restrict ν (t i)

theorem MeasureTheory.Measure.restrict_iUnion_congr {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [Countable ι] {s : ι → Set α} : MeasureTheory.Measure.restrict μ (⋃ (i : ι), s i) = MeasureTheory.Measure.restrict ν (⋃ (i : ι), s i) ↔ ∀ (i : ι), MeasureTheory.Measure.restrict μ (s i) = MeasureTheory.Measure.restrict ν (s i)

theorem MeasureTheory.Measure.restrict_biUnion_congr {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {s : Set ι} {t : ι → Set α} (hc : Set.Countable s) : MeasureTheory.Measure.restrict μ (⋃ (i : ι) (_ : i ∈ s), t i) = MeasureTheory.Measure.restrict ν (⋃ (i : ι) (_ : i ∈ s), t i) ↔ ∀ (i : ι), i ∈ s → MeasureTheory.Measure.restrict μ (t i) = MeasureTheory.Measure.restrict ν (t i)

theorem MeasureTheory.Measure.restrict_sUnion_congr {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {S : Set (Set α)} (hc : Set.Countable S) : MeasureTheory.Measure.restrict μ (⋃₀ S) = MeasureTheory.Measure.restrict ν (⋃₀ S) ↔ ∀ (s : Set α), s ∈ S → MeasureTheory.Measure.restrict μ s = MeasureTheory.Measure.restrict ν s

theorem MeasureTheory.Measure.restrict_sInf_eq_sInf_restrict {α : Type u_1} {t : Set α} {m0 : MeasurableSpace α} {m : Set (MeasureTheory.Measure α)} (hm : Set.Nonempty m) (ht : MeasurableSet t) : MeasureTheory.Measure.restrict (sInf m) t = sInf ((fun μ => MeasureTheory.Measure.restrict μ t) '' m)

This lemma shows that Inf and restrict commute for measures.

theorem MeasureTheory.Measure.exists_mem_of_measure_ne_zero_of_ae {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hs : ↑↑μ s ≠ 0) {p : α → Prop} (hp : ∀ᵐ (x : α) ∂MeasureTheory.Measure.restrict μ s, p x) : ∃ x, x ∈ s ∧ p x

Extensionality results

theorem MeasureTheory.Measure.ext_iff_of_iUnion_eq_univ {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [Countable ι] {s : ι → Set α} (hs : ⋃ (i : ι), s i = Set.univ) : μ = ν ↔ ∀ (i : ι), MeasureTheory.Measure.restrict μ (s i) = MeasureTheory.Measure.restrict ν (s i)

Two measures are equal if they have equal restrictions on a spanning collection of sets (formulated using Union).

theorem MeasureTheory.Measure.ext_of_iUnion_eq_univ {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [Countable ι] {s : ι → Set α} (hs : ⋃ (i : ι), s i = Set.univ) : (∀ (i : ι), MeasureTheory.Measure.restrict μ (s i) = MeasureTheory.Measure.restrict ν (s i)) → μ = ν

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

---

Two measures are equal if they have equal restrictions on a spanning collection of sets (formulated using Union).

theorem MeasureTheory.Measure.ext_iff_of_biUnion_eq_univ {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {S : Set ι} {s : ι → Set α} (hc : Set.Countable S) (hs : ⋃ (i : ι) (_ : i ∈ S), s i = Set.univ) : μ = ν ↔ ∀ (i : ι), i ∈ S → MeasureTheory.Measure.restrict μ (s i) = MeasureTheory.Measure.restrict ν (s i)

Two measures are equal if they have equal restrictions on a spanning collection of sets (formulated using biUnion).

theorem MeasureTheory.Measure.ext_of_biUnion_eq_univ {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {S : Set ι} {s : ι → Set α} (hc : Set.Countable S) (hs : ⋃ (i : ι) (_ : i ∈ S), s i = Set.univ) : (∀ (i : ι), i ∈ S → MeasureTheory.Measure.restrict μ (s i) = MeasureTheory.Measure.restrict ν (s i)) → μ = ν

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

---

Two measures are equal if they have equal restrictions on a spanning collection of sets (formulated using biUnion).

theorem MeasureTheory.Measure.ext_iff_of_sUnion_eq_univ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {S : Set (Set α)} (hc : Set.Countable S) (hs : ⋃₀ S = Set.univ) : μ = ν ↔ ∀ (s : Set α), s ∈ S → MeasureTheory.Measure.restrict μ s = MeasureTheory.Measure.restrict ν s

Two measures are equal if they have equal restrictions on a spanning collection of sets (formulated using sUnion).

theorem MeasureTheory.Measure.ext_of_sUnion_eq_univ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {S : Set (Set α)} (hc : Set.Countable S) (hs : ⋃₀ S = Set.univ) : (∀ (s : Set α), s ∈ S → MeasureTheory.Measure.restrict μ s = MeasureTheory.Measure.restrict ν s) → μ = ν

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

---

Two measures are equal if they have equal restrictions on a spanning collection of sets (formulated using sUnion).

theorem MeasureTheory.Measure.ext_of_generateFrom_of_cover {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {S : Set (Set α)} {T : Set (Set α)} (h_gen : m0 = MeasurableSpace.generateFrom S) (hc : Set.Countable T) (h_inter : IsPiSystem S) (hU : ⋃₀ T = Set.univ) (htop : ∀ (t : Set α), t ∈ T → ↑↑μ t ≠ ⊤) (ST_eq : ∀ (t : Set α), t ∈ T → ∀ (s : Set α), s ∈ S → ↑↑μ (s ∩ t) = ↑↑ν (s ∩ t)) (T_eq : ∀ (t : Set α), t ∈ T → ↑↑μ t = ↑↑ν t) : μ = ν

theorem MeasureTheory.Measure.ext_of_generateFrom_of_cover_subset {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {S : Set (Set α)} {T : Set (Set α)} (h_gen : m0 = MeasurableSpace.generateFrom S) (h_inter : IsPiSystem S) (h_sub : T ⊆ S) (hc : Set.Countable T) (hU : ⋃₀ T = Set.univ) (htop : ∀ (s : Set α), s ∈ T → ↑↑μ s ≠ ⊤) (h_eq : ∀ (s : Set α), s ∈ S → ↑↑μ s = ↑↑ν s) : μ = ν

Two measures are equal if they are equal on the π-system generating the σ-algebra, and they are both finite on an increasing spanning sequence of sets in the π-system. This lemma is formulated using sUnion.

theorem MeasureTheory.Measure.ext_of_generateFrom_of_iUnion {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} (C : Set (Set α)) (B : ℕ → Set α) (hA : m0 = MeasurableSpace.generateFrom C) (hC : IsPiSystem C) (h1B : ⋃ (i : ℕ), B i = Set.univ) (h2B : ∀ (i : ℕ), B i ∈ C) (hμB : ∀ (i : ℕ), ↑↑μ (B i) ≠ ⊤) (h_eq : ∀ (s : Set α), s ∈ C → ↑↑μ s = ↑↑ν s) : μ = ν

Two measures are equal if they are equal on the π-system generating the σ-algebra, and they are both finite on an increasing spanning sequence of sets in the π-system. This lemma is formulated using iUnion. FiniteSpanningSetsIn.ext is a reformulation of this lemma.

def MeasureTheory.Measure.sum {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} (f : ι → MeasureTheory.Measure α) : MeasureTheory.Measure α

Sum of an indexed family of measures.

Equations

• One or more equations did not get rendered due to their size.

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.le_sum {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} (μ : ι → MeasureTheory.Measure α) (i : ι) : μ i ≤ MeasureTheory.Measure.sum μ

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

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 μ = Finset.sum Finset.univ fun i => μ i

@[simp]

theorem MeasureTheory.Measure.sum_coe_finset {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} (s : Finset ι) (μ : ι → MeasureTheory.Measure α) : (MeasureTheory.Measure.sum fun i => μ ↑i) = Finset.sum s fun i => μ i

@[simp]

theorem MeasureTheory.Measure.ae_sum_eq {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} [Countable ι] (μ : ι → MeasureTheory.Measure α) : MeasureTheory.Measure.ae (MeasureTheory.Measure.sum μ) = ⨆ (i : ι), MeasureTheory.Measure.ae (μ i)

theorem MeasureTheory.Measure.sum_bool {α : Type u_1} {m0 : MeasurableSpace α} (f : Bool → MeasureTheory.Measure α) : MeasureTheory.Measure.sum f = f true + f false

theorem MeasureTheory.Measure.sum_cond {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) : (MeasureTheory.Measure.sum fun b => bif b then μ else ν) = μ + ν

@[simp]

theorem MeasureTheory.Measure.restrict_sum {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} (μ : ι → MeasureTheory.Measure α) {s : Set α} (hs : MeasurableSet s) : MeasureTheory.Measure.restrict (MeasureTheory.Measure.sum μ) s = MeasureTheory.Measure.sum fun i => MeasureTheory.Measure.restrict (μ i) s

theorem MeasureTheory.Measure.sum_of_empty {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} [IsEmpty ι] (μ : ι → MeasureTheory.Measure α) : MeasureTheory.Measure.sum μ = 0

theorem MeasureTheory.Measure.sum_add_sum_compl {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} (s : Set ι) (μ : ι → MeasureTheory.Measure α) : ((MeasureTheory.Measure.sum fun i => μ ↑i) + MeasureTheory.Measure.sum fun i => μ ↑i) = MeasureTheory.Measure.sum μ

theorem MeasureTheory.Measure.sum_congr {α : Type u_1} {m0 : MeasurableSpace α} {μ : ℕ → MeasureTheory.Measure α} {ν : ℕ → MeasureTheory.Measure α} (h : ∀ (n : ℕ), μ n = ν n) : MeasureTheory.Measure.sum μ = MeasureTheory.Measure.sum ν

theorem MeasureTheory.Measure.sum_add_sum {α : Type u_1} {m0 : MeasurableSpace α} (μ : ℕ → MeasureTheory.Measure α) (ν : ℕ → MeasureTheory.Measure α) : MeasureTheory.Measure.sum μ + MeasureTheory.Measure.sum ν = MeasureTheory.Measure.sum fun n => μ n + ν n

theorem MeasureTheory.Measure.restrict_iUnion_ae {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable ι] {s : ι → Set α} (hd : Pairwise (MeasureTheory.AEDisjoint μ on s)) (hm : ∀ (i : ι), MeasureTheory.NullMeasurableSet (s i)) : MeasureTheory.Measure.restrict μ (⋃ (i : ι), s i) = MeasureTheory.Measure.sum fun i => MeasureTheory.Measure.restrict μ (s i)

theorem MeasureTheory.Measure.restrict_iUnion {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable ι] {s : ι → Set α} (hd : Pairwise (Disjoint on s)) (hm : ∀ (i : ι), MeasurableSet (s i)) : MeasureTheory.Measure.restrict μ (⋃ (i : ι), s i) = MeasureTheory.Measure.sum fun i => MeasureTheory.Measure.restrict μ (s i)

theorem MeasureTheory.Measure.restrict_iUnion_le {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable ι] {s : ι → Set α} : MeasureTheory.Measure.restrict μ (⋃ (i : ι), s i) ≤ MeasureTheory.Measure.sum fun i => MeasureTheory.Measure.restrict μ (s i)

Absolute continuity

def MeasureTheory.Measure.AbsolutelyContinuous {α : Type u_1} {_m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) : Prop

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

Equations

• MeasureTheory.Measure.AbsolutelyContinuous μ ν = ∀ ⦃s : Set α⦄, ↑↑ν s = 0 → ↑↑μ s = 0

def MeasureTheory.«term_≪_» : Lean.TrailingParserDescr

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

Equations

• MeasureTheory.«term_≪_» = Lean.ParserDescr.trailingNode `MeasureTheory.term_≪_ 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≪ ") (Lean.ParserDescr.cat `term 51))

theorem MeasureTheory.Measure.absolutelyContinuous_of_le {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} (h : μ ≤ ν) : MeasureTheory.Measure.AbsolutelyContinuous μ ν

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

Alias of MeasureTheory.Measure.absolutelyContinuous_of_le.

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

theorem Eq.absolutelyContinuous {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} (h : μ = ν) : MeasureTheory.Measure.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) : MeasureTheory.Measure.AbsolutelyContinuous μ ν

theorem MeasureTheory.Measure.AbsolutelyContinuous.refl {α : Type u_1} {_m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) : MeasureTheory.Measure.AbsolutelyContinuous μ μ

theorem MeasureTheory.Measure.AbsolutelyContinuous.rfl {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} : MeasureTheory.Measure.AbsolutelyContinuous μ μ

instance MeasureTheory.Measure.AbsolutelyContinuous.instIsRefl {α : Type u_1} [MeasurableSpace α] : IsRefl (MeasureTheory.Measure α) fun x x_1 => MeasureTheory.Measure.AbsolutelyContinuous x x_1

Equations

• @MeasureTheory.Measure.AbsolutelyContinuous.instIsRefl = @MeasureTheory.Measure.AbsolutelyContinuous.instIsRefl.proof_1

theorem MeasureTheory.Measure.AbsolutelyContinuous.trans {α : Type u_1} {m0 : MeasurableSpace α} {μ₁ : MeasureTheory.Measure α} {μ₂ : MeasureTheory.Measure α} {μ₃ : MeasureTheory.Measure α} (h1 : MeasureTheory.Measure.AbsolutelyContinuous μ₁ μ₂) (h2 : MeasureTheory.Measure.AbsolutelyContinuous μ₂ μ₃) : MeasureTheory.Measure.AbsolutelyContinuous μ₁ μ₃

theorem MeasureTheory.Measure.AbsolutelyContinuous.map {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} (h : MeasureTheory.Measure.AbsolutelyContinuous μ ν) {f : α → β} (hf : Measurable f) : MeasureTheory.Measure.AbsolutelyContinuous (MeasureTheory.Measure.map f μ) (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 : MeasureTheory.Measure.AbsolutelyContinuous μ ν) (c : R) : MeasureTheory.Measure.AbsolutelyContinuous (c • μ) ν

theorem MeasureTheory.Measure.absolutelyContinuous_of_le_smul {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {μ' : MeasureTheory.Measure α} {c : ENNReal} (hμ'_le : μ' ≤ c • μ) : MeasureTheory.Measure.AbsolutelyContinuous μ' μ

theorem MeasureTheory.Measure.ae_le_iff_absolutelyContinuous {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} : MeasureTheory.Measure.ae μ ≤ MeasureTheory.Measure.ae ν ↔ MeasureTheory.Measure.AbsolutelyContinuous μ ν

theorem LE.le.absolutelyContinuous_of_ae {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} : MeasureTheory.Measure.ae μ ≤ MeasureTheory.Measure.ae ν → MeasureTheory.Measure.AbsolutelyContinuous μ ν

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

theorem MeasureTheory.Measure.AbsolutelyContinuous.ae_le {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} : MeasureTheory.Measure.AbsolutelyContinuous μ ν → MeasureTheory.Measure.ae μ ≤ MeasureTheory.Measure.ae ν

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

theorem MeasureTheory.Measure.ae_mono' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} : MeasureTheory.Measure.AbsolutelyContinuous μ ν → MeasureTheory.Measure.ae μ ≤ MeasureTheory.Measure.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 : MeasureTheory.Measure.AbsolutelyContinuous μ ν) {f : α → δ} {g : α → δ} (h' : f =ᶠ[MeasureTheory.Measure.ae ν] g) : f =ᶠ[MeasureTheory.Measure.ae μ] g

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

structure MeasureTheory.Measure.QuasiMeasurePreserving {α : Type u_1} {β : Type u_2} [MeasurableSpace β] {m0 : MeasurableSpace α} (f : α → β) (μa : autoParam (MeasureTheory.Measure α) _auto✝) (μb : autoParam (MeasureTheory.Measure β) _auto✝) : Prop

• measurable : Measurable f
• absolutelyContinuous : MeasureTheory.Measure.AbsolutelyContinuous (MeasureTheory.Measure.map f μa) μb

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.

theorem MeasureTheory.Measure.QuasiMeasurePreserving.id {α : Type u_1} {_m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) : MeasureTheory.Measure.QuasiMeasurePreserving id

theorem Measurable.quasiMeasurePreserving {α : Type u_1} {β : Type u_2} [MeasurableSpace β] {f : α → β} {_m0 : MeasurableSpace α} (hf : Measurable f) (μ : MeasureTheory.Measure α) : MeasureTheory.Measure.QuasiMeasurePreserving f

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) (ha : MeasureTheory.Measure.AbsolutelyContinuous μa' μa) : MeasureTheory.Measure.QuasiMeasurePreserving f

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) (ha : MeasureTheory.Measure.AbsolutelyContinuous μb μb') : MeasureTheory.Measure.QuasiMeasurePreserving f

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 : MeasureTheory.Measure.AbsolutelyContinuous μa' μa) (hb : MeasureTheory.Measure.AbsolutelyContinuous μb μb') (h : MeasureTheory.Measure.QuasiMeasurePreserving f) : MeasureTheory.Measure.QuasiMeasurePreserving f

theorem MeasureTheory.Measure.QuasiMeasurePreserving.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] [MeasurableSpace γ] {μa : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β} {μc : MeasureTheory.Measure γ} {g : β → γ} {f : α → β} (hg : MeasureTheory.Measure.QuasiMeasurePreserving g) (hf : MeasureTheory.Measure.QuasiMeasurePreserving f) : MeasureTheory.Measure.QuasiMeasurePreserving (g ∘ f)

theorem MeasureTheory.Measure.QuasiMeasurePreserving.iterate {α : Type u_1} {m0 : MeasurableSpace α} {μa : MeasureTheory.Measure α} {f : α → α} (hf : MeasureTheory.Measure.QuasiMeasurePreserving f) (n : ℕ) : MeasureTheory.Measure.QuasiMeasurePreserving f^[n]

theorem MeasureTheory.Measure.QuasiMeasurePreserving.aemeasurable {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μa : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β} {f : α → β} (hf : MeasureTheory.Measure.QuasiMeasurePreserving f) : AEMeasurable f

theorem MeasureTheory.Measure.QuasiMeasurePreserving.ae_map_le {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μa : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β} {f : α → β} (h : MeasureTheory.Measure.QuasiMeasurePreserving f) : MeasureTheory.Measure.ae (MeasureTheory.Measure.map f μa) ≤ MeasureTheory.Measure.ae μb

theorem MeasureTheory.Measure.QuasiMeasurePreserving.tendsto_ae {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μa : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β} {f : α → β} (h : MeasureTheory.Measure.QuasiMeasurePreserving f) : Filter.Tendsto f (MeasureTheory.Measure.ae μa) (MeasureTheory.Measure.ae μ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) {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) {g₁ : β → δ} {g₂ : β → δ} (hg : g₁ =ᶠ[MeasureTheory.Measure.ae μb] g₂) : g₁ ∘ f =ᶠ[MeasureTheory.Measure.ae μ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) {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) (h : s ≤ᶠ[MeasureTheory.Measure.ae μb] t) : f ⁻¹' s ≤ᶠ[MeasureTheory.Measure.ae μa] f ⁻¹' 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) (h : s =ᶠ[MeasureTheory.Measure.ae μb] t) : f ⁻¹' s =ᶠ[MeasureTheory.Measure.ae μa] f ⁻¹' t

theorem MeasureTheory.Measure.QuasiMeasurePreserving.preimage_iterate_ae_eq {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : α → α} (hf : MeasureTheory.Measure.QuasiMeasurePreserving f) (k : ℕ) (hs : f ⁻¹' s =ᶠ[MeasureTheory.Measure.ae μ] s) : f^[k] ⁻¹' s =ᶠ[MeasureTheory.Measure.ae μ] s

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 =ᶠ[MeasureTheory.Measure.ae μ] s) : ↑(e ^ k) '' s =ᶠ[MeasureTheory.Measure.ae μ] 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 =ᶠ[MeasureTheory.Measure.ae μ] s) : Filter.limsup (fun n => (Set.preimage f)^[n] s) Filter.atTop =ᶠ[MeasureTheory.Measure.ae μ] 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 =ᶠ[MeasureTheory.Measure.ae μ] s) : Filter.liminf (fun n => (Set.preimage f)^[n] s) Filter.atTop =ᶠ[MeasureTheory.Measure.ae μ] s

theorem MeasureTheory.Measure.QuasiMeasurePreserving.exists_preimage_eq_of_preimage_ae {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : α → α} (h : MeasureTheory.Measure.QuasiMeasurePreserving f) (hs : MeasurableSet s) (hs' : f ⁻¹' s =ᶠ[MeasureTheory.Measure.ae μ] s) : ∃ t, MeasurableSet t ∧ t =ᶠ[MeasureTheory.Measure.ae μ] s ∧ f ⁻¹' t = t

By replacing a measurable set that is almost invariant with the limsup of its preimages, we obtain a measurable set that is almost equal and strictly invariant.

(The liminf would work just as well.)

theorem MeasureTheory.Measure.QuasiMeasurePreserving.vadd_ae_eq_of_ae_eq {G : Type u_8} {α : Type u_9} [AddGroup G] [AddAction G α] [MeasurableSpace α] {s : Set α} {t : Set α} {μ : MeasureTheory.Measure α} (g : G) (h_qmp : MeasureTheory.Measure.QuasiMeasurePreserving ((fun x x_1 => x +ᵥ x_1) (-g))) (h_ae_eq : s =ᶠ[MeasureTheory.Measure.ae μ] t) : g +ᵥ s =ᶠ[MeasureTheory.Measure.ae μ] g +ᵥ t

theorem MeasureTheory.Measure.QuasiMeasurePreserving.smul_ae_eq_of_ae_eq {G : Type u_8} {α : Type u_9} [Group G] [MulAction G α] [MeasurableSpace α] {s : Set α} {t : Set α} {μ : MeasureTheory.Measure α} (g : G) (h_qmp : MeasureTheory.Measure.QuasiMeasurePreserving ((fun x x_1 => x • x_1) g⁻¹)) (h_ae_eq : s =ᶠ[MeasureTheory.Measure.ae μ] t) : g • s =ᶠ[MeasureTheory.Measure.ae μ] g • t

theorem MeasureTheory.Measure.pairwise_aedisjoint_of_aedisjoint_forall_ne_zero {G : Type u_8} {α : Type u_9} [AddGroup G] [AddAction G α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (h_ae_disjoint : ∀ (g : G), g ≠ 0 → MeasureTheory.AEDisjoint μ (g +ᵥ s) s) (h_qmp : ∀ (g : G), MeasureTheory.Measure.QuasiMeasurePreserving ((fun x x_1 => x +ᵥ x_1) g)) : Pairwise (MeasureTheory.AEDisjoint μ on fun g => g +ᵥ s)

theorem MeasureTheory.Measure.pairwise_aedisjoint_of_aedisjoint_forall_ne_one {G : Type u_8} {α : Type u_9} [Group G] [MulAction G α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (h_ae_disjoint : ∀ (g : G), g ≠ 1 → MeasureTheory.AEDisjoint μ (g • s) s) (h_qmp : ∀ (g : G), MeasureTheory.Measure.QuasiMeasurePreserving ((fun x x_1 => x • x_1) g)) : Pairwise (MeasureTheory.AEDisjoint μ on fun g => g • s)

The cofinite filter

def MeasureTheory.Measure.cofinite {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) : Filter α

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

Equations

• One or more equations did not get rendered due to their size.

theorem MeasureTheory.Measure.mem_cofinite {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} : s ∈ MeasureTheory.Measure.cofinite μ ↔ ↑↑μ sᶜ < ⊤

theorem MeasureTheory.Measure.compl_mem_cofinite {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} : sᶜ ∈ MeasureTheory.Measure.cofinite μ ↔ ↑↑μ s < ⊤

theorem MeasureTheory.Measure.eventually_cofinite {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : α → Prop} : (∀ᶠ (x : α) in MeasureTheory.Measure.cofinite μ, p x) ↔ ↑↑μ {x | ¬p x} < ⊤

theorem MeasureTheory.NullMeasurableSet.preimage {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → β} {t : Set β} (ht : MeasureTheory.NullMeasurableSet t) (hf : MeasureTheory.Measure.QuasiMeasurePreserving f) : MeasureTheory.NullMeasurableSet (f ⁻¹' t)

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

theorem MeasureTheory.NullMeasurableSet.mono_ac {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {s : Set α} (h : MeasureTheory.NullMeasurableSet s) (hle : MeasureTheory.Measure.AbsolutelyContinuous ν μ) : MeasureTheory.NullMeasurableSet s

theorem MeasureTheory.NullMeasurableSet.mono {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {s : Set α} (h : MeasureTheory.NullMeasurableSet s) (hle : ν ≤ μ) : MeasureTheory.NullMeasurableSet s

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) : MeasureTheory.AEDisjoint μ (f ⁻¹' s) (f ⁻¹' t)

@[simp]

theorem MeasureTheory.ae_eq_bot {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} : MeasureTheory.Measure.ae μ = ⊥ ↔ μ = 0

@[simp]

theorem MeasureTheory.ae_neBot {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} : Filter.NeBot (MeasureTheory.Measure.ae μ) ↔ μ ≠ 0

instance MeasureTheory.Measure.ae.neBot {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NeZero μ] : Filter.NeBot (MeasureTheory.Measure.ae μ)

Equations

• @MeasureTheory.Measure.ae.neBot = @MeasureTheory.Measure.ae.neBot.proof_1

@[simp]

theorem MeasureTheory.ae_zero {α : Type u_1} {_m0 : MeasurableSpace α} : MeasureTheory.Measure.ae 0 = ⊥

theorem MeasureTheory.ae_mono {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} (h : μ ≤ ν) : MeasureTheory.Measure.ae μ ≤ MeasureTheory.Measure.ae ν

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) : s ∈ MeasureTheory.Measure.ae (MeasureTheory.Measure.map f μ) ↔ f ⁻¹' s ∈ MeasureTheory.Measure.ae μ

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.Measure.ae (MeasureTheory.Measure.map f μ)) : f ⁻¹' s ∈ MeasureTheory.Measure.ae μ

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

@[simp]

theorem MeasureTheory.ae_restrict_iUnion_eq {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable ι] (s : ι → Set α) : MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ (⋃ (i : ι), s i)) = ⨆ (i : ι), MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ (s i))

@[simp]

theorem MeasureTheory.ae_restrict_union_eq {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Set α) (t : Set α) : MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ (s ∪ t)) = MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ s) ⊔ MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ t)

theorem MeasureTheory.ae_restrict_biUnion_eq {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : ι → Set α) {t : Set ι} (ht : Set.Countable t) : MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ (⋃ (i : ι) (_ : i ∈ t), s i)) = ⨆ (i : ι) (_ : i ∈ t), MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ (s i))

theorem MeasureTheory.ae_restrict_biUnion_finset_eq {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : ι → Set α) (t : Finset ι) : MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ (⋃ (i : ι) (_ : i ∈ t), s i)) = ⨆ (i : ι) (_ : i ∈ t), MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ (s i))

theorem MeasureTheory.ae_restrict_iUnion_iff {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable ι] (s : ι → Set α) (p : α → Prop) : (∀ᵐ (x : α) ∂MeasureTheory.Measure.restrict μ (⋃ (i : ι), s i), p x) ↔ ∀ (i : ι), ∀ᵐ (x : α) ∂MeasureTheory.Measure.restrict μ (s i), p x

theorem MeasureTheory.ae_restrict_union_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Set α) (t : Set α) (p : α → Prop) : (∀ᵐ (x : α) ∂MeasureTheory.Measure.restrict μ (s ∪ t), p x) ↔ (∀ᵐ (x : α) ∂MeasureTheory.Measure.restrict μ s, p x) ∧ ∀ᵐ (x : α) ∂MeasureTheory.Measure.restrict μ t, p x

theorem MeasureTheory.ae_restrict_biUnion_iff {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : ι → Set α) {t : Set ι} (ht : Set.Countable t) (p : α → Prop) : (∀ᵐ (x : α) ∂MeasureTheory.Measure.restrict μ (⋃ (i : ι) (_ : i ∈ t), s i), p x) ↔ ∀ (i : ι), i ∈ t → ∀ᵐ (x : α) ∂MeasureTheory.Measure.restrict μ (s i), p x

@[simp]

theorem MeasureTheory.ae_restrict_biUnion_finset_iff {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : ι → Set α) (t : Finset ι) (p : α → Prop) : (∀ᵐ (x : α) ∂MeasureTheory.Measure.restrict μ (⋃ (i : ι) (_ : i ∈ t), s i), p x) ↔ ∀ (i : ι), i ∈ t → ∀ᵐ (x : α) ∂MeasureTheory.Measure.restrict μ (s i), p x

theorem MeasureTheory.ae_eq_restrict_iUnion_iff {α : Type u_1} {δ : Type u_4} {ι : Type u_5} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable ι] (s : ι → Set α) (f : α → δ) (g : α → δ) : f =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ (⋃ (i : ι), s i))] g ↔ ∀ (i : ι), f =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ (s i))] g

theorem MeasureTheory.ae_eq_restrict_biUnion_iff {α : Type u_1} {δ : Type u_4} {ι : Type u_5} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : ι → Set α) {t : Set ι} (ht : Set.Countable t) (f : α → δ) (g : α → δ) : f =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ (⋃ (i : ι) (_ : i ∈ t), s i))] g ↔ ∀ (i : ι), i ∈ t → f =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ (s i))] g

theorem MeasureTheory.ae_eq_restrict_biUnion_finset_iff {α : Type u_1} {δ : Type u_4} {ι : Type u_5} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : ι → Set α) (t : Finset ι) (f : α → δ) (g : α → δ) : f =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ (⋃ (i : ι) (_ : i ∈ t), s i))] g ↔ ∀ (i : ι), i ∈ t → f =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ (s i))] g

theorem MeasureTheory.ae_restrict_uIoc_eq {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [LinearOrder α] (a : α) (b : α) : MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ (Ι a b)) = MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ (Set.Ioc a b)) ⊔ MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ (Set.Ioc b a))

theorem MeasureTheory.ae_restrict_uIoc_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [LinearOrder α] {a : α} {b : α} {P : α → Prop} : (∀ᵐ (x : α) ∂MeasureTheory.Measure.restrict μ (Ι a b), P x) ↔ (∀ᵐ (x : α) ∂MeasureTheory.Measure.restrict μ (Set.Ioc a b), P x) ∧ ∀ᵐ (x : α) ∂MeasureTheory.Measure.restrict μ (Set.Ioc b a), P x

See also MeasureTheory.ae_uIoc_iff.

theorem MeasureTheory.ae_restrict_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {p : α → Prop} (hp : MeasurableSet {x | p x}) : (∀ᵐ (x : α) ∂MeasureTheory.Measure.restrict μ s, p x) ↔ ∀ᵐ (x : α) ∂μ, x ∈ s → p x

theorem MeasureTheory.ae_imp_of_ae_restrict {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {p : α → Prop} (h : ∀ᵐ (x : α) ∂MeasureTheory.Measure.restrict μ s, p x) : ∀ᵐ (x : α) ∂μ, x ∈ s → p x

theorem MeasureTheory.ae_restrict_iff' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {p : α → Prop} (hs : MeasurableSet s) : (∀ᵐ (x : α) ∂MeasureTheory.Measure.restrict μ s, p x) ↔ ∀ᵐ (x : α) ∂μ, x ∈ s → p x

theorem Filter.EventuallyEq.restrict {α : Type u_1} {δ : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → δ} {g : α → δ} {s : Set α} (hfg : f =ᶠ[MeasureTheory.Measure.ae μ] g) : f =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ s)] g

theorem MeasureTheory.ae_restrict_mem {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) : ∀ᵐ (x : α) ∂MeasureTheory.Measure.restrict μ s, x ∈ s

theorem MeasureTheory.ae_restrict_mem₀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasureTheory.NullMeasurableSet s) : ∀ᵐ (x : α) ∂MeasureTheory.Measure.restrict μ s, x ∈ s

theorem MeasureTheory.ae_restrict_of_ae {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {p : α → Prop} (h : ∀ᵐ (x : α) ∂μ, p x) : ∀ᵐ (x : α) ∂MeasureTheory.Measure.restrict μ s, p x

theorem MeasureTheory.ae_restrict_iff'₀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {p : α → Prop} (hs : MeasureTheory.NullMeasurableSet s) : (∀ᵐ (x : α) ∂MeasureTheory.Measure.restrict μ s, p x) ↔ ∀ᵐ (x : α) ∂μ, x ∈ s → p x

theorem MeasureTheory.ae_restrict_of_ae_restrict_of_subset {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} {p : α → Prop} (hst : s ⊆ t) (h : ∀ᵐ (x : α) ∂MeasureTheory.Measure.restrict μ t, p x) : ∀ᵐ (x : α) ∂MeasureTheory.Measure.restrict μ s, p x

theorem MeasureTheory.ae_of_ae_restrict_of_ae_restrict_compl {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (t : Set α) {p : α → Prop} (ht : ∀ᵐ (x : α) ∂MeasureTheory.Measure.restrict μ t, p x) (htc : ∀ᵐ (x : α) ∂MeasureTheory.Measure.restrict μ tᶜ, p x) : ∀ᵐ (x : α) ∂μ, p x

theorem MeasureTheory.mem_map_restrict_ae_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_8} {s : Set α} {t : Set β} {f : α → β} (hs : MeasurableSet s) : t ∈ Filter.map f (MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ s)) ↔ ↑↑μ ((f ⁻¹' t)ᶜ ∩ s) = 0

theorem MeasureTheory.ae_smul_measure {α : Type u_1} {R : Type u_6} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : α → Prop} [Monoid R] [DistribMulAction R ENNReal] [IsScalarTower R ENNReal ENNReal] (h : ∀ᵐ (x : α) ∂μ, p x) (c : R) : ∀ᵐ (x : α) ∂c • μ, p x

theorem MeasureTheory.ae_add_measure_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : α → Prop} {ν : MeasureTheory.Measure α} : (∀ᵐ (x : α) ∂μ + ν, p x) ↔ (∀ᵐ (x : α) ∂μ, p x) ∧ ∀ᵐ (x : α) ∂ν, p x

theorem MeasureTheory.ae_eq_comp' {α : Type u_1} {β : Type u_2} {δ : Type u_4} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → β} {g : β → δ} {g' : β → δ} (hf : AEMeasurable f) (h : g =ᶠ[MeasureTheory.Measure.ae ν] g') (h2 : MeasureTheory.Measure.AbsolutelyContinuous (MeasureTheory.Measure.map f μ) ν) : g ∘ f =ᶠ[MeasureTheory.Measure.ae μ] g' ∘ f

theorem MeasureTheory.Measure.QuasiMeasurePreserving.ae_eq_comp {α : Type u_1} {β : Type u_2} {δ : Type u_4} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → β} {g : β → δ} {g' : β → δ} (hf : MeasureTheory.Measure.QuasiMeasurePreserving f) (h : g =ᶠ[MeasureTheory.Measure.ae ν] g') : g ∘ f =ᶠ[MeasureTheory.Measure.ae μ] g' ∘ f

theorem MeasureTheory.ae_eq_comp {α : Type u_1} {β : Type u_2} {δ : Type u_4} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : α → β} {g : β → δ} {g' : β → δ} (hf : AEMeasurable f) (h : g =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.map f μ)] g') : g ∘ f =ᶠ[MeasureTheory.Measure.ae μ] g' ∘ f

theorem MeasureTheory.sub_ae_eq_zero {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_8} [AddGroup β] (f : α → β) (g : α → β) : f - g =ᶠ[MeasureTheory.Measure.ae μ] 0 ↔ f =ᶠ[MeasureTheory.Measure.ae μ] g

theorem MeasureTheory.le_ae_restrict {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} : MeasureTheory.Measure.ae μ ⊓ Filter.principal s ≤ MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ s)

@[simp]

theorem MeasureTheory.ae_restrict_eq {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) : MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ s) = MeasureTheory.Measure.ae μ ⊓ Filter.principal s

theorem MeasureTheory.ae_restrict_eq_bot {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} : MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ s) = ⊥ ↔ ↑↑μ s = 0

theorem MeasureTheory.ae_restrict_neBot {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} : Filter.NeBot (MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ s)) ↔ ↑↑μ s ≠ 0

theorem MeasureTheory.self_mem_ae_restrict {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) : s ∈ MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ s)

theorem MeasureTheory.ae_restrict_of_ae_eq_of_ae_restrict {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : α → Prop} {t : α → Prop} (hst : s =ᶠ[MeasureTheory.Measure.ae μ] t) {p : α → Prop} : (∀ᵐ (x : α) ∂MeasureTheory.Measure.restrict μ s, p x) → ∀ᵐ (x : α) ∂MeasureTheory.Measure.restrict μ t, p x

If two measurable sets are ae_eq then any proposition that is almost everywhere true on one is almost everywhere true on the other

theorem MeasureTheory.ae_restrict_congr_set {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : α → Prop} {t : α → Prop} (hst : s =ᶠ[MeasureTheory.Measure.ae μ] t) {p : α → Prop} : (∀ᵐ (x : α) ∂MeasureTheory.Measure.restrict μ s, p x) ↔ ∀ᵐ (x : α) ∂MeasureTheory.Measure.restrict μ t, p x

If two measurable sets are ae_eq then any proposition that is almost everywhere true on one is almost everywhere true on the other

theorem MeasureTheory.measure_setOf_frequently_eq_zero {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : ℕ → α → Prop} (hp : ∑' (i : ℕ), ↑↑μ {x | p i x} ≠ ⊤) : ↑↑μ {x | ∃ᶠ (n : ℕ) in Filter.atTop, p n x} = 0

A version of the Borel-Cantelli lemma: if pᵢ is a sequence of predicates such that ∑ μ {x | pᵢ x} is finite, then the measure of x such that pᵢ x holds frequently as i → ∞ (or equivalently, pᵢ x holds for infinitely many i) is equal to zero.

theorem MeasureTheory.ae_eventually_not_mem {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : ℕ → Set α} (hs : ∑' (i : ℕ), ↑↑μ (s i) ≠ ⊤) : ∀ᵐ (x : α) ∂μ, ∀ᶠ (n : ℕ) in Filter.atTop, ¬x ∈ s n

A version of the Borel-Cantelli lemma: if sᵢ is a sequence of sets such that ∑ μ sᵢ exists, then for almost all x, x does not belong to almost all sᵢ.

theorem MeasureTheory.NullMeasurable.measure_preimage_eq_measure_restrict_preimage_of_ae_compl_eq_const {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_8} [MeasurableSpace β] {b : β} {f : α → β} {s : Set α} (f_mble : MeasureTheory.NullMeasurable f) (hs : f =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ sᶜ)] fun x => b) {t : Set β} (t_mble : MeasurableSet t) (ht : ¬b ∈ t) : ↑↑μ (f ⁻¹' t) = ↑↑(MeasureTheory.Measure.restrict μ s) (f ⁻¹' t)

theorem MeasureTheory.biSup_measure_Iic {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Preorder α] {s : Set α} (hsc : Set.Countable s) (hst : ∀ (x : α), ∃ y, y ∈ s ∧ x ≤ y) (hdir : DirectedOn (fun x x_1 => x ≤ x_1) s) : ⨆ (x : α) (_ : x ∈ s), ↑↑μ (Set.Iic x) = ↑↑μ Set.univ

theorem MeasureTheory.tendsto_measure_Ico_atTop {α : Type u_1} {m0 : MeasurableSpace α} [SemilatticeSup α] [NoMaxOrder α] [Filter.IsCountablyGenerated Filter.atTop] (μ : 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 α} [SemilatticeInf α] [NoMinOrder α] [Filter.IsCountablyGenerated Filter.atBot] (μ : 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 α} [SemilatticeSup α] [Filter.IsCountablyGenerated Filter.atTop] (μ : 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 α} [SemilatticeInf α] [h : Filter.IsCountablyGenerated Filter.atBot] (μ : 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) : Set.Iio a =ᶠ[MeasureTheory.Measure.ae μ] Set.Iic a

theorem MeasureTheory.Ioi_ae_eq_Ici' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [PartialOrder α] {a : α} (ha : ↑↑μ {a} = 0) : Set.Ioi a =ᶠ[MeasureTheory.Measure.ae μ] Set.Ici a

theorem MeasureTheory.Ioo_ae_eq_Ioc' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [PartialOrder α] {a : α} {b : α} (hb : ↑↑μ {b} = 0) : Set.Ioo a b =ᶠ[MeasureTheory.Measure.ae μ] Set.Ioc a b

theorem MeasureTheory.Ioc_ae_eq_Icc' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [PartialOrder α] {a : α} {b : α} (ha : ↑↑μ {a} = 0) : Set.Ioc a b =ᶠ[MeasureTheory.Measure.ae μ] Set.Icc a b

theorem MeasureTheory.Ioo_ae_eq_Ico' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [PartialOrder α] {a : α} {b : α} (ha : ↑↑μ {a} = 0) : Set.Ioo a b =ᶠ[MeasureTheory.Measure.ae μ] Set.Ico a b

theorem MeasureTheory.Ioo_ae_eq_Icc' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [PartialOrder α] {a : α} {b : α} (ha : ↑↑μ {a} = 0) (hb : ↑↑μ {b} = 0) : Set.Ioo a b =ᶠ[MeasureTheory.Measure.ae μ] Set.Icc a b

theorem MeasureTheory.Ico_ae_eq_Icc' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [PartialOrder α] {a : α} {b : α} (hb : ↑↑μ {b} = 0) : Set.Ico a b =ᶠ[MeasureTheory.Measure.ae μ] Set.Icc a b

theorem MeasureTheory.Ico_ae_eq_Ioc' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [PartialOrder α] {a : α} {b : α} (ha : ↑↑μ {a} = 0) (hb : ↑↑μ {b} = 0) : Set.Ico a b =ᶠ[MeasureTheory.Measure.ae μ] Set.Ioc a b

class MeasureTheory.IsFiniteMeasure {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) : Prop

• measure_univ_lt_top : ↑↑μ Set.univ < ⊤

A measure μ is called finite if μ univ < ∞.

theorem MeasureTheory.not_isFiniteMeasure_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} : ¬MeasureTheory.IsFiniteMeasure μ ↔ ↑↑μ Set.univ = ⊤

instance MeasureTheory.Restrict.isFiniteMeasure {α : Type u_1} {m0 : MeasurableSpace α} {s : Set α} (μ : MeasureTheory.Measure α) [hs : Fact (↑↑μ s < ⊤)] : MeasureTheory.IsFiniteMeasure (MeasureTheory.Measure.restrict μ s)

Equations

• @MeasureTheory.Restrict.isFiniteMeasure = @MeasureTheory.Restrict.isFiniteMeasure.proof_1

theorem MeasureTheory.measure_lt_top {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (s : Set α) : ↑↑μ s < ⊤

instance MeasureTheory.isFiniteMeasureRestrict {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (s : Set α) [h : MeasureTheory.IsFiniteMeasure μ] : MeasureTheory.IsFiniteMeasure (MeasureTheory.Measure.restrict μ s)

Equations

• @MeasureTheory.isFiniteMeasureRestrict = @MeasureTheory.isFiniteMeasureRestrict.proof_1

theorem MeasureTheory.measure_ne_top {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (s : Set α) : ↑↑μ s ≠ ⊤

theorem MeasureTheory.measure_compl_le_add_of_le_add {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} [MeasureTheory.IsFiniteMeasure μ] (hs : MeasurableSet s) (ht : MeasurableSet t) {ε : ENNReal} (h : ↑↑μ s ≤ ↑↑μ t + ε) : ↑↑μ tᶜ ≤ ↑↑μ sᶜ + ε

theorem MeasureTheory.measure_compl_le_add_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} [MeasureTheory.IsFiniteMeasure μ] (hs : MeasurableSet s) (ht : MeasurableSet t) {ε : ENNReal} : ↑↑μ sᶜ ≤ ↑↑μ tᶜ + ε ↔ ↑↑μ t ≤ ↑↑μ s + ε

def MeasureTheory.measureUnivNNReal {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) : NNReal

The measure of the whole space with respect to a finite measure, considered as ℝ≥0.

Equations

• MeasureTheory.measureUnivNNReal μ = ENNReal.toNNReal (↑↑μ Set.univ)

@[simp]

theorem MeasureTheory.coe_measureUnivNNReal {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] : ↑(MeasureTheory.measureUnivNNReal μ) = ↑↑μ Set.univ

instance MeasureTheory.isFiniteMeasureZero {α : Type u_1} {m0 : MeasurableSpace α} : MeasureTheory.IsFiniteMeasure 0

Equations

• @MeasureTheory.isFiniteMeasureZero = @MeasureTheory.isFiniteMeasureZero.proof_1

instance MeasureTheory.isFiniteMeasureOfIsEmpty {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [IsEmpty α] : MeasureTheory.IsFiniteMeasure μ

Equations

• @MeasureTheory.isFiniteMeasureOfIsEmpty = @MeasureTheory.isFiniteMeasureOfIsEmpty.proof_1

@[simp]

theorem MeasureTheory.measureUnivNNReal_zero {α : Type u_1} {m0 : MeasurableSpace α} : MeasureTheory.measureUnivNNReal 0 = 0

instance MeasureTheory.isFiniteMeasureAdd {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] : MeasureTheory.IsFiniteMeasure (μ + ν)

Equations

• @MeasureTheory.isFiniteMeasureAdd = @MeasureTheory.isFiniteMeasureAdd.proof_1

instance MeasureTheory.isFiniteMeasureSMulNNReal {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {r : NNReal} : MeasureTheory.IsFiniteMeasure (r • μ)

Equations

• @MeasureTheory.isFiniteMeasureSMulNNReal = @MeasureTheory.isFiniteMeasureSMulNNReal.proof_1

instance MeasureTheory.IsFiniteMeasure.average {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} : MeasureTheory.IsFiniteMeasure ((↑↑μ Set.univ)⁻¹ • μ)

Equations

• @MeasureTheory.IsFiniteMeasure.average = @MeasureTheory.IsFiniteMeasure.average.proof_1

instance MeasureTheory.isFiniteMeasureSMulOfNNRealTower {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {R : Type u_8} [SMul R NNReal] [SMul R ENNReal] [IsScalarTower R NNReal ENNReal] [IsScalarTower R ENNReal ENNReal] [MeasureTheory.IsFiniteMeasure μ] {r : R} : MeasureTheory.IsFiniteMeasure (r • μ)

Equations

• @MeasureTheory.isFiniteMeasureSMulOfNNRealTower = @MeasureTheory.isFiniteMeasureSMulOfNNRealTower.proof_1

theorem MeasureTheory.isFiniteMeasure_of_le {α : Type u_1} {m0 : MeasurableSpace α} {ν : MeasureTheory.Measure α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (h : ν ≤ μ) : MeasureTheory.IsFiniteMeasure ν

theorem MeasureTheory.Measure.isFiniteMeasure_map {α : Type u_1} {β : Type u_2} [MeasurableSpace β] {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (f : α → β) : MeasureTheory.IsFiniteMeasure (MeasureTheory.Measure.map f μ)

@[simp]

theorem MeasureTheory.measureUnivNNReal_eq_zero {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] : MeasureTheory.measureUnivNNReal μ = 0 ↔ μ = 0

theorem MeasureTheory.measureUnivNNReal_pos {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] (hμ : μ ≠ 0) : 0 < MeasureTheory.measureUnivNNReal μ

theorem MeasureTheory.Measure.le_of_add_le_add_left {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν₁ : MeasureTheory.Measure α} {ν₂ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] (A2 : μ + ν₁ ≤ μ + ν₂) : ν₁ ≤ ν₂

le_of_add_le_add_left is normally applicable to OrderedCancelAddCommMonoid, but it holds for measures with the additional assumption that μ is finite.

theorem MeasureTheory.summable_measure_toReal {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [hμ : MeasureTheory.IsFiniteMeasure μ] {f : ℕ → Set α} (hf₁ : ∀ (i : ℕ), MeasurableSet (f i)) (hf₂ : Pairwise (Disjoint on f)) : Summable fun x => ENNReal.toReal (↑↑μ (f x))

theorem MeasureTheory.ae_eq_univ_iff_measure_eq {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsFiniteMeasure μ] (hs : MeasureTheory.NullMeasurableSet s) : s =ᶠ[MeasureTheory.Measure.ae μ] Set.univ ↔ ↑↑μ s = ↑↑μ Set.univ

theorem MeasureTheory.ae_iff_measure_eq {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {p : α → Prop} (hp : MeasureTheory.NullMeasurableSet {a | p a}) : (∀ᵐ (a : α) ∂μ, p a) ↔ ↑↑μ {a | p a} = ↑↑μ Set.univ

theorem MeasureTheory.ae_mem_iff_measure_eq {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {s : Set α} (hs : MeasureTheory.NullMeasurableSet s) : (∀ᵐ (a : α) ∂μ, a ∈ s) ↔ ↑↑μ s = ↑↑μ Set.univ

theorem MeasureTheory.abs_toReal_measure_sub_le_measure_symmDiff' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (hs : MeasurableSet s) (ht : MeasurableSet t) (hs' : ↑↑μ s ≠ ⊤) (ht' : ↑↑μ t ≠ ⊤) : |ENNReal.toReal (↑↑μ s) - ENNReal.toReal (↑↑μ t)| ≤ ENNReal.toReal (↑↑μ (s ∆ t))

theorem MeasureTheory.abs_toReal_measure_sub_le_measure_symmDiff {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} [MeasureTheory.IsFiniteMeasure μ] (hs : MeasurableSet s) (ht : MeasurableSet t) : |ENNReal.toReal (↑↑μ s) - ENNReal.toReal (↑↑μ t)| ≤ ENNReal.toReal (↑↑μ (s ∆ t))

class MeasureTheory.IsProbabilityMeasure {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) : Prop

• measure_univ : ↑↑μ Set.univ = 1

A measure μ is called a probability measure if μ univ = 1.

instance MeasureTheory.IsProbabilityMeasure.toIsFiniteMeasure {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] : MeasureTheory.IsFiniteMeasure μ

Equations

• @MeasureTheory.IsProbabilityMeasure.toIsFiniteMeasure = @MeasureTheory.IsProbabilityMeasure.toIsFiniteMeasure.proof_1

theorem MeasureTheory.IsProbabilityMeasure.ne_zero {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] : μ ≠ 0

instance MeasureTheory.IsProbabilityMeasure.neZero {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] : NeZero μ

Equations

• @MeasureTheory.IsProbabilityMeasure.neZero = @MeasureTheory.IsProbabilityMeasure.neZero.proof_1

theorem MeasureTheory.IsProbabilityMeasure.ae_neBot {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] : Filter.NeBot (MeasureTheory.Measure.ae μ)

theorem MeasureTheory.prob_add_prob_compl {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsProbabilityMeasure μ] (h : MeasurableSet s) : ↑↑μ s + ↑↑μ sᶜ = 1

theorem MeasureTheory.prob_le_one {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsProbabilityMeasure μ] : ↑↑μ s ≤ 1

instance MeasureTheory.isProbabilityMeasureSMul {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [NeZero μ] : MeasureTheory.IsProbabilityMeasure ((↑↑μ Set.univ)⁻¹ • μ)

Equations

• @MeasureTheory.isProbabilityMeasureSMul = @MeasureTheory.isProbabilityMeasureSMul.proof_1

theorem MeasureTheory.isProbabilityMeasure_map {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {f : α → β} (hf : AEMeasurable f) : MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.map f μ)

@[simp]

theorem MeasureTheory.one_le_prob_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsProbabilityMeasure μ] : 1 ≤ ↑↑μ s ↔ ↑↑μ s = 1

theorem MeasureTheory.prob_compl_eq_one_sub {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsProbabilityMeasure μ] (hs : MeasurableSet s) : ↑↑μ sᶜ = 1 - ↑↑μ s

Note that this is not quite as useful as it looks because the measure takes values in ℝ≥0∞. Thus the subtraction appearing is the truncated subtraction of ℝ≥0∞, rather than the better-behaved subtraction of ℝ.

@[simp]

theorem MeasureTheory.prob_compl_eq_zero_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsProbabilityMeasure μ] (hs : MeasurableSet s) : ↑↑μ sᶜ = 0 ↔ ↑↑μ s = 1

@[simp]

theorem MeasureTheory.prob_compl_eq_one_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsProbabilityMeasure μ] (hs : MeasurableSet s) : ↑↑μ sᶜ = 1 ↔ ↑↑μ s = 0

class MeasureTheory.NoAtoms {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) : Prop

• measure_singleton : ∀ (x : α), ↑↑μ {x} = 0

Measure μ has no atoms if the measure of each singleton is zero.

NB: Wikipedia assumes that for any measurable set s with positive μ-measure, there exists a measurable t ⊆ s such that 0 < μ t < μ s. While this implies μ {x} = 0, the converse is not true.

theorem Set.Subsingleton.measure_zero {α : Type u_8} {_m : MeasurableSpace α} {s : Set α} (hs : Set.Subsingleton s) (μ : MeasureTheory.Measure α) [MeasureTheory.NoAtoms μ] : ↑↑μ s = 0

theorem MeasureTheory.Measure.restrict_singleton' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] {a : α} : MeasureTheory.Measure.restrict μ {a} = 0

instance MeasureTheory.Measure.restrict.instNoAtoms {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] (s : Set α) : MeasureTheory.NoAtoms (MeasureTheory.Measure.restrict μ s)

Equations

• @MeasureTheory.Measure.restrict.instNoAtoms = @MeasureTheory.Measure.restrict.instNoAtoms.proof_1

theorem Set.Countable.measure_zero {α : Type u_8} {m : MeasurableSpace α} {s : Set α} (h : Set.Countable s) (μ : MeasureTheory.Measure α) [MeasureTheory.NoAtoms μ] : ↑↑μ s = 0

theorem Set.Countable.ae_not_mem {α : Type u_8} {m : MeasurableSpace α} {s : Set α} (h : Set.Countable s) (μ : MeasureTheory.Measure α) [MeasureTheory.NoAtoms μ] : ∀ᵐ (x : α) ∂μ, ¬x ∈ s

theorem Set.Finite.measure_zero {α : Type u_8} {_m : MeasurableSpace α} {s : Set α} (h : Set.Finite s) (μ : MeasureTheory.Measure α) [MeasureTheory.NoAtoms μ] : ↑↑μ s = 0

theorem Finset.measure_zero {α : Type u_8} {_m : MeasurableSpace α} (s : Finset α) (μ : MeasureTheory.Measure α) [MeasureTheory.NoAtoms μ] : ↑↑μ ↑s = 0

theorem MeasureTheory.insert_ae_eq_self {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] (a : α) (s : Set α) : insert a s =ᶠ[MeasureTheory.Measure.ae μ] s

theorem MeasureTheory.Iio_ae_eq_Iic {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] [PartialOrder α] {a : α} : Set.Iio a =ᶠ[MeasureTheory.Measure.ae μ] Set.Iic a

theorem MeasureTheory.Ioi_ae_eq_Ici {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] [PartialOrder α] {a : α} : Set.Ioi a =ᶠ[MeasureTheory.Measure.ae μ] Set.Ici a

theorem MeasureTheory.Ioo_ae_eq_Ioc {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] [PartialOrder α] {a : α} {b : α} : Set.Ioo a b =ᶠ[MeasureTheory.Measure.ae μ] Set.Ioc a b

theorem MeasureTheory.Ioc_ae_eq_Icc {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] [PartialOrder α] {a : α} {b : α} : Set.Ioc a b =ᶠ[MeasureTheory.Measure.ae μ] Set.Icc a b

theorem MeasureTheory.Ioo_ae_eq_Ico {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] [PartialOrder α] {a : α} {b : α} : Set.Ioo a b =ᶠ[MeasureTheory.Measure.ae μ] Set.Ico a b

theorem MeasureTheory.Ioo_ae_eq_Icc {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] [PartialOrder α] {a : α} {b : α} : Set.Ioo a b =ᶠ[MeasureTheory.Measure.ae μ] Set.Icc a b

theorem MeasureTheory.Ico_ae_eq_Icc {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] [PartialOrder α] {a : α} {b : α} : Set.Ico a b =ᶠ[MeasureTheory.Measure.ae μ] Set.Icc a b

theorem MeasureTheory.Ico_ae_eq_Ioc {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] [PartialOrder α] {a : α} {b : α} : Set.Ico a b =ᶠ[MeasureTheory.Measure.ae μ] Set.Ioc a b

theorem MeasureTheory.uIoc_ae_eq_interval {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NoAtoms μ] [LinearOrder α] {a : α} {b : α} : Ι a b =ᶠ[MeasureTheory.Measure.ae μ] Set.uIcc a b

theorem MeasureTheory.ite_ae_eq_of_measure_zero {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {γ : Type u_8} (f : α → γ) (g : α → γ) (s : Set α) (hs_zero : ↑↑μ s = 0) : (fun x => if x ∈ s then f x else g x) =ᶠ[MeasureTheory.Measure.ae μ] g

theorem MeasureTheory.ite_ae_eq_of_measure_compl_zero {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {γ : Type u_8} (f : α → γ) (g : α → γ) (s : Set α) (hs_zero : ↑↑μ sᶜ = 0) : (fun x => if x ∈ s then f x else g x) =ᶠ[MeasureTheory.Measure.ae μ] f

def MeasureTheory.Measure.FiniteAtFilter {α : Type u_1} {_m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : Filter α) : Prop

A measure is called finite at filter f if it is finite at some set s ∈ f. Equivalently, it is eventually finite at s in f.small_sets.

Equations

• MeasureTheory.Measure.FiniteAtFilter μ f = ∃ s, s ∈ f ∧ ↑↑μ s < ⊤

theorem MeasureTheory.Measure.finiteAtFilter_of_finite {α : Type u_1} {_m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (f : Filter α) : MeasureTheory.Measure.FiniteAtFilter μ f

theorem MeasureTheory.Measure.FiniteAtFilter.exists_mem_basis {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : Filter α} (hμ : MeasureTheory.Measure.FiniteAtFilter μ f) {p : ι → Prop} {s : ι → Set α} (hf : Filter.HasBasis f p s) : ∃ i, p i ∧ ↑↑μ (s i) < ⊤

theorem MeasureTheory.Measure.finiteAtBot {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) : MeasureTheory.Measure.FiniteAtFilter μ ⊥

structure MeasureTheory.Measure.FiniteSpanningSetsIn {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (C : Set (Set α)) : Type u_1

• set : ℕ → Set α
• set_mem : ∀ (i : ℕ), MeasureTheory.Measure.FiniteSpanningSetsIn.set s i ∈ C
• finite : ∀ (i : ℕ), ↑↑μ (MeasureTheory.Measure.FiniteSpanningSetsIn.set s i) < ⊤
• spanning : ⋃ (i : ℕ), MeasureTheory.Measure.FiniteSpanningSetsIn.set s i = Set.univ

μ has finite spanning sets in C if there is a countable sequence of sets in C that have finite measures. This structure is a type, which is useful if we want to record extra properties about the sets, such as that they are monotone. SigmaFinite is defined in terms of this: μ is σ-finite if there exists a sequence of finite spanning sets in the collection of all measurable sets.

class MeasureTheory.SigmaFinite {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) : Prop

• out' : Nonempty (MeasureTheory.Measure.FiniteSpanningSetsIn μ Set.univ)

A measure μ is called σ-finite if there is a countable collection of sets { A i | i ∈ ℕ } such that μ (A i) < ∞ and ⋃ i, A i = s.

theorem MeasureTheory.sigmaFinite_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} : MeasureTheory.SigmaFinite μ ↔ Nonempty (MeasureTheory.Measure.FiniteSpanningSetsIn μ Set.univ)

theorem MeasureTheory.SigmaFinite.out {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (h : MeasureTheory.SigmaFinite μ) : Nonempty (MeasureTheory.Measure.FiniteSpanningSetsIn μ Set.univ)

def MeasureTheory.Measure.toFiniteSpanningSetsIn {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [h : MeasureTheory.SigmaFinite μ] : MeasureTheory.Measure.FiniteSpanningSetsIn μ {s | MeasurableSet s}

If μ is σ-finite it has finite spanning sets in the collection of all measurable sets.

Equations

• One or more equations did not get rendered due to their size.

def MeasureTheory.spanningSets {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] (i : ℕ) : Set α

A noncomputable way to get a monotone collection of sets that span univ and have finite measure using Classical.choose. This definition satisfies monotonicity in addition to all other properties in SigmaFinite.

Equations

• MeasureTheory.spanningSets μ i = Set.Accumulate (MeasureTheory.Measure.toFiniteSpanningSetsIn μ).set i

theorem MeasureTheory.monotone_spanningSets {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] : Monotone (MeasureTheory.spanningSets μ)

theorem MeasureTheory.measurable_spanningSets {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] (i : ℕ) : MeasurableSet (MeasureTheory.spanningSets μ i)

theorem MeasureTheory.measure_spanningSets_lt_top {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] (i : ℕ) : ↑↑μ (MeasureTheory.spanningSets μ i) < ⊤

theorem MeasureTheory.iUnion_spanningSets {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] : ⋃ (i : ℕ), MeasureTheory.spanningSets μ i = Set.univ

theorem MeasureTheory.isCountablySpanning_spanningSets {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] : IsCountablySpanning (Set.range (MeasureTheory.spanningSets μ))

def MeasureTheory.spanningSetsIndex {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] (x : α) : ℕ

spanningSetsIndex μ x is the least n : ℕ such that x ∈ spanningSets μ n.

Equations

• MeasureTheory.spanningSetsIndex μ x = Nat.find (_ : ∃ i, x ∈ MeasureTheory.spanningSets μ i)

theorem MeasureTheory.measurable_spanningSetsIndex {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] : Measurable (MeasureTheory.spanningSetsIndex μ)

theorem MeasureTheory.preimage_spanningSetsIndex_singleton {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] (n : ℕ) : MeasureTheory.spanningSetsIndex μ ⁻¹' {n} = disjointed (MeasureTheory.spanningSets μ) n

theorem MeasureTheory.spanningSetsIndex_eq_iff {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] {x : α} {n : ℕ} : MeasureTheory.spanningSetsIndex μ x = n ↔ x ∈ disjointed (MeasureTheory.spanningSets μ) n

theorem MeasureTheory.mem_disjointed_spanningSetsIndex {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] (x : α) : x ∈ disjointed (MeasureTheory.spanningSets μ) (MeasureTheory.spanningSetsIndex μ x)

theorem MeasureTheory.mem_spanningSetsIndex {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] (x : α) : x ∈ MeasureTheory.spanningSets μ (MeasureTheory.spanningSetsIndex μ x)

theorem MeasureTheory.mem_spanningSets_of_index_le {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] (x : α) {n : ℕ} (hn : MeasureTheory.spanningSetsIndex μ x ≤ n) : x ∈ MeasureTheory.spanningSets μ n

theorem MeasureTheory.eventually_mem_spanningSets {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] (x : α) : ∀ᶠ (n : ℕ) in Filter.atTop, x ∈ MeasureTheory.spanningSets μ n

theorem MeasureTheory.Measure.iSup_restrict_spanningSets {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.SigmaFinite μ] (hs : MeasurableSet s) : ⨆ (i : ℕ), ↑↑(MeasureTheory.Measure.restrict μ (MeasureTheory.spanningSets μ i)) s = ↑↑μ s

theorem MeasureTheory.Measure.exists_subset_measure_lt_top {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.SigmaFinite μ] {r : ENNReal} (hs : MeasurableSet s) (h's : r < ↑↑μ s) : ∃ t, MeasurableSet t ∧ t ⊆ s ∧ r < ↑↑μ t ∧ ↑↑μ t < ⊤

In a σ-finite space, any measurable set of measure > r contains a measurable subset of finite measure > r.

theorem MeasureTheory.Measure.forall_measure_inter_spanningSets_eq_zero {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] (s : Set α) : (∀ (n : ℕ), ↑↑μ (s ∩ MeasureTheory.spanningSets μ n) = 0) ↔ ↑↑μ s = 0

A set in a σ-finite space has zero measure if and only if its intersection with all members of the countable family of finite measure spanning sets has zero measure.

theorem MeasureTheory.Measure.exists_measure_inter_spanningSets_pos {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] (s : Set α) : (∃ n, 0 < ↑↑μ (s ∩ MeasureTheory.spanningSets μ n)) ↔ 0 < ↑↑μ s

A set in a σ-finite space has positive measure if and only if its intersection with some member of the countable family of finite measure spanning sets has positive measure.

theorem MeasureTheory.Measure.finite_const_le_meas_of_disjoint_iUnion₀ {α : Type u_1} {ι : Type u_8} [MeasurableSpace α] (μ : MeasureTheory.Measure α) {ε : ENNReal} (ε_pos : 0 < ε) {As : ι → Set α} (As_mble : ∀ (i : ι), MeasureTheory.NullMeasurableSet (As i)) (As_disj : Pairwise (MeasureTheory.AEDisjoint μ on As)) (Union_As_finite : ↑↑μ (⋃ (i : ι), As i) ≠ ⊤) : Set.Finite {i | ε ≤ ↑↑μ (As i)}

If the union of a.e.-disjoint null-measurable sets has finite measure, then there are only finitely many members of the union whose measure exceeds any given positive number.

theorem MeasureTheory.Measure.finite_const_le_meas_of_disjoint_iUnion {α : Type u_1} {ι : Type u_8} [MeasurableSpace α] (μ : MeasureTheory.Measure α) {ε : ENNReal} (ε_pos : 0 < ε) {As : ι → Set α} (As_mble : ∀ (i : ι), MeasurableSet (As i)) (As_disj : Pairwise (Disjoint on As)) (Union_As_finite : ↑↑μ (⋃ (i : ι), As i) ≠ ⊤) : Set.Finite {i | ε ≤ ↑↑μ (As i)}

If the union of disjoint measurable sets has finite measure, then there are only finitely many members of the union whose measure exceeds any given positive number.

theorem Set.Infinite.meas_eq_top {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasurableSingletonClass α] {s : Set α} (hs : Set.Infinite s) (h' : ∃ ε, ε ≠ 0 ∧ ∀ (x : α), x ∈ s → ε ≤ ↑↑μ {x}) : ↑↑μ s = ⊤

If all elements of an infinite set have measure uniformly separated from zero, then the set has infinite measure.

theorem MeasureTheory.Measure.countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top₀ {α : Type u_1} {ι : Type u_8} [MeasurableSpace α] (μ : MeasureTheory.Measure α) {As : ι → Set α} (As_mble : ∀ (i : ι), MeasureTheory.NullMeasurableSet (As i)) (As_disj : Pairwise (MeasureTheory.AEDisjoint μ on As)) (Union_As_finite : ↑↑μ (⋃ (i : ι), As i) ≠ ⊤) : Set.Countable {i | 0 < ↑↑μ (As i)}

If the union of a.e.-disjoint null-measurable sets has finite measure, then there are only countably many members of the union whose measure is positive.

theorem MeasureTheory.Measure.countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top {α : Type u_1} {ι : Type u_8} [MeasurableSpace α] (μ : MeasureTheory.Measure α) {As : ι → Set α} (As_mble : ∀ (i : ι), MeasurableSet (As i)) (As_disj : Pairwise (Disjoint on As)) (Union_As_finite : ↑↑μ (⋃ (i : ι), As i) ≠ ⊤) : Set.Countable {i | 0 < ↑↑μ (As i)}

If the union of disjoint measurable sets has finite measure, then there are only countably many members of the union whose measure is positive.

theorem MeasureTheory.Measure.countable_meas_pos_of_disjoint_iUnion₀ {α : Type u_1} {ι : Type u_8} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] {As : ι → Set α} (As_mble : ∀ (i : ι), MeasureTheory.NullMeasurableSet (As i)) (As_disj : Pairwise (MeasureTheory.AEDisjoint μ on As)) : Set.Countable {i | 0 < ↑↑μ (As i)}

In a σ-finite space, among disjoint null-measurable sets, only countably many can have positive measure.

theorem MeasureTheory.Measure.countable_meas_pos_of_disjoint_iUnion {α : Type u_1} {ι : Type u_8} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] {As : ι → Set α} (As_mble : ∀ (i : ι), MeasurableSet (As i)) (As_disj : Pairwise (Disjoint on As)) : Set.Countable {i | 0 < ↑↑μ (As i)}

In a σ-finite space, among disjoint measurable sets, only countably many can have positive measure.

theorem MeasureTheory.Measure.countable_meas_level_set_pos₀ {α : Type u_8} {β : Type u_9} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] [MeasurableSpace β] [MeasurableSingletonClass β] {g : α → β} (g_mble : MeasureTheory.NullMeasurable g) : Set.Countable {t | 0 < ↑↑μ {a | g a = t}}

theorem MeasureTheory.Measure.countable_meas_level_set_pos {α : Type u_8} {β : Type u_9} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] [MeasurableSpace β] [MeasurableSingletonClass β] {g : α → β} (g_mble : Measurable g) : Set.Countable {t | 0 < ↑↑μ {a | g a = t}}

theorem MeasureTheory.Measure.measure_toMeasurable_inter_of_cover {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) {t : Set α} {v : ℕ → Set α} (hv : t ⊆ ⋃ (n : ℕ), v n) (h'v : ∀ (n : ℕ), ↑↑μ (t ∩ v n) ≠ ⊤) : ↑↑μ (MeasureTheory.toMeasurable μ t ∩ s) = ↑↑μ (t ∩ s)

If a set t is covered by a countable family of finite measure sets, then its measurable superset toMeasurable μ t (which has the same measure as t) satisfies, for any measurable set s, the equality μ (toMeasurable μ t ∩ s) = μ (t ∩ s).

theorem MeasureTheory.Measure.restrict_toMeasurable_of_cover {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {v : ℕ → Set α} (hv : s ⊆ ⋃ (n : ℕ), v n) (h'v : ∀ (n : ℕ), ↑↑μ (s ∩ v n) ≠ ⊤) : MeasureTheory.Measure.restrict μ (MeasureTheory.toMeasurable μ s) = MeasureTheory.Measure.restrict μ s

theorem MeasureTheory.Measure.measure_toMeasurable_inter_of_sigmaFinite {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] {s : Set α} (hs : MeasurableSet s) (t : Set α) : ↑↑μ (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) = μ (t ∩ s). This only holds when μ is σ-finite. For a version without this assumption (but requiring that t has finite measure), see measure_toMeasurable_inter.

@[simp]

theorem MeasureTheory.Measure.restrict_toMeasurable_of_sigmaFinite {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] (s : Set α) : MeasureTheory.Measure.restrict μ (MeasureTheory.toMeasurable μ s) = MeasureTheory.Measure.restrict μ s

def MeasureTheory.Measure.FiniteSpanningSetsIn.mono' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {C : Set (Set α)} {D : Set (Set α)} (h : MeasureTheory.Measure.FiniteSpanningSetsIn μ C) (hC : C ∩ {s | ↑↑μ s < ⊤} ⊆ D) : MeasureTheory.Measure.FiniteSpanningSetsIn μ D

If μ has finite spanning sets in C and C ∩ {s | μ s < ∞} ⊆ D then μ has finite spanning sets in D.

Equations

• One or more equations did not get rendered due to their size.

def MeasureTheory.Measure.FiniteSpanningSetsIn.mono {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {C : Set (Set α)} {D : Set (Set α)} (h : MeasureTheory.Measure.FiniteSpanningSetsIn μ C) (hC : C ⊆ D) : MeasureTheory.Measure.FiniteSpanningSetsIn μ D

If μ has finite spanning sets in C and C ⊆ D then μ has finite spanning sets in D.

Equations

• MeasureTheory.Measure.FiniteSpanningSetsIn.mono h hC = MeasureTheory.Measure.FiniteSpanningSetsIn.mono' h (_ : ∀ (_s : Set α), _s ∈ C ∩ {s | ↑↑μ s < ⊤} → _s ∈ D)

theorem MeasureTheory.Measure.FiniteSpanningSetsIn.sigmaFinite {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {C : Set (Set α)} (h : MeasureTheory.Measure.FiniteSpanningSetsIn μ C) : MeasureTheory.SigmaFinite μ

If μ has finite spanning sets in the collection of measurable sets C, then μ is σ-finite.

theorem MeasureTheory.Measure.FiniteSpanningSetsIn.ext {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {C : Set (Set α)} (hA : m0 = MeasurableSpace.generateFrom C) (hC : IsPiSystem C) (h : MeasureTheory.Measure.FiniteSpanningSetsIn μ C) (h_eq : ∀ (s : Set α), s ∈ C → ↑↑μ s = ↑↑ν s) : μ = ν

An extensionality for measures. It is ext_of_generateFrom_of_iUnion formulated in terms of FiniteSpanningSetsIn.

theorem MeasureTheory.Measure.FiniteSpanningSetsIn.isCountablySpanning {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {C : Set (Set α)} (h : MeasureTheory.Measure.FiniteSpanningSetsIn μ C) : IsCountablySpanning C

theorem MeasureTheory.Measure.sigmaFinite_of_countable {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {S : Set (Set α)} (hc : Set.Countable S) (hμ : ∀ (s : Set α), s ∈ S → ↑↑μ s < ⊤) (hU : ⋃₀ S = Set.univ) : MeasureTheory.SigmaFinite μ

def MeasureTheory.Measure.FiniteSpanningSetsIn.ofLE {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} (h : ν ≤ μ) {C : Set (Set α)} (S : MeasureTheory.Measure.FiniteSpanningSetsIn μ C) : MeasureTheory.Measure.FiniteSpanningSetsIn ν C

Given measures μ, ν where ν ≤ μ, FiniteSpanningSetsIn.ofLe provides the induced FiniteSpanningSet with respect to ν from a FiniteSpanningSet with respect to μ.

Equations

• One or more equations did not get rendered due to their size.

theorem MeasureTheory.Measure.sigmaFinite_of_le {α : Type u_1} {m0 : MeasurableSpace α} {ν : MeasureTheory.Measure α} (μ : MeasureTheory.Measure α) [hs : MeasureTheory.SigmaFinite μ] (h : ν ≤ μ) : MeasureTheory.SigmaFinite ν

instance MeasureTheory.IsFiniteMeasure.toSigmaFinite {α : Type u_1} {_m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] : MeasureTheory.SigmaFinite μ

Every finite measure is σ-finite.

Equations

• @MeasureTheory.IsFiniteMeasure.toSigmaFinite = @MeasureTheory.IsFiniteMeasure.toSigmaFinite.proof_1

theorem MeasureTheory.sigmaFinite_bot_iff {α : Type u_1} (μ : MeasureTheory.Measure α) : MeasureTheory.SigmaFinite μ ↔ MeasureTheory.IsFiniteMeasure μ

instance MeasureTheory.Restrict.sigmaFinite {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] (s : Set α) : MeasureTheory.SigmaFinite (MeasureTheory.Measure.restrict μ s)

Equations

• @MeasureTheory.Restrict.sigmaFinite = @MeasureTheory.Restrict.sigmaFinite.proof_1

instance MeasureTheory.sum.sigmaFinite {α : Type u_1} {m0 : MeasurableSpace α} {ι : Type u_8} [Finite ι] (μ : ι → MeasureTheory.Measure α) [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] : MeasureTheory.SigmaFinite (MeasureTheory.Measure.sum μ)

Equations

• @MeasureTheory.sum.sigmaFinite = @MeasureTheory.sum.sigmaFinite.proof_1

instance MeasureTheory.Add.sigmaFinite {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] : MeasureTheory.SigmaFinite (μ + ν)

Equations

• @MeasureTheory.Add.sigmaFinite = @MeasureTheory.Add.sigmaFinite.proof_1

instance MeasureTheory.SMul.sigmaFinite {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] (c : NNReal) : MeasureTheory.SigmaFinite (c • μ)

Equations

• @MeasureTheory.SMul.sigmaFinite = @MeasureTheory.SMul.sigmaFinite.proof_1

theorem MeasureTheory.SigmaFinite.of_map {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] (μ : MeasureTheory.Measure α) {f : α → β} (hf : AEMeasurable f) (h : MeasureTheory.SigmaFinite (MeasureTheory.Measure.map f μ)) : MeasureTheory.SigmaFinite μ

theorem MeasurableEquiv.sigmaFinite_map {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} (f : α ≃ᵐ β) (h : MeasureTheory.SigmaFinite μ) : MeasureTheory.SigmaFinite (MeasureTheory.Measure.map (↑f) μ)

theorem MeasureTheory.ae_of_forall_measure_lt_top_ae_restrict' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] (P : α → Prop) (h : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ↑↑ν s < ⊤ → ∀ᵐ (x : α) ∂MeasureTheory.Measure.restrict μ s, P x) : ∀ᵐ (x : α) ∂μ, P x

Similar to ae_of_forall_measure_lt_top_ae_restrict, but where you additionally get the hypothesis that another σ-finite measure has finite values on s.

theorem MeasureTheory.ae_of_forall_measure_lt_top_ae_restrict {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] (P : α → Prop) (h : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∀ᵐ (x : α) ∂MeasureTheory.Measure.restrict μ s, P x) : ∀ᵐ (x : α) ∂μ, P x

To prove something for almost all x w.r.t. a σ-finite measure, it is sufficient to show that this holds almost everywhere in sets where the measure has finite value.

class MeasureTheory.IsLocallyFiniteMeasure {α : Type u_1} {m0 : MeasurableSpace α} [TopologicalSpace α] (μ : MeasureTheory.Measure α) : Prop

• finiteAtNhds : ∀ (x : α), MeasureTheory.Measure.FiniteAtFilter μ (nhds x)

A measure is called locally finite if it is finite in some neighborhood of each point.

instance MeasureTheory.IsFiniteMeasure.toIsLocallyFiniteMeasure {α : Type u_1} {m0 : MeasurableSpace α} [TopologicalSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] : MeasureTheory.IsLocallyFiniteMeasure μ

Equations

• @MeasureTheory.IsFiniteMeasure.toIsLocallyFiniteMeasure = @MeasureTheory.IsFiniteMeasure.toIsLocallyFiniteMeasure.proof_1

theorem MeasureTheory.Measure.finiteAt_nhds {α : Type u_1} {m0 : MeasurableSpace α} [TopologicalSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] (x : α) : MeasureTheory.Measure.FiniteAtFilter μ (nhds x)

theorem MeasureTheory.Measure.smul_finite {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] {c : ENNReal} (hc : c ≠ ⊤) : MeasureTheory.IsFiniteMeasure (c • μ)

theorem MeasureTheory.Measure.exists_isOpen_measure_lt_top {α : Type u_1} {m0 : MeasurableSpace α} [TopologicalSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] (x : α) : ∃ s, x ∈ s ∧ IsOpen s ∧ ↑↑μ s < ⊤

instance MeasureTheory.isLocallyFiniteMeasureSMulNNReal {α : Type u_1} {m0 : MeasurableSpace α} [TopologicalSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] (c : NNReal) : MeasureTheory.IsLocallyFiniteMeasure (c • μ)

Equations

• @MeasureTheory.isLocallyFiniteMeasureSMulNNReal = @MeasureTheory.isLocallyFiniteMeasureSMulNNReal.proof_1

theorem MeasureTheory.Measure.isTopologicalBasis_isOpen_lt_top {α : Type u_1} {m0 : MeasurableSpace α} [TopologicalSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] : TopologicalSpace.IsTopologicalBasis {s | IsOpen s ∧ ↑↑μ s < ⊤}

class MeasureTheory.IsFiniteMeasureOnCompacts {α : Type u_1} {m0 : MeasurableSpace α} [TopologicalSpace α] (μ : MeasureTheory.Measure α) : Prop

• lt_top_of_isCompact : ∀ ⦃K : Set α⦄, IsCompact K → ↑↑μ K < ⊤

A measure μ is finite on compacts if any compact set K satisfies μ K < ∞.

theorem IsCompact.measure_lt_top {α : Type u_1} {m0 : MeasurableSpace α} [TopologicalSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasureOnCompacts μ] ⦃K : Set α⦄ (hK : IsCompact K) : ↑↑μ K < ⊤

A compact subset has finite measure for a measure which is finite on compacts.

theorem Bornology.IsBounded.measure_lt_top {α : Type u_1} {m0 : MeasurableSpace α} [PseudoMetricSpace α] [ProperSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasureOnCompacts μ] ⦃s : Set α⦄ (hs : Bornology.IsBounded s) : ↑↑μ s < ⊤

A bounded subset has finite measure for a measure which is finite on compact sets, in a proper space.

theorem MeasureTheory.measure_closedBall_lt_top {α : Type u_1} {m0 : MeasurableSpace α} [PseudoMetricSpace α] [ProperSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasureOnCompacts μ] {x : α} {r : ℝ} : ↑↑μ (Metric.closedBall x r) < ⊤

theorem MeasureTheory.measure_ball_lt_top {α : Type u_1} {m0 : MeasurableSpace α} [PseudoMetricSpace α] [ProperSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasureOnCompacts μ] {x : α} {r : ℝ} : ↑↑μ (Metric.ball x r) < ⊤

theorem MeasureTheory.IsFiniteMeasureOnCompacts.smul {α : Type u_1} {m0 : MeasurableSpace α} [TopologicalSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasureOnCompacts μ] {c : ENNReal} (hc : c ≠ ⊤) : MeasureTheory.IsFiniteMeasureOnCompacts (c • μ)

theorem MeasureTheory.CompactSpace.isFiniteMeasure {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace α] [CompactSpace α] [MeasureTheory.IsFiniteMeasureOnCompacts μ] : MeasureTheory.IsFiniteMeasure μ

Note this cannot be an instance because it would form a typeclass loop with isFiniteMeasureOnCompacts_of_isLocallyFiniteMeasure.

instance MeasureTheory.sigmaFinite_of_locallyFinite {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace α] [TopologicalSpace.SecondCountableTopology α] [MeasureTheory.IsLocallyFiniteMeasure μ] : MeasureTheory.SigmaFinite μ

Equations

• @MeasureTheory.sigmaFinite_of_locallyFinite = @MeasureTheory.sigmaFinite_of_locallyFinite.proof_1

theorem MeasureTheory.isLocallyFiniteMeasure_of_isFiniteMeasureOnCompacts {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace α] [WeaklyLocallyCompactSpace α] [MeasureTheory.IsFiniteMeasureOnCompacts μ] : MeasureTheory.IsLocallyFiniteMeasure μ

A measure which is finite on compact sets in a locally compact space is locally finite. Not registered as an instance to avoid a loop with the other direction.

theorem MeasureTheory.exists_pos_measure_of_cover {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable ι] {U : ι → Set α} (hU : ⋃ (i : ι), U i = Set.univ) (hμ : μ ≠ 0) : ∃ i, 0 < ↑↑μ (U i)

theorem MeasureTheory.exists_pos_preimage_ball {α : Type u_1} {δ : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [PseudoMetricSpace δ] (f : α → δ) (x : δ) (hμ : μ ≠ 0) : ∃ n, 0 < ↑↑μ (f ⁻¹' Metric.ball x ↑n)

theorem MeasureTheory.exists_pos_ball {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [PseudoMetricSpace α] (x : α) (hμ : μ ≠ 0) : ∃ n, 0 < ↑↑μ (Metric.ball x ↑n)

theorem MeasureTheory.null_of_locally_null {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace α] [TopologicalSpace.SecondCountableTopology α] (s : Set α) (hs : ∀ (x : α), x ∈ s → ∃ u, u ∈ nhdsWithin x s ∧ ↑↑μ u = 0) : ↑↑μ s = 0

If a set has zero measure in a neighborhood of each of its points, then it has zero measure in a second-countable space.

theorem MeasureTheory.exists_mem_forall_mem_nhdsWithin_pos_measure {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace α] [TopologicalSpace.SecondCountableTopology α] {s : Set α} (hs : ↑↑μ s ≠ 0) : ∃ x, x ∈ s ∧ ∀ (t : Set α), t ∈ nhdsWithin x s → 0 < ↑↑μ t

theorem MeasureTheory.exists_ne_forall_mem_nhds_pos_measure_preimage {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_8} [TopologicalSpace β] [T1Space β] [TopologicalSpace.SecondCountableTopology β] [Nonempty β] {f : α → β} (h : ∀ (b : β), ∃ᵐ (x : α) ∂μ, f x ≠ b) : ∃ a b, a ≠ b ∧ (∀ (s : Set β), s ∈ nhds a → 0 < ↑↑μ (f ⁻¹' s)) ∧ ∀ (t : Set β), t ∈ nhds b → 0 < ↑↑μ (f ⁻¹' t)

theorem MeasureTheory.ext_on_measurableSpace_of_generate_finite {α : Type u_8} (m₀ : MeasurableSpace α) {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] (C : Set (Set α)) (hμν : ∀ (s : Set α), s ∈ C → ↑↑μ s = ↑↑ν s) {m : MeasurableSpace α} (h : m ≤ m₀) (hA : m = MeasurableSpace.generateFrom C) (hC : IsPiSystem C) (h_univ : ↑↑μ Set.univ = ↑↑ν Set.univ) {s : Set α} (hs : MeasurableSet s) : ↑↑μ s = ↑↑ν s

If two finite measures give the same mass to the whole space and coincide on a π-system made of measurable sets, then they coincide on all sets in the σ-algebra generated by the π-system.

theorem MeasureTheory.ext_of_generate_finite {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} (C : Set (Set α)) (hA : m0 = MeasurableSpace.generateFrom C) (hC : IsPiSystem C) [MeasureTheory.IsFiniteMeasure μ] (hμν : ∀ (s : Set α), s ∈ C → ↑↑μ s = ↑↑ν s) (h_univ : ↑↑μ Set.univ = ↑↑ν Set.univ) : μ = ν

Two finite measures are equal if they are equal on the π-system generating the σ-algebra (and univ).

def MeasureTheory.Measure.FiniteSpanningSetsIn.disjointed {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (S : MeasureTheory.Measure.FiniteSpanningSetsIn μ {s | MeasurableSet s}) : MeasureTheory.Measure.FiniteSpanningSetsIn μ {s | MeasurableSet s}

Given S : μ.FiniteSpanningSetsIn {s | MeasurableSet s}, FiniteSpanningSetsIn.disjointed provides a FiniteSpanningSetsIn {s | MeasurableSet s} such that its underlying sets are pairwise disjoint.

Equations

• One or more equations did not get rendered due to their size.

theorem MeasureTheory.Measure.FiniteSpanningSetsIn.disjointed_set_eq {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (S : MeasureTheory.Measure.FiniteSpanningSetsIn μ {s | MeasurableSet s}) : (MeasureTheory.Measure.FiniteSpanningSetsIn.disjointed S).set = disjointed S.set

theorem MeasureTheory.Measure.exists_eq_disjoint_finiteSpanningSetsIn {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] : ∃ S T, S.set = T.set ∧ Pairwise (Disjoint on S.set)

theorem MeasureTheory.Measure.FiniteAtFilter.filter_mono {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : Filter α} {g : Filter α} (h : f ≤ g) : MeasureTheory.Measure.FiniteAtFilter μ g → MeasureTheory.Measure.FiniteAtFilter μ f

theorem MeasureTheory.Measure.FiniteAtFilter.inf_of_left {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : Filter α} {g : Filter α} (h : MeasureTheory.Measure.FiniteAtFilter μ f) : MeasureTheory.Measure.FiniteAtFilter μ (f ⊓ g)

theorem MeasureTheory.Measure.FiniteAtFilter.inf_of_right {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : Filter α} {g : Filter α} (h : MeasureTheory.Measure.FiniteAtFilter μ g) : MeasureTheory.Measure.FiniteAtFilter μ (f ⊓ g)

@[simp]

theorem MeasureTheory.Measure.FiniteAtFilter.inf_ae_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : Filter α} : MeasureTheory.Measure.FiniteAtFilter μ (f ⊓ MeasureTheory.Measure.ae μ) ↔ MeasureTheory.Measure.FiniteAtFilter μ f

theorem MeasureTheory.Measure.FiniteAtFilter.of_inf_ae {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : Filter α} : MeasureTheory.Measure.FiniteAtFilter μ (f ⊓ MeasureTheory.Measure.ae μ) → MeasureTheory.Measure.FiniteAtFilter μ f

Alias of the forward direction of MeasureTheory.Measure.FiniteAtFilter.inf_ae_iff.

theorem MeasureTheory.Measure.FiniteAtFilter.filter_mono_ae {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : Filter α} {g : Filter α} (h : f ⊓ MeasureTheory.Measure.ae μ ≤ g) (hg : MeasureTheory.Measure.FiniteAtFilter μ g) : MeasureTheory.Measure.FiniteAtFilter μ f

theorem MeasureTheory.Measure.FiniteAtFilter.measure_mono {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : Filter α} (h : μ ≤ ν) : MeasureTheory.Measure.FiniteAtFilter ν f → MeasureTheory.Measure.FiniteAtFilter μ f

theorem MeasureTheory.Measure.FiniteAtFilter.mono {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : Filter α} {g : Filter α} (hf : f ≤ g) (hμ : μ ≤ ν) : MeasureTheory.Measure.FiniteAtFilter ν g → MeasureTheory.Measure.FiniteAtFilter μ f

theorem MeasureTheory.Measure.FiniteAtFilter.eventually {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : Filter α} (h : MeasureTheory.Measure.FiniteAtFilter μ f) : ∀ᶠ (s : Set α) in Filter.smallSets f, ↑↑μ s < ⊤

theorem MeasureTheory.Measure.FiniteAtFilter.filterSup {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : Filter α} {g : Filter α} : MeasureTheory.Measure.FiniteAtFilter μ f → MeasureTheory.Measure.FiniteAtFilter μ g → MeasureTheory.Measure.FiniteAtFilter μ (f ⊔ g)

theorem MeasureTheory.Measure.finiteAt_nhdsWithin {α : Type u_1} [TopologicalSpace α] {_m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] (x : α) (s : Set α) : MeasureTheory.Measure.FiniteAtFilter μ (nhdsWithin x s)

@[simp]

theorem MeasureTheory.Measure.finiteAt_principal {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} : MeasureTheory.Measure.FiniteAtFilter μ (Filter.principal s) ↔ ↑↑μ s < ⊤

theorem MeasureTheory.Measure.isLocallyFiniteMeasure_of_le {α : Type u_1} [TopologicalSpace α] {_m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [H : MeasureTheory.IsLocallyFiniteMeasure μ] (h : ν ≤ μ) : MeasureTheory.IsLocallyFiniteMeasure ν

theorem MeasurableEmbedding.map_apply {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {m1 : MeasurableSpace β} {f : α → β} (hf : MeasurableEmbedding f) (μ : MeasureTheory.Measure α) (s : Set β) : ↑↑(MeasureTheory.Measure.map f μ) s = ↑↑μ (f ⁻¹' s)

theorem MeasurableEmbedding.map_comap {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {m1 : MeasurableSpace β} {f : α → β} (hf : MeasurableEmbedding f) (μ : MeasureTheory.Measure β) : MeasureTheory.Measure.map f (MeasureTheory.Measure.comap f μ) = MeasureTheory.Measure.restrict μ (Set.range f)

theorem MeasurableEmbedding.comap_apply {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {m1 : MeasurableSpace β} {f : α → β} (hf : MeasurableEmbedding f) (μ : MeasureTheory.Measure β) (s : Set α) : ↑↑(MeasureTheory.Measure.comap f μ) s = ↑↑μ (f '' s)

theorem MeasurableEmbedding.ae_map_iff {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {m1 : MeasurableSpace β} {f : α → β} (hf : MeasurableEmbedding f) {p : β → Prop} {μ : MeasureTheory.Measure α} : (∀ᵐ (x : β) ∂MeasureTheory.Measure.map f μ, p x) ↔ ∀ᵐ (x : α) ∂μ, p (f x)

theorem MeasurableEmbedding.restrict_map {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {m1 : MeasurableSpace β} {f : α → β} (hf : MeasurableEmbedding f) (μ : MeasureTheory.Measure α) (s : Set β) : MeasureTheory.Measure.restrict (MeasureTheory.Measure.map f μ) s = MeasureTheory.Measure.map f (MeasureTheory.Measure.restrict μ (f ⁻¹' s))

theorem MeasurableEmbedding.comap_preimage {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {m1 : MeasurableSpace β} {f : α → β} (hf : MeasurableEmbedding f) (μ : MeasureTheory.Measure β) {s : Set β} (hs : MeasurableSet s) : ↑↑(MeasureTheory.Measure.comap f μ) (f ⁻¹' s) = ↑↑μ (s ∩ Set.range f)

theorem comap_subtype_coe_apply {α : Type u_1} {_m0 : MeasurableSpace α} {s : Set α} (hs : MeasurableSet s) (μ : MeasureTheory.Measure α) (t : Set ↑s) : ↑↑(MeasureTheory.Measure.comap Subtype.val μ) t = ↑↑μ (Subtype.val '' t)

theorem map_comap_subtype_coe {α : Type u_1} {m0 : MeasurableSpace α} {s : Set α} (hs : MeasurableSet s) (μ : MeasureTheory.Measure α) : MeasureTheory.Measure.map Subtype.val (MeasureTheory.Measure.comap Subtype.val μ) = MeasureTheory.Measure.restrict μ s

theorem ae_restrict_iff_subtype {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) {p : α → Prop} : (∀ᵐ (x : α) ∂MeasureTheory.Measure.restrict μ s, p x) ↔ ∀ᵐ (x : ↑s) ∂MeasureTheory.Measure.comap Subtype.val μ, p ↑x

Volume on s : Set α

instance SetCoe.measureSpace {α : Type u_1} [MeasureTheory.MeasureSpace α] (s : Set α) : MeasureTheory.MeasureSpace ↑s

Equations

• SetCoe.measureSpace s = MeasureTheory.MeasureSpace.mk (MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume)

theorem volume_set_coe_def {α : Type u_1} [MeasureTheory.MeasureSpace α] (s : Set α) : MeasureTheory.volume = MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume

theorem MeasurableSet.map_coe_volume {α : Type u_1} [MeasureTheory.MeasureSpace α] {s : Set α} (hs : MeasurableSet s) : MeasureTheory.Measure.map Subtype.val MeasureTheory.volume = MeasureTheory.Measure.restrict MeasureTheory.volume s

theorem volume_image_subtype_coe {α : Type u_1} [MeasureTheory.MeasureSpace α] {s : Set α} (hs : MeasurableSet s) (t : Set ↑s) : ↑↑MeasureTheory.volume (Subtype.val '' t) = ↑↑MeasureTheory.volume t

@[simp]

theorem volume_preimage_coe {α : Type u_1} [MeasureTheory.MeasureSpace α] {s : Set α} {t : Set α} (hs : MeasureTheory.NullMeasurableSet s) (ht : MeasurableSet t) : ↑↑MeasureTheory.volume (Subtype.val ⁻¹' t) = ↑↑MeasureTheory.volume (t ∩ s)

Interactions of measurable equivalences and measures

theorem MeasurableEquiv.map_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [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).

@[simp]

theorem MeasurableEquiv.map_symm_map {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} (e : α ≃ᵐ β) : MeasureTheory.Measure.map (↑(MeasurableEquiv.symm e)) (MeasureTheory.Measure.map (↑e) μ) = μ

@[simp]

theorem MeasurableEquiv.map_map_symm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {ν : MeasureTheory.Measure β} (e : α ≃ᵐ β) : MeasureTheory.Measure.map (↑e) (MeasureTheory.Measure.map (↑(MeasurableEquiv.symm e)) ν) = ν

theorem MeasurableEquiv.map_measurableEquiv_injective {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) : Function.Injective (MeasureTheory.Measure.map ↑e)

theorem MeasurableEquiv.map_apply_eq_iff_map_symm_apply_eq {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} (e : α ≃ᵐ β) : MeasureTheory.Measure.map (↑e) μ = ν ↔ MeasureTheory.Measure.map (↑(MeasurableEquiv.symm e)) ν = μ

theorem MeasurableEquiv.restrict_map {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} (e : α ≃ᵐ β) (s : Set β) : MeasureTheory.Measure.restrict (MeasureTheory.Measure.map (↑e) μ) s = MeasureTheory.Measure.map (↑e) (MeasureTheory.Measure.restrict μ (↑e ⁻¹' s))

theorem MeasurableEquiv.map_ae {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (f : α ≃ᵐ β) (μ : MeasureTheory.Measure α) : Filter.map (↑f) (MeasureTheory.Measure.ae μ) = MeasureTheory.Measure.ae (MeasureTheory.Measure.map (↑f) μ)

theorem MeasurableEquiv.quasiMeasurePreserving_symm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (μ : MeasureTheory.Measure α) (e : α ≃ᵐ β) : MeasureTheory.Measure.QuasiMeasurePreserving ↑(MeasurableEquiv.symm e)

theorem MeasureTheory.OuterMeasure.toMeasure_zero {α : Type u_1} [MeasurableSpace α] : MeasureTheory.OuterMeasure.toMeasure 0 (_ : inst✝ ≤ MeasureTheory.OuterMeasure.caratheodory 0) = 0

theorem IsCompact.exists_open_superset_measure_lt_top' {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (h : IsCompact s) (hμ : ∀ (x : α), x ∈ s → MeasureTheory.Measure.FiniteAtFilter μ (nhds x)) : ∃ U x, IsOpen U ∧ ↑↑μ U < ⊤

If s is a compact set and μ is finite at 𝓝 x for every x ∈ s, then s admits an open superset of finite measure.

theorem IsCompact.exists_open_superset_measure_lt_top {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] {s : Set α} (h : IsCompact s) (μ : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] : ∃ U x, IsOpen U ∧ ↑↑μ U < ⊤

If s is a compact set and μ is a locally finite measure, then s admits an open superset of finite measure.

theorem IsCompact.measure_lt_top_of_nhdsWithin {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (h : IsCompact s) (hμ : ∀ (x : α), x ∈ s → MeasureTheory.Measure.FiniteAtFilter μ (nhdsWithin x s)) : ↑↑μ s < ⊤

theorem IsCompact.measure_zero_of_nhdsWithin {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (hs : IsCompact s) : (∀ (a : α), a ∈ s → ∃ t, t ∈ nhdsWithin a s ∧ ↑↑μ t = 0) → ↑↑μ s = 0

instance isFiniteMeasureOnCompacts_of_isLocallyFiniteMeasure {α : Type u_1} [TopologicalSpace α] : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.IsLocallyFiniteMeasure μ], MeasureTheory.IsFiniteMeasureOnCompacts μ

Equations

• @isFiniteMeasureOnCompacts_of_isLocallyFiniteMeasure = @isFiniteMeasureOnCompacts_of_isLocallyFiniteMeasure.proof_1

theorem isFiniteMeasure_iff_isFiniteMeasureOnCompacts_of_compactSpace {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [CompactSpace α] : MeasureTheory.IsFiniteMeasure μ ↔ MeasureTheory.IsFiniteMeasureOnCompacts μ

def MeasureTheory.Measure.finiteSpanningSetsInCompact {α : Type u_1} [TopologicalSpace α] [SigmaCompactSpace α] : {x : MeasurableSpace α} → (μ : MeasureTheory.Measure α) → [inst : MeasureTheory.IsLocallyFiniteMeasure μ] → MeasureTheory.Measure.FiniteSpanningSetsIn μ {K | IsCompact K}

Compact covering of a σ-compact topological space as MeasureTheory.Measure.FiniteSpanningSetsIn.

Equations

• One or more equations did not get rendered due to their size.

def MeasureTheory.Measure.finiteSpanningSetsInOpen {α : Type u_1} [TopologicalSpace α] [SigmaCompactSpace α] : {x : MeasurableSpace α} → (μ : MeasureTheory.Measure α) → [inst : MeasureTheory.IsLocallyFiniteMeasure μ] → MeasureTheory.Measure.FiniteSpanningSetsIn μ {K | IsOpen K}

A locally finite measure on a σ-compact topological space admits a finite spanning sequence of open sets.

Equations

• One or more equations did not get rendered due to their size.

@[irreducible]

def MeasureTheory.Measure.finiteSpanningSetsInOpen' {α : Type u_8} [TopologicalSpace α] [TopologicalSpace.SecondCountableTopology α] {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] : MeasureTheory.Measure.FiniteSpanningSetsIn μ {K | IsOpen K}

A locally finite measure on a second countable topological space admits a finite spanning sequence of open sets.

Equations

• @MeasureTheory.Measure.finiteSpanningSetsInOpen' = wrapped✝.1

theorem MeasureTheory.Measure.finiteSpanningSetsInOpen'_def {α : Type u_8} [TopologicalSpace α] [TopologicalSpace.SecondCountableTopology α] {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] : MeasureTheory.Measure.finiteSpanningSetsInOpen' μ = Nonempty.some (_ : Nonempty (MeasureTheory.Measure.FiniteSpanningSetsIn μ {K | IsOpen K}))

theorem measure_Icc_lt_top {α : Type u_1} [Preorder α] [TopologicalSpace α] [CompactIccSpace α] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure μ] {a : α} {b : α} : ↑↑μ (Set.Icc a b) < ⊤

theorem measure_Ico_lt_top {α : Type u_1} [Preorder α] [TopologicalSpace α] [CompactIccSpace α] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure μ] {a : α} {b : α} : ↑↑μ (Set.Ico a b) < ⊤

theorem measure_Ioc_lt_top {α : Type u_1} [Preorder α] [TopologicalSpace α] [CompactIccSpace α] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure μ] {a : α} {b : α} : ↑↑μ (Set.Ioc a b) < ⊤

theorem measure_Ioo_lt_top {α : Type u_1} [Preorder α] [TopologicalSpace α] [CompactIccSpace α] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure μ] {a : α} {b : α} : ↑↑μ (Set.Ioo a b) < ⊤

theorem piecewise_ae_eq_restrict {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {f : α → β} {g : α → β} (hs : MeasurableSet s) : Set.piecewise s f g =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ s)] f

theorem piecewise_ae_eq_restrict_compl {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {f : α → β} {g : α → β} (hs : MeasurableSet s) : Set.piecewise s f g =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ sᶜ)] g

theorem piecewise_ae_eq_of_ae_eq_set {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} {f : α → β} {g : α → β} (hst : s =ᶠ[MeasureTheory.Measure.ae μ] t) : Set.piecewise s f g =ᶠ[MeasureTheory.Measure.ae μ] Set.piecewise t f g

theorem mem_map_indicator_ae_iff_mem_map_restrict_ae_of_zero_mem {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {f : α → β} [Zero β] {t : Set β} (ht : 0 ∈ t) (hs : MeasurableSet s) : t ∈ Filter.map (Set.indicator s f) (MeasureTheory.Measure.ae μ) ↔ t ∈ Filter.map f (MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ s))

theorem mem_map_indicator_ae_iff_of_zero_nmem {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {f : α → β} [Zero β] {t : Set β} (ht : ¬0 ∈ t) : t ∈ Filter.map (Set.indicator s f) (MeasureTheory.Measure.ae μ) ↔ ↑↑μ ((f ⁻¹' t)ᶜ ∪ sᶜ) = 0

theorem map_restrict_ae_le_map_indicator_ae {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {f : α → β} [Zero β] (hs : MeasurableSet s) : Filter.map f (MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ s)) ≤ Filter.map (Set.indicator s f) (MeasureTheory.Measure.ae μ)

theorem indicator_ae_eq_restrict {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {f : α → β} [Zero β] (hs : MeasurableSet s) : Set.indicator s f =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ s)] f

theorem indicator_ae_eq_restrict_compl {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {f : α → β} [Zero β] (hs : MeasurableSet s) : Set.indicator s f =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ sᶜ)] 0

theorem indicator_ae_eq_of_restrict_compl_ae_eq_zero {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {f : α → β} [Zero β] (hs : MeasurableSet s) (hf : f =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ sᶜ)] 0) : Set.indicator s f =ᶠ[MeasureTheory.Measure.ae μ] f

theorem indicator_ae_eq_zero_of_restrict_ae_eq_zero {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {f : α → β} [Zero β] (hs : MeasurableSet s) (hf : f =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ s)] 0) : Set.indicator s f =ᶠ[MeasureTheory.Measure.ae μ] 0

theorem indicator_ae_eq_of_ae_eq_set {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} {f : α → β} [Zero β] (hst : s =ᶠ[MeasureTheory.Measure.ae μ] t) : Set.indicator s f =ᶠ[MeasureTheory.Measure.ae μ] Set.indicator t f

theorem indicator_meas_zero {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {f : α → β} [Zero β] (hs : ↑↑μ s = 0) : Set.indicator s f =ᶠ[MeasureTheory.Measure.ae μ] 0

theorem ae_eq_restrict_iff_indicator_ae_eq {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {f : α → β} [Zero β] {g : α → β} (hs : MeasurableSet s) : f =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ s)] g ↔ Set.indicator s f =ᶠ[MeasureTheory.Measure.ae μ] Set.indicator s g