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_1} {s : Finset S} : ∀ {x : MeasurableSpace S} [inst : MeasurableSingletonClass S] (μ : MeasureTheory.Measure S), (s.sum fun (x_1 : S) => μ {x_1}) = μ ↑s

@[simp]

theorem Finset.sum_toReal_measure_singleton {S : Type u_1} {s : Finset S} : ∀ {x : MeasurableSpace S} [inst : MeasurableSingletonClass S] (μ : MeasureTheory.Measure S) [inst : MeasureTheory.IsFiniteMeasure μ], (s.sum fun (x_1 : S) => (μ {x_1}).toReal) = (μ ↑s).toReal

theorem sum_measure_singleton {S : Type u_1} [Fintype S] : ∀ {x : MeasurableSpace S} [inst : MeasurableSingletonClass S] (μ : MeasureTheory.Measure S), (Finset.univ.sum fun (x_1 : S) => μ {x_1}) = μ Set.univ

theorem sum_toReal_measure_singleton {S : Type u_1} [Fintype S] : ∀ {x : MeasurableSpace S} [inst : MeasurableSingletonClass S] (μ : MeasureTheory.Measure S) [inst : MeasureTheory.IsFiniteMeasure μ], (Finset.univ.sum fun (x_1 : S) => (μ {x_1}).toReal) = (μ Set.univ).toReal

theorem sum_measure_preimage_singleton' {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] {T : Type u} [Fintype T] [MeasurableSpace T] [MeasurableSingletonClass T] {Y : Ω → T} (hY : Measurable Y) : (Finset.univ.sum fun (y : T) => (μ (Y ⁻¹' {y})).toReal) = 1

Variant of sum_measure_preimage_singleton using real numbers rather than extended nonnegative reals.

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

theorem MeasureTheory.measure_ne_top_of_subset {α : Type u_1} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α}, s ⊆ t → μ t ≠ ⊤ → μ s ≠ ⊤

theorem MeasureTheory.measure_diff_eq_top {α : Type u_1} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α}, μ s = ⊤ → μ t ≠ ⊤ → μ (s \ t) = ⊤

theorem MeasureTheory.measure_symmDiff_eq_top {α : Type u_1} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α}, μ s ≠ ⊤ → μ t = ⊤ → μ (symmDiff s t) = ⊤

theorem MeasureTheory.measureReal_eq_zero_iff {α : Type u_1} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}, autoParam (μ s ≠ ⊤) _auto✝ → (μ.real s = 0 ↔ μ s = 0)

@[simp]

theorem MeasureTheory.measureReal_zero {α : Type u_1} : ∀ {x : MeasurableSpace α} (s : Set α), MeasureTheory.Measure.real 0 s = 0

@[simp]

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

@[simp]

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

@[simp]

theorem MeasureTheory.IsProbabilityMeasure.measureReal_univ {α : Type u_1} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.IsProbabilityMeasure μ], μ.real Set.univ = 1

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

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

theorem MeasureTheory.nonempty_of_measureReal_ne_zero {α : Type u_1} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}, μ.real s ≠ 0 → s.Nonempty

@[simp]

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

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

theorem MeasureTheory.measureReal_mono {α : Type u_1} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α}, s₁ ⊆ s₂ → autoParam (μ s₂ ≠ ⊤) _auto✝ → μ.real s₁ ≤ μ.real s₂

theorem MeasureTheory.measureReal_mono_null {α : Type u_1} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α}, s₁ ⊆ s₂ → μ.real s₂ = 0 → autoParam (μ s₂ ≠ ⊤) _auto✝ → μ.real s₁ = 0

theorem MeasureTheory.measureReal_le_measureReal_union_left {α : Type u_1} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α}, autoParam (μ t ≠ ⊤) _auto✝ → μ.real s ≤ μ.real (s ∪ t)

theorem MeasureTheory.measureReal_le_measureReal_union_right {α : Type u_1} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α}, autoParam (μ s ≠ ⊤) _auto✝ → μ.real t ≤ μ.real (s ∪ t)

theorem MeasureTheory.measureReal_union_le {α : Type u_1} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.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 α} {μ : MeasureTheory.Measure α} (s : Finset β) (f : β → Set α), μ.real (⋃ b ∈ s, f b) ≤ s.sum fun (p : β) => μ.real (f p)

theorem MeasureTheory.measureReal_iUnion_fintype_le {α : Type u_1} {β : Type u_2} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : Fintype β] (f : β → Set α), μ.real (⋃ (b : β), f b) ≤ Finset.univ.sum fun (p : β) => μ.real (f p)

