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

@[simp]

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

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

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

theorem measure_eq_univ_of_forall_singleton {X : Type u_4} [Countable X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} {s : Set X} (hμ : ∀ x ∈ sᶜ, μ {x} = 0) : μ s = μ Set.univ

theorem measure_eq_one_of_forall_singleton {X : Type u_4} [Countable X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] {s : Set X} (hμ : ∀ x ∈ sᶜ, μ {x} = 0) : μ s = 1

theorem sum_measure_preimage_singleton' {Ω : Type u_2} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] {T : Type u_4} [Fintype T] [MeasurableSpace T] [MeasurableSingletonClass T] {Y : Ω → T} (hY : Measurable Y) : ∑ 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_4} : {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_4} : ∀ {x : MeasurableSpace α} (μ : MeasureTheory.Measure α) (s : Set α), μ.real s = (μ s).toReal

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

@[simp]

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

theorem MeasureTheory.map_measureReal_apply {α : Type u_4} {β : Type u_5} : ∀ {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_4} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α}, s₁ ⊆ s₂ → autoParam (μ s₂ ≠ ⊤) _auto✝ → μ.real s₁ ≤ μ.real s₂

theorem MeasureTheory.measureReal_mono_null {α : Type u_4} : ∀ {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_4} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α}, autoParam (μ t ≠ ⊤) _auto✝ → μ.real s ≤ μ.real (s ∪ t)

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

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

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

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

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

theorem MeasureTheory.measureReal_union_null {α : Type u_4} : ∀ {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_4} : ∀ {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_4} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α}, 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_4} : ∀ {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_4} : ∀ {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_4} : ∀ {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_4} : ∀ {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_4} : ∀ {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_4} : ∀ {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_4} : ∀ {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_4} : ∀ {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_4} : ∀ {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_4} : ∀ {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_4} : ∀ {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_4} : ∀ {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_4} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α}, MeasureTheory.NullMeasurableSet s μ → MeasureTheory.NullMeasurableSet t μ → autoParam (μ s ≠ ⊤) _auto✝ → autoParam (μ t ≠ ⊤) _auto✝¹ → μ.real (symmDiff s t) = μ.real (s \ t) + μ.real (t \ s)

theorem MeasureTheory.measureReal_symmDiff_le {α : Type u_4} : ∀ {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_4} : ∀ {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} {α : Type u_4} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {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) = ∑ p ∈ s, μ.real (f p)

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

theorem MeasureTheory.sum_measureReal_preimage_singleton {α : Type u_4} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_6} (s : Finset β) {f : α → β}, (∀ y ∈ s, MeasurableSet (f ⁻¹' {y})) → autoParam (∀ a ∈ s, μ (f ⁻¹' {a}) ≠ ⊤) _auto✝ → ∑ 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_4} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasurableSingletonClass α] [inst : 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_4} : ∀ {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_4} : ∀ {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_4} : ∀ {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_4} : ∀ {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_4} : ∀ {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_4} : ∀ {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_4} : ∀ {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_4} : ∀ {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_4} : ∀ {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_4} : ∀ {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_4} : ∀ {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_4} : ∀ {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_4} : ∀ {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_4} : ∀ {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} {α : Type u_4} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.IsFiniteMeasure μ] {s : Finset ι} {t : ι → Set α}, (∀ i ∈ s, MeasurableSet (t i)) → (↑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_4} {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. TODO: use NullMeasurable sets like in the mathlib file.

theorem MeasureTheory.nonempty_inter_of_measureReal_lt_add {α : Type u_4} {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_4} {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_4} {β : Type u_5} : ∀ {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.ext_iff_measureReal_singleton {S : Type u_3} [Fintype S] [MeasurableSpace 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_4} {T : Type u_5} : ∀ {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}) = ∑ y : T, μ.real {(x_2, y)}

theorem measureReal_preimage_snd_singleton_eq_sum {S : Type u_4} {T : Type u_5} [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}) = ∑ x_2 : S, μ.real {(x_2, y)}