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 new tactic (still in prototype form) for goals of the form ≠ ∞.

There are certainly many missing lemmas. The idea is to add the missing ones as we notice that they would be useful while doing the project.

I haven't transferred any lemma involving infinite sums, as summability issues are really more painful with reals than nonnegative extended reals. I don't expect we will need them in the project, but we should probably add them back in the long run if they turn out to be useful.

@[simp]

theorem Finset.sum_measure_singleton {S : Type u_2} {s : Finset S} {x✝ : MeasurableSpace S} [MeasurableSingletonClass S] (μ : MeasureTheory.Measure S) : ∑ x ∈ s, μ {x} = μ ↑s

@[simp]

theorem Finset.sum_toReal_measure_singleton {S : Type u_2} {s : Finset S} {x✝ : MeasurableSpace S} [MeasurableSingletonClass S] (μ : MeasureTheory.Measure S) [MeasureTheory.IsFiniteMeasure μ] : ∑ x ∈ s, (μ {x}).toReal = (μ ↑s).toReal

theorem sum_measure_singleton {S : Type u_2} [Fintype S] {x✝ : MeasurableSpace S} [MeasurableSingletonClass S] (μ : MeasureTheory.Measure S) : ∑ x : S, μ {x} = μ Set.univ

theorem sum_toReal_measure_singleton {S : Type u_2} [Fintype S] {x✝ : MeasurableSpace S} [MeasurableSingletonClass S] (μ : MeasureTheory.Measure S) [MeasureTheory.IsFiniteMeasure μ] : ∑ x : S, (μ {x}).toReal = (μ Set.univ).toReal

def MeasureTheory.Measure.real {α : Type u_2} {x✝ : MeasurableSpace α} (μ : MeasureTheory.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_2} {x✝ : MeasurableSpace α} (μ : MeasureTheory.Measure α) (s : Set α) : μ.real s = (μ s).toReal

def MeasureTheory.Measure.nnreal {α : Type u_2} {x✝ : MeasurableSpace α} (μ : MeasureTheory.Measure α) (s : Set α) : NNReal

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

Equations

• μ.nnreal s = (μ s).toNNReal

theorem MeasureTheory.measureNNReal_def {α : Type u_2} {x✝ : MeasurableSpace α} (μ : MeasureTheory.Measure α) (s : Set α) : μ.nnreal s = (μ s).toNNReal

theorem MeasureTheory.measureNNReal_toReal {α : Type u_2} {x✝ : MeasurableSpace α} (μ : MeasureTheory.Measure α) (s : Set α) : ↑(μ.nnreal s) = μ.real s

theorem MeasureTheory.measureNNReal_val {α : Type u_2} {x✝ : MeasurableSpace α} (μ : MeasureTheory.Measure α) (s : Set α) : ↑(μ.nnreal s) = μ.real s

theorem MeasureTheory.measure_ne_top_of_subset {α : Type u_2} {x✝ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α} (h : s ⊆ t) (ht : μ t ≠ ⊤) : μ s ≠ ⊤

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

@[simp]

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

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

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

theorem MeasureTheory.measureReal_mono_null {α : Type u_2} {x✝ : MeasurableSpace α} {μ : MeasureTheory.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_2} {x✝ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α} (h : μ t ≠ ⊤ := by finiteness) : μ.real s ≤ μ.real (s ∪ t)

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

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

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

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