theorem MeasureTheory.measureReal_iUnion_fintype {α : Type u_1} {β : Type u_2} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : Fintype β] {f : β → Set α}, Pairwise (Disjoint on f) → (∀ (i : β), MeasurableSet (f i)) → autoParam (∀ (i : β), μ (f i) ≠ ⊤) _auto✝ → μ.real (⋃ (b : β), f b) = Finset.univ.sum fun (p : β) => μ.real (f p)

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

@[simp]

theorem MeasureTheory.measureReal_union_null_iff {α : Type u_1} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α}, autoParam (μ s₁ ≠ ⊤) _auto✝ → autoParam (μ s₂ ≠ ⊤) _auto✝¹ → (μ.real (s₁ ∪ s₂) = 0 ↔ μ.real s₁ = 0 ∧ μ.real s₂ = 0)

theorem MeasureTheory.measureReal_congr {α : Type u_1} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α}, μ.ae.EventuallyEq 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_1} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set α} (s : Set α), MeasureTheory.NullMeasurableSet t μ → autoParam (μ s ≠ ⊤) _auto✝ → μ.real (s ∩ t) + μ.real (s \ t) = μ.real s

theorem MeasureTheory.measureReal_union_add_inter₀ {α : Type u_1} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set α} (s : Set α), MeasureTheory.NullMeasurableSet t μ → autoParam (μ s ≠ ⊤) _auto✝ → autoParam (μ t ≠ ⊤) _auto✝¹ → μ.real (s ∪ t) + μ.real (s ∩ t) = μ.real s + μ.real t

theorem MeasureTheory.measureReal_union_add_inter₀' {α : Type u_1} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}, MeasureTheory.NullMeasurableSet s μ → ∀ (t : Set α), autoParam (μ s ≠ ⊤) _auto✝ → autoParam (μ t ≠ ⊤) _auto✝¹ → μ.real (s ∪ t) + μ.real (s ∩ t) = μ.real s + μ.real t

theorem MeasureTheory.measureReal_union₀ {α : Type u_1} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α}, MeasureTheory.NullMeasurableSet t μ → MeasureTheory.AEDisjoint μ s t → autoParam (μ s ≠ ⊤) _auto✝ → autoParam (μ t ≠ ⊤) _auto✝¹ → μ.real (s ∪ t) = μ.real s + μ.real t

theorem MeasureTheory.measureReal_union₀' {α : Type u_1} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α}, MeasureTheory.NullMeasurableSet s μ → MeasureTheory.AEDisjoint μ s t → autoParam (μ s ≠ ⊤) _auto✝ → autoParam (μ t ≠ ⊤) _auto✝¹ → μ.real (s ∪ t) = μ.real s + μ.real t

theorem MeasureTheory.measureReal_add_measureReal_compl₀ {α : Type u_1} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.IsFiniteMeasure μ] {s : Set α}, MeasureTheory.NullMeasurableSet s μ → μ.real s + μ.real sᶜ = μ.real Set.univ

theorem MeasureTheory.measureReal_union {α : Type u_1} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α}, Disjoint s₁ s₂ → MeasurableSet s₂ → autoParam (μ s₁ ≠ ⊤) _auto✝ → autoParam (μ s₂ ≠ ⊤) _auto✝¹ → μ.real (s₁ ∪ s₂) = μ.real s₁ + μ.real s₂

theorem MeasureTheory.measureReal_union' {α : Type u_1} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α}, Disjoint s₁ s₂ → MeasurableSet s₁ → autoParam (μ s₁ ≠ ⊤) _auto✝ → autoParam (μ s₂ ≠ ⊤) _auto✝¹ → μ.real (s₁ ∪ s₂) = μ.real s₁ + μ.real s₂

theorem MeasureTheory.measureReal_inter_add_diff {α : Type u_1} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set α} (s : Set α), MeasurableSet t → autoParam (μ s ≠ ⊤) _auto✝ → μ.real (s ∩ t) + μ.real (s \ t) = μ.real s

theorem MeasureTheory.measureReal_diff_add_inter {α : Type u_1} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set α} (s : Set α), MeasurableSet t → autoParam (μ s ≠ ⊤) _auto✝ → μ.real (s \ t) + μ.real (s ∩ t) = μ.real s

theorem MeasureTheory.measureReal_union_add_inter {α : Type u_1} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set α} (s : Set α), MeasurableSet t → autoParam (μ s ≠ ⊤) _auto✝ → autoParam (μ t ≠ ⊤) _auto✝¹ → μ.real (s ∪ t) + μ.real (s ∩ t) = μ.real s + μ.real t

theorem MeasureTheory.measureReal_union_add_inter' {α : Type u_1} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}, MeasurableSet s → ∀ (t : Set α), autoParam (μ s ≠ ⊤) _auto✝ → autoParam (μ t ≠ ⊤) _auto✝¹ → μ.real (s ∪ t) + μ.real (s ∩ t) = μ.real s + μ.real t

