Measures as real-valued functions

Given a measure μ, we define μ.real as the function sending a set s to (μ s).toReal, and develop a basic API around this.

We essentially copy relevant lemmas from the files MeasureSpaceDef.lean, NullMeasurable.lean and MeasureSpace.lean, and adapt them by replacing in their name measure with measureReal.

Many lemmas require an assumption that some set has finite measure. These assumptions are written in the form (h : μ s ≠ ∞ := by finiteness), where finiteness is a tactic for goals of the form ≠ ∞.

There are certainly many missing lemmas. The missing ones should be added as they are needed.

There are no lemmas on infinite sums, as summability issues are really more painful with reals than nonnegative extended reals. They should probably be added in the long run.

def MeasureTheory.Measure.real {α : Type u_1} {x✝ : MeasurableSpace α} (μ : Measure α) (s : Set α) : ℝ

The real-valued version of a measure. Maps infinite measure sets to zero. Use as μ.real s.

Equations

• μ.real s = (μ s).toReal

theorem MeasureTheory.measureReal_def {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} (s : Set α) : μ.real s = (μ s).toReal

theorem MeasureTheory.Measure.real_def {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} (s : Set α) : μ.real s = (μ s).toReal

Alias of MeasureTheory.measureReal_def.

theorem MeasureTheory.measureReal_eq_zero_iff {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} {s : Set α} (h : μ s ≠ ⊤ := by finiteness) : μ.real s = 0 ↔ μ s = 0

@[simp]

theorem MeasureTheory.measureReal_zero {α : Type u_1} {x✝ : MeasurableSpace α} : Measure.real 0 = 0

theorem MeasureTheory.measureReal_zero_apply {α : Type u_1} {x✝ : MeasurableSpace α} (s : Set α) : Measure.real 0 s = 0

@[simp]

theorem MeasureTheory.measureReal_nonneg {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} {s : Set α} : 0 ≤ μ.real s

@[simp]

theorem MeasureTheory.measureReal_empty {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} : μ.real ∅ = 0

@[simp]

theorem MeasureTheory.measureReal_univ_eq_one {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} [IsProbabilityMeasure μ] : μ.real Set.univ = 1

theorem MeasureTheory.measureReal_univ_pos {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} [IsFiniteMeasure μ] [NeZero μ] : 0 < μ.real Set.univ

theorem MeasureTheory.measureReal_univ_ne_zero {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} [IsFiniteMeasure μ] [NeZero μ] : μ.real Set.univ ≠ 0

theorem MeasureTheory.nonempty_of_measureReal_ne_zero {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} {s : Set α} (h : μ.real s ≠ 0) : s.Nonempty

@[simp]

theorem MeasureTheory.measureReal_ennreal_smul_apply {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} {s : Set α} (c : ENNReal) : (c • μ).real s = c.toReal * μ.real s

@[simp]

theorem MeasureTheory.measureReal_nnreal_smul_apply {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} {s : Set α} (c : NNReal) : (c • μ).real s = ↑c * μ.real s

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

theorem MeasureTheory.measureReal_mono {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} {s₁ s₂ : Set α} (h : s₁ ⊆ s₂) (h₂ : μ s₂ ≠ ⊤ := by finiteness) : μ.real s₁ ≤ μ.real s₂