theorem MeasureTheory.measureReal_iUnion_fintype {α : Type u_2} {β : Type u_3} {x✝ : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Fintype β] {f : β → Set α} (hn : Pairwise (Disjoint on 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_2} {x✝ : MeasurableSpace α} {μ : MeasureTheory.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_2} {x✝ : MeasurableSpace α} {μ : MeasureTheory.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_2} {x✝ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α} (H : s =ᵐ[μ] 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_2} {x✝ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set α} (s : Set α) (ht : MeasureTheory.NullMeasurableSet t μ) (h : μ s ≠ ⊤ := by finiteness) : μ.real (s ∩ t) + μ.real (s \ t) = μ.real s

theorem MeasureTheory.measureReal_union_add_inter₀ {α : Type u_2} {x✝ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set α} (s : Set α) (ht : MeasureTheory.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_2} {x✝ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasureTheory.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_2} {x✝ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α} (ht : MeasureTheory.NullMeasurableSet t μ) (hd : MeasureTheory.AEDisjoint μ s t) (h₁ : μ s ≠ ⊤ := by finiteness) (h₂ : μ t ≠ ⊤ := by finiteness) : μ.real (s ∪ t) = μ.real s + μ.real t

theorem MeasureTheory.measureReal_union₀' {α : Type u_2} {x✝ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α} (hs : MeasureTheory.NullMeasurableSet s μ) (hd : MeasureTheory.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_2} {x✝ : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {s : Set α} (hs : MeasureTheory.NullMeasurableSet s μ) : μ.real s + μ.real sᶜ = μ.real Set.univ

theorem MeasureTheory.measureReal_union {α : Type u_2} {x✝ : MeasurableSpace α} {μ : MeasureTheory.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_2} {x✝ : MeasurableSpace α} {μ : MeasureTheory.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_2} {x✝ : MeasurableSpace α} {μ : MeasureTheory.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_2} {x✝ : MeasurableSpace α} {μ : MeasureTheory.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_2} {x✝ : MeasurableSpace α} {μ : MeasureTheory.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_2} {x✝ : MeasurableSpace α} {μ : MeasureTheory.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_2} {x✝ : MeasurableSpace α} {μ : MeasureTheory.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_2} {x✝ : MeasurableSpace α} {μ : MeasureTheory.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_add_measureReal_compl {α : Type u_2} {x✝ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsFiniteMeasure μ] (h : MeasurableSet s) : μ.real s + μ.real sᶜ = μ.real Set.univ

theorem MeasureTheory.measureReal_biUnion_finset₀ {ι : Type u_1} {α : Type u_2} {x✝ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Finset ι} {f : ι → Set α} (hd : (↑s).Pairwise (MeasureTheory.AEDisjoint μ on f)) (hm : ∀ b ∈ s, MeasureTheory.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_2} {x✝ : MeasurableSpace α} {μ : MeasureTheory.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_2} {β : Type u_3} {x✝ : MeasurableSpace α} {μ : MeasureTheory.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_2} {x✝ : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasurableSingletonClass α] [MeasureTheory.IsFiniteMeasure μ] (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_2} {x✝ : MeasurableSpace α} {μ : MeasureTheory.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_2} {x✝ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α} (h : μ.real s₂ = 0) (h' : μ s₂ ≠ ⊤ := by finiteness) : μ.real (s₁ \ s₂) = μ.real s₁

theorem MeasureTheory.measureReal_add_diff {α : Type u_2} {x✝ : MeasurableSpace α} {μ : MeasureTheory.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_2} {x✝ : MeasurableSpace α} {μ : MeasureTheory.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_2} {x✝ : MeasurableSpace α} {μ : MeasureTheory.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_2} {x✝ : MeasurableSpace α} {μ : MeasureTheory.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_2} {x✝ : MeasurableSpace α} {μ : MeasureTheory.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_2} {x✝ : MeasurableSpace α} {μ : MeasureTheory.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_2} {x✝ : MeasurableSpace α} {μ : MeasureTheory.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_2} {x✝ : MeasurableSpace α} {μ : MeasureTheory.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_2} {x✝ : MeasurableSpace α} {μ : MeasureTheory.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_2} {x✝ : MeasurableSpace α} {μ : MeasureTheory.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_2} {x✝ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsFiniteMeasure μ] (h₁ : MeasurableSet s) : μ.real sᶜ = μ.real Set.univ - μ.real s

theorem MeasureTheory.measureReal_union_congr_of_subset {α : Type u_2} {x✝ : MeasurableSpace α} {μ : MeasureTheory.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_2} {x✝ : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.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_2} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.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 in 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_2} {m : MeasurableSpace α} (μ : MeasureTheory.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_2} {m : MeasurableSpace α} (μ : MeasureTheory.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_2} {β : Type u_3} {x✝ : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SigmaFinite ν] (s : Set α) (t : Set β) : (μ.prod ν).real (s ×ˢ t) = μ.real s * ν.real t

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

def Mathlib.Meta.Positivity.evalMeasureReal : Mathlib.Meta.Positivity.PositivityExt

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

Equations

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