theorem MeasureTheory.measureReal_symmDiff_eq {α : Type u_1} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α}, MeasurableSet s → MeasurableSet t → autoParam (μ s ≠ ⊤) _auto✝ → autoParam (μ t ≠ ⊤) _auto✝¹ → μ.real (symmDiff s t) = μ.real (s \ t) + μ.real (t \ s)

theorem MeasureTheory.measureReal_symmDiff_le {α : Type u_1} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s t u : Set α), autoParam (μ s ≠ ⊤) _auto✝ → autoParam (μ t ≠ ⊤) _auto✝¹ → μ.real (symmDiff s u) ≤ μ.real (symmDiff s t) + μ.real (symmDiff t u)

theorem MeasureTheory.measureReal_add_measureReal_compl {α : Type u_1} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [inst : MeasureTheory.IsFiniteMeasure μ], MeasurableSet s → μ.real s + μ.real sᶜ = μ.real Set.univ

theorem MeasureTheory.measureReal_biUnion_finset₀ {α : Type u_1} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Type u_3} {s : Finset ι} {f : ι → Set α}, (↑s).Pairwise (MeasureTheory.AEDisjoint μ on f) → (∀ b ∈ s, MeasureTheory.NullMeasurableSet (f b) μ) → autoParam (∀ b ∈ s, μ (f b) ≠ ⊤) _auto✝ → μ.real (⋃ b ∈ s, f b) = s.sum fun (p : ι) => μ.real (f p)

theorem MeasureTheory.measureReal_biUnion_finset {α : Type u_1} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Type u_3} {s : Finset ι} {f : ι → Set α}, (↑s).PairwiseDisjoint f → (∀ b ∈ s, MeasurableSet (f b)) → autoParam (∀ b ∈ s, μ (f b) ≠ ⊤) _auto✝ → μ.real (⋃ b ∈ s, f b) = s.sum fun (p : ι) => μ.real (f p)

theorem MeasureTheory.sum_measureReal_preimage_singleton {α : Type u_1} {β : Type u_2} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Finset β) {f : α → β}, (∀ y ∈ s, MeasurableSet (f ⁻¹' {y})) → autoParam (∀ a ∈ s, μ (f ⁻¹' {a}) ≠ ⊤) _auto✝ → (s.sum fun (b : β) => μ.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 α} {μ : MeasureTheory.Measure α} [inst : MeasurableSingletonClass α] [inst : MeasureTheory.IsFiniteMeasure μ] (s : Finset α), (s.sum fun (b : α) => μ.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 α} {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α}, μ.real (s₁ ∩ s₂) = 0 → autoParam (μ s₁ ≠ ⊤) _auto✝ → μ.real (s₁ \ s₂) = μ.real s₁

theorem MeasureTheory.measureReal_diff_null {α : Type u_1} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α}, μ.real s₂ = 0 → autoParam (μ s₂ ≠ ⊤) _auto✝ → μ.real (s₁ \ s₂) = μ.real s₁

theorem MeasureTheory.measureReal_add_diff {α : Type u_1} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}, MeasurableSet s → ∀ (t : Set α), autoParam (μ s ≠ ⊤) _auto✝ → autoParam (μ t ≠ ⊤) _auto✝¹ → μ.real s + μ.real (t \ s) = μ.real (s ∪ t)

theorem MeasureTheory.measureReal_diff' {α : Type u_1} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set α} (s : Set α), MeasurableSet t → autoParam (μ s ≠ ⊤) _auto✝ → autoParam (μ t ≠ ⊤) _auto✝¹ → μ.real (s \ t) = μ.real (s ∪ t) - μ.real t

theorem MeasureTheory.measureReal_diff {α : Type u_1} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α}, s₂ ⊆ s₁ → MeasurableSet s₂ → autoParam (μ s₁ ≠ ⊤) _auto✝ → μ.real (s₁ \ s₂) = μ.real s₁ - μ.real s₂

theorem MeasureTheory.le_measureReal_diff {α : Type u_1} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α}, autoParam (μ s₂ ≠ ⊤) _auto✝ → μ.real s₁ - μ.real s₂ ≤ μ.real (s₁ \ s₂)

theorem MeasureTheory.measureReal_diff_lt_of_lt_add {α : Type u_1} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α}, MeasurableSet s → s ⊆ t → ∀ (ε : ℝ), μ.real t < μ.real s + ε → autoParam (μ t ≠ ⊤) _auto✝ → μ.real (t \ s) < ε

theorem MeasureTheory.measureReal_diff_le_iff_le_add {α : Type u_1} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α}, MeasurableSet s → s ⊆ t → ∀ (ε : ℝ), autoParam (μ t ≠ ⊤) _auto✝ → (μ.real (t \ s) ≤ ε ↔ μ.real t ≤ μ.real s + ε)