theorem MeasureTheory.measureReal_mono_null {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} {s₁ s₂ : Set α} (h : s₁ ⊆ s₂) (h₂ : μ.real s₂ = 0) (h'₂ : μ s₂ ≠ ⊤ := by finiteness) : μ.real s₁ = 0

theorem MeasureTheory.measureReal_le_measureReal_union_left {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} {s t : Set α} (h : μ t ≠ ⊤ := by finiteness) : μ.real s ≤ μ.real (s ∪ t)

theorem MeasureTheory.measureReal_le_measureReal_union_right {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} {s t : Set α} (h : μ s ≠ ⊤ := by finiteness) : μ.real t ≤ μ.real (s ∪ t)

theorem MeasureTheory.measureReal_union_le {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} (s₁ s₂ : Set α) : μ.real (s₁ ∪ s₂) ≤ μ.real s₁ + μ.real s₂

theorem MeasureTheory.measureReal_biUnion_finset_le {α : Type u_1} {β : Type u_2} {x✝ : MeasurableSpace α} {μ : Measure α} (s : Finset β) (f : β → Set α) : μ.real (⋃ b ∈ s, f b) ≤ ∑ p ∈ s, μ.real (f p)

theorem MeasureTheory.measureReal_iUnion_fintype_le {α : Type u_1} {β : Type u_2} {x✝ : MeasurableSpace α} {μ : Measure α} [Fintype β] (f : β → Set α) : μ.real (⋃ (b : β), f b) ≤ ∑ p : β, μ.real (f p)

theorem MeasureTheory.measureReal_iUnion_fintype {α : Type u_1} {β : Type u_2} {x✝ : MeasurableSpace α} {μ : Measure α} [Fintype β] {f : β → Set α} (hn : Pairwise (Function.onFun Disjoint f)) (h : ∀ (i : β), MeasurableSet (f i)) (h' : ∀ (i : β), μ (f i) ≠ ⊤ := by finiteness) : μ.real (⋃ (b : β), f b) = ∑ p : β, μ.real (f p)

theorem MeasureTheory.measureReal_union_null {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} {s₁ s₂ : Set α} (h₁ : μ.real s₁ = 0) (h₂ : μ.real s₂ = 0) : μ.real (s₁ ∪ s₂) = 0

@[simp]

theorem MeasureTheory.measureReal_union_null_iff {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} {s₁ s₂ : Set α} (h₁ : μ s₁ ≠ ⊤ := by finiteness) (h₂ : μ s₂ ≠ ⊤ := by finiteness) : μ.real (s₁ ∪ s₂) = 0 ↔ μ.real s₁ = 0 ∧ μ.real s₂ = 0

theorem MeasureTheory.measureReal_congr {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} {s t : Set α} (H : s =ᶠ[ae μ] t) : μ.real s = μ.real t

If two sets are equal modulo a set of measure zero, then μ.real s = μ.real t.

theorem MeasureTheory.measureReal_inter_add_diff₀ {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} {t : Set α} (s : Set α) (ht : NullMeasurableSet t μ) (h : μ s ≠ ⊤ := by finiteness) : μ.real (s ∩ t) + μ.real (s \ t) = μ.real s

theorem MeasureTheory.measureReal_union_add_inter₀ {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} {t : Set α} (s : Set α) (ht : NullMeasurableSet t μ) (h₁ : μ s ≠ ⊤ := by finiteness) (h₂ : μ t ≠ ⊤ := by finiteness) : μ.real (s ∪ t) + μ.real (s ∩ t) = μ.real s + μ.real t

theorem MeasureTheory.measureReal_union_add_inter₀' {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} {s : Set α} (hs : NullMeasurableSet s μ) (t : Set α) (h₁ : μ s ≠ ⊤ := by finiteness) (h₂ : μ t ≠ ⊤ := by finiteness) : μ.real (s ∪ t) + μ.real (s ∩ t) = μ.real s + μ.real t

theorem MeasureTheory.measureReal_union₀ {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} {s t : Set α} (ht : NullMeasurableSet t μ) (hd : AEDisjoint μ s t) (h₁ : μ s ≠ ⊤ := by finiteness) (h₂ : μ t ≠ ⊤ := by finiteness) : μ.real (s ∪ t) = μ.real s + μ.real t

theorem MeasureTheory.measureReal_union₀' {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} {s t : Set α} (hs : NullMeasurableSet s μ) (hd : AEDisjoint μ s t) (h₁ : μ s ≠ ⊤ := by finiteness) (h₂ : μ t ≠ ⊤ := by finiteness) : μ.real (s ∪ t) = μ.real s + μ.real t

theorem MeasureTheory.measureReal_add_measureReal_compl₀ {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} {s : Set α} [IsFiniteMeasure μ] (hs : NullMeasurableSet s μ) : μ.real s + μ.real sᶜ = μ.real Set.univ

theorem MeasureTheory.measureReal_add_measureReal_compl {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} {s : Set α} [IsFiniteMeasure μ] (h : MeasurableSet s) : μ.real s + μ.real sᶜ = μ.real Set.univ

theorem MeasureTheory.measureReal_union {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} {s₁ s₂ : Set α} (hd : Disjoint s₁ s₂) (h : MeasurableSet s₂) (h₁ : μ s₁ ≠ ⊤ := by finiteness) (h₂ : μ s₂ ≠ ⊤ := by finiteness) : μ.real (s₁ ∪ s₂) = μ.real s₁ + μ.real s₂

theorem MeasureTheory.measureReal_union' {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} {s₁ s₂ : Set α} (hd : Disjoint s₁ s₂) (h : MeasurableSet s₁) (h₁ : μ s₁ ≠ ⊤ := by finiteness) (h₂ : μ s₂ ≠ ⊤ := by finiteness) : μ.real (s₁ ∪ s₂) = μ.real s₁ + μ.real s₂

theorem MeasureTheory.measureReal_inter_add_diff {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} {t : Set α} (s : Set α) (ht : MeasurableSet t) (h : μ s ≠ ⊤ := by finiteness) : μ.real (s ∩ t) + μ.real (s \ t) = μ.real s

theorem MeasureTheory.measureReal_diff_add_inter {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} {t : Set α} (s : Set α) (ht : MeasurableSet t) (h : μ s ≠ ⊤ := by finiteness) : μ.real (s \ t) + μ.real (s ∩ t) = μ.real s

theorem MeasureTheory.measureReal_union_add_inter {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} {t : Set α} (s : Set α) (ht : MeasurableSet t) (h₁ : μ s ≠ ⊤ := by finiteness) (h₂ : μ t ≠ ⊤ := by finiteness) : μ.real (s ∪ t) + μ.real (s ∩ t) = μ.real s + μ.real t

theorem MeasureTheory.measureReal_union_add_inter' {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} {s : Set α} (hs : MeasurableSet s) (t : Set α) (h₁ : μ s ≠ ⊤ := by finiteness) (h₂ : μ t ≠ ⊤ := by finiteness) : μ.real (s ∪ t) + μ.real (s ∩ t) = μ.real s + μ.real t

theorem MeasureTheory.measureReal_symmDiff_eq {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} {s t : Set α} (hs : MeasurableSet s) (ht : MeasurableSet t) (h₁ : μ s ≠ ⊤ := by finiteness) (h₂ : μ t ≠ ⊤ := by finiteness) : μ.real (symmDiff s t) = μ.real (s \ t) + μ.real (t \ s)

theorem MeasureTheory.measureReal_symmDiff_le {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} (s t u : Set α) (h₁ : μ s ≠ ⊤ := by finiteness) (h₂ : μ t ≠ ⊤ := by finiteness) : μ.real (symmDiff s u) ≤ μ.real (symmDiff s t) + μ.real (symmDiff t u)

theorem MeasureTheory.measureReal_biUnion_finset₀ {α : Type u_1} {ι : Type u_3} {x✝ : MeasurableSpace α} {μ : Measure α} {s : Finset ι} {f : ι → Set α} (hd : (↑s).Pairwise (Function.onFun (AEDisjoint μ) f)) (hm : ∀ b ∈ s, NullMeasurableSet (f b) μ) (h : ∀ b ∈ s, μ (f b) ≠ ⊤ := by finiteness) : μ.real (⋃ b ∈ s, f b) = ∑ p ∈ s, μ.real (f p)

theorem MeasureTheory.measureReal_biUnion_finset {α : Type u_1} {ι : Type u_3} {x✝ : MeasurableSpace α} {μ : Measure α} {s : Finset ι} {f : ι → Set α} (hd : (↑s).PairwiseDisjoint f) (hm : ∀ b ∈ s, MeasurableSet (f b)) (h : ∀ b ∈ s, μ (f b) ≠ ⊤ := by finiteness) : μ.real (⋃ b ∈ s, f b) = ∑ p ∈ s, μ.real (f p)

theorem MeasureTheory.sum_measureReal_preimage_singleton {α : Type u_1} {β : Type u_2} {x✝ : MeasurableSpace α} {μ : Measure α} (s : Finset β) {f : α → β} (hf : ∀ y ∈ s, MeasurableSet (f ⁻¹' {y})) (h : ∀ a ∈ s, μ (f ⁻¹' {a}) ≠ ⊤ := by finiteness) : ∑ b ∈ s, μ.real (f ⁻¹' {b}) = μ.real (f ⁻¹' ↑s)

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

@[simp]

theorem MeasureTheory.Finset.sum_realMeasure_singleton {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} [MeasurableSingletonClass α] [SigmaFinite μ] (s : Finset α) : ∑ b ∈ s, μ.real {b} = μ.real ↑s

If s is a Finset, then the sums of the real measures of the singletons in the set is the real measure of the set.

theorem MeasureTheory.measureReal_diff_null' {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} {s₁ s₂ : Set α} (h : μ.real (s₁ ∩ s₂) = 0) (h' : μ s₁ ≠ ⊤ := by finiteness) : μ.real (s₁ \ s₂) = μ.real s₁

theorem MeasureTheory.measureReal_diff_null {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} {s₁ s₂ : Set α} (h : μ.real s₂ = 0) (h' : μ s₂ ≠ ⊤ := by finiteness) : μ.real (s₁ \ s₂) = μ.real s₁

theorem MeasureTheory.measureReal_add_diff {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} {s : Set α} (hs : MeasurableSet s) (t : Set α) (h₁ : μ s ≠ ⊤ := by finiteness) (h₂ : μ t ≠ ⊤ := by finiteness) : μ.real s + μ.real (t \ s) = μ.real (s ∪ t)

theorem MeasureTheory.measureReal_diff' {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} {t : Set α} (s : Set α) (hm : MeasurableSet t) (h₁ : μ s ≠ ⊤ := by finiteness) (h₂ : μ t ≠ ⊤ := by finiteness) : μ.real (s \ t) = μ.real (s ∪ t) - μ.real t

theorem MeasureTheory.measureReal_diff {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} {s₁ s₂ : Set α} (h : s₂ ⊆ s₁) (h₂ : MeasurableSet s₂) (h₁ : μ s₁ ≠ ⊤ := by finiteness) : μ.real (s₁ \ s₂) = μ.real s₁ - μ.real s₂

theorem MeasureTheory.le_measureReal_diff {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} {s₁ s₂ : Set α} (h : μ s₂ ≠ ⊤ := by finiteness) : μ.real s₁ - μ.real s₂ ≤ μ.real (s₁ \ s₂)

theorem MeasureTheory.measureReal_diff_lt_of_lt_add {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} {s t : Set α} (hs : MeasurableSet s) (hst : s ⊆ t) (ε : ℝ) (h : μ.real t < μ.real s + ε) (ht' : μ t ≠ ⊤ := by finiteness) : μ.real (t \ s) < ε

theorem MeasureTheory.measureReal_diff_le_iff_le_add {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} {s t : Set α} (hs : MeasurableSet s) (hst : s ⊆ t) (ε : ℝ) (ht' : μ t ≠ ⊤ := by finiteness) : μ.real (t \ s) ≤ ε ↔ μ.real t ≤ μ.real s + ε

theorem MeasureTheory.measureReal_eq_measureReal_of_null_diff {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} {s t : Set α} (hst : s ⊆ t) (h_nulldiff : μ.real (t \ s) = 0) (h : μ (t \ s) ≠ ⊤ := by finiteness) : μ.real s = μ.real t

theorem MeasureTheory.measureReal_eq_measureReal_of_between_null_diff {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} {s₁ s₂ s₃ : Set α} (h12 : s₁ ⊆ s₂) (h23 : s₂ ⊆ s₃) (h_nulldiff : μ.real (s₃ \ s₁) = 0) (h' : μ (s₃ \ s₁) ≠ ⊤ := by finiteness) : μ.real s₁ = μ.real s₂ ∧ μ.real s₂ = μ.real s₃

theorem MeasureTheory.measureReal_eq_measureReal_smaller_of_between_null_diff {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} {s₁ s₂ s₃ : Set α} (h12 : s₁ ⊆ s₂) (h23 : s₂ ⊆ s₃) (h_nulldiff : μ.real (s₃ \ s₁) = 0) (h' : μ (s₃ \ s₁) ≠ ⊤ := by finiteness) : μ.real s₁ = μ.real s₂

theorem MeasureTheory.measureReal_eq_measureReal_larger_of_between_null_diff {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} {s₁ s₂ s₃ : Set α} (h12 : s₁ ⊆ s₂) (h23 : s₂ ⊆ s₃) (h_nulldiff : μ.real (s₃ \ s₁) = 0) (h' : μ (s₃ \ s₁) ≠ ⊤ := by finiteness) : μ.real s₂ = μ.real s₃

theorem MeasureTheory.measureReal_compl {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} {s : Set α} [IsFiniteMeasure μ] (h₁ : MeasurableSet s) : μ.real sᶜ = μ.real Set.univ - μ.real s

theorem MeasureTheory.measureReal_union_congr_of_subset {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} {s₁ s₂ t₁ t₂ : Set α} (hs : s₁ ⊆ s₂) (hsμ : μ.real s₂ ≤ μ.real s₁) (ht : t₁ ⊆ t₂) (htμ : μ.real t₂ ≤ μ.real t₁) (h₁ : μ s₂ ≠ ⊤ := by finiteness) (h₂ : μ t₂ ≠ ⊤ := by finiteness) : μ.real (s₁ ∪ t₁) = μ.real (s₂ ∪ t₂)

theorem MeasureTheory.sum_measureReal_le_measureReal_univ {α : Type u_1} {ι : Type u_3} {x✝ : MeasurableSpace α} {μ : Measure α} [IsFiniteMeasure μ] {s : Finset ι} {t : ι → Set α} (h : ∀ i ∈ s, MeasurableSet (t i)) (H : (↑s).PairwiseDisjoint t) : ∑ i ∈ s, μ.real (t i) ≤ μ.real Set.univ

theorem MeasureTheory.exists_nonempty_inter_of_measureReal_univ_lt_sum_measureReal {α : Type u_1} {ι : Type u_3} {x✝ : MeasurableSpace α} {μ : Measure α} [IsFiniteMeasure μ] {s : Finset ι} {t : ι → Set α} (h : ∀ i ∈ s, MeasurableSet (t i)) (H : μ.real Set.univ < ∑ i ∈ s, μ.real (t i)) : ∃ i ∈ s, ∃ j ∈ s, ∃ (_ : i ≠ j), (t i ∩ t j).Nonempty

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

theorem MeasureTheory.nonempty_inter_of_measureReal_lt_add {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} {s t u : Set α} (ht : MeasurableSet t) (h's : s ⊆ u) (h't : t ⊆ u) (h : μ.real u < μ.real s + μ.real t) (hu : μ u ≠ ⊤ := by finiteness) : (s ∩ t).Nonempty

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

theorem MeasureTheory.nonempty_inter_of_measureReal_lt_add' {α : Type u_1} {x✝ : MeasurableSpace α} {μ : Measure α} {s t u : Set α} (hs : MeasurableSet s) (h's : s ⊆ u) (h't : t ⊆ u) (h : μ.real u < μ.real s + μ.real t) (hu : μ u ≠ ⊤ := by finiteness) : (s ∩ t).Nonempty

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

theorem MeasureTheory.measureReal_prod_prod {α : Type u_1} {β : Type u_2} {x✝ : MeasurableSpace α} {μ : Measure α} {x✝¹ : MeasurableSpace β} {ν : Measure β} [SigmaFinite ν] (s : Set α) (t : Set β) : (μ.prod ν).real (s ×ˢ t) = μ.real s * ν.real t

theorem MeasureTheory.ext_iff_measureReal_singleton {S : Type u_4} [Countable S] [MeasurableSpace S] {μ1 μ2 : Measure S} [IsFiniteMeasure μ1] [IsFiniteMeasure μ2] : μ1 = μ2 ↔ ∀ (x : S), μ1.real {x} = μ2.real {x}

def Mathlib.Meta.Positivity.evalMeasureReal : PositivityExt

Extension for the positivity tactic: applications of μ.real are nonnegative.

Equations

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