theorem MeasureTheory.measureReal_eq_measureReal_of_null_diff {α : Type u_1} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α}, s ⊆ t → μ.real (t \ s) = 0 → autoParam (μ (t \ s) ≠ ⊤) _auto✝ → μ.real s = μ.real t

theorem MeasureTheory.measureReal_eq_measureReal_of_between_null_diff {α : Type u_1} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ s₃ : Set α}, s₁ ⊆ s₂ → s₂ ⊆ s₃ → μ.real (s₃ \ s₁) = 0 → autoParam (μ (s₃ \ s₁) ≠ ⊤) _auto✝ → μ.real s₁ = μ.real s₂ ∧ μ.real s₂ = μ.real s₃

theorem MeasureTheory.measureReal_eq_measureReal_smaller_of_between_null_diff {α : Type u_1} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ s₃ : Set α}, s₁ ⊆ s₂ → s₂ ⊆ s₃ → μ.real (s₃ \ s₁) = 0 → autoParam (μ (s₃ \ s₁) ≠ ⊤) _auto✝ → μ.real s₁ = μ.real s₂

theorem MeasureTheory.measureReal_eq_measureReal_larger_of_between_null_diff {α : Type u_1} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ s₃ : Set α}, s₁ ⊆ s₂ → s₂ ⊆ s₃ → μ.real (s₃ \ s₁) = 0 → autoParam (μ (s₃ \ s₁) ≠ ⊤) _auto✝ → μ.real s₂ = μ.real s₃

theorem MeasureTheory.measureReal_compl {α : Type u_1} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [inst : MeasureTheory.IsFiniteMeasure μ], MeasurableSet s → μ.real sᶜ = μ.real Set.univ - μ.real s

theorem MeasureTheory.measureReal_union_congr_of_subset {α : Type u_1} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ t₁ t₂ : Set α}, s₁ ⊆ s₂ → μ.real s₂ ≤ μ.real s₁ → t₁ ⊆ t₂ → μ.real t₂ ≤ μ.real t₁ → autoParam (μ s₂ ≠ ⊤) _auto✝ → autoParam (μ t₂ ≠ ⊤) _auto✝¹ → μ.real (s₁ ∪ t₁) = μ.real (s₂ ∪ t₂)

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

theorem MeasureTheory.exists_nonempty_inter_of_measureReal_univ_lt_sum_measureReal {α : Type u_1} {ι : Type u_3} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] {s : Finset ι} {t : ι → Set α} (h : ∀ i ∈ s, MeasurableSet (t i)) (H : μ.real Set.univ < s.sum fun (i : ι) => μ.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_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) {s : Set α} {t : Set α} {u : Set α} (ht : MeasurableSet t) (h's : s ⊆ u) (h't : t ⊆ u) (h : μ.real u < μ.real s + μ.real t) (hu : autoParam (μ u ≠ ⊤) _auto✝) : (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} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) {s : Set α} {t : Set α} {u : Set α} (hs : MeasurableSet s) (h's : s ⊆ u) (h't : t ⊆ u) (h : μ.real u < μ.real s + μ.real t) (hu : autoParam (μ u ≠ ⊤) _auto✝) : (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 α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_1 : MeasureTheory.SigmaFinite ν] (s : Set α) (t : Set β), (μ.prod ν).real (s ×ˢ t) = μ.real s * ν.real t

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

Generalized in Measure.ext_iff_singleton_finiteSupport at Entropy.Measure

theorem MeasureTheory.ext_iff_measureReal_singleton {S : Type u_3} [Fintype S] [MeasurableSpace S] [MeasurableSingletonClass S] {μ1 : MeasureTheory.Measure S} {μ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.

theorem measureReal_preimage_fst_singleton_eq_sum {S : Type u_1} {T : Type u_2} : ∀ {x : MeasurableSpace S} [inst : MeasurableSingletonClass S] [inst : Fintype T] {x_1 : MeasurableSpace T} [inst_1 : MeasurableSingletonClass T] (μ : MeasureTheory.Measure (S × T)) [inst_2 : MeasureTheory.IsFiniteMeasure μ] (x_2 : S), μ.real (Prod.fst ⁻¹' {x_2}) = Finset.univ.sum fun (y : T) => μ.real {(x_2, y)}

theorem measureReal_preimage_snd_singleton_eq_sum {S : Type u_1} {T : Type u_2} [Fintype S] : ∀ {x : MeasurableSpace S} [inst : MeasurableSingletonClass S] {x_1 : MeasurableSpace T} [inst : MeasurableSingletonClass T] (μ : MeasureTheory.Measure (S × T)) [inst : MeasureTheory.IsFiniteMeasure μ] (y : T), μ.real (Prod.snd ⁻¹' {y}) = Finset.univ.sum fun (x_2 : S) => μ.real {(x_2, y)}