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}
[MeasurableSingletonClass S]
(μ : MeasureTheory.Measure S)
:
∑ x ∈ s, μ {x} = μ ↑s
@[simp]
theorem
Finset.sum_toReal_measure_singleton
{S : Type u_4}
{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_4}
[Fintype S]
{x✝ : MeasurableSpace S}
[MeasurableSingletonClass S]
(μ : MeasureTheory.Measure S)
:
∑ x : S, μ {x} = μ Set.univ
theorem
sum_toReal_measure_singleton
{S : Type u_4}
[Fintype S]
{x✝ : MeasurableSpace S}
[MeasurableSingletonClass S]
(μ : MeasureTheory.Measure S)
[MeasureTheory.IsFiniteMeasure μ]
:
∑ x : S, (μ {x}).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)
:
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 α)
(s : Set α)
:
The real-valued version of a measure. Maps infinite measure sets to zero. Use as μ.real s.
Equations
- μ.real s = (μ s).toReal
Instances For
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 α}
(h : s ⊆ t)
(ht : μ t ≠ ⊤)
:
theorem
MeasureTheory.measure_diff_eq_top
{α : Type u_4}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s t : Set α}
(hs : μ s = ⊤)
(ht : μ t ≠ ⊤)
:
theorem
MeasureTheory.measure_symmDiff_eq_top
{α : Type u_4}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s t : Set α}
(hs : μ s ≠ ⊤)
(ht : μ t = ⊤)
:
theorem
MeasureTheory.measureReal_eq_zero_iff
{α : Type u_4}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
(h : μ s ≠ ⊤ := by finiteness)
:
@[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 α}
:
@[simp]
theorem
MeasureTheory.IsProbabilityMeasure.measureReal_univ
{α : Type u_4}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsProbabilityMeasure μ]
:
μ.real Set.univ = 1
theorem
MeasureTheory.measureReal_univ_pos
{α : Type u_4}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
[NeZero μ]
:
0 < μ.real Set.univ
theorem
MeasureTheory.measureReal_univ_ne_zero
{α : Type u_4}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
[NeZero μ]
:
μ.real Set.univ ≠ 0
theorem
MeasureTheory.nonempty_of_measureReal_ne_zero
{α : Type u_4}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
(h : μ.real s ≠ 0)
:
s.Nonempty
@[simp]
theorem
MeasureTheory.measureReal_smul_apply
{α : Type u_4}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
(c : ENNReal)
:
theorem
MeasureTheory.map_measureReal_apply
{α : Type u_4}
{β : Type u_5}
{x✝ : MeasurableSpace α}
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{f : α → β}
(hf : Measurable f)
{s : Set β}
(hs : 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 α}
(h : s₁ ⊆ s₂)
(h₂ : μ s₂ ≠ ⊤ := by finiteness)
:
μ.real s₁ ≤ μ.real s₂
theorem
MeasureTheory.measureReal_mono_null
{α : Type u_4}
{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_4}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s t : Set α}
(h : μ t ≠ ⊤ := by finiteness)
:
theorem
MeasureTheory.measureReal_le_measureReal_union_right
{α : Type u_4}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s t : Set α}
(h : μ s ≠ ⊤ := by finiteness)
:
theorem
MeasureTheory.measureReal_union_le
{α : Type u_4}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(s₁ s₂ : Set α)
:
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}
[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}
[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_4}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s₁ s₂ : Set α}
(h₁ : μ.real s₁ = 0)
(h₂ : μ.real s₂ = 0)
:
theorem
MeasureTheory.measureReal_congr
{α : Type u_4}
{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_4}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{t : Set α}
(s : Set α)
(ht : MeasureTheory.NullMeasurableSet t μ)
(h : μ s ≠ ⊤ := by finiteness)
:
theorem
MeasureTheory.measureReal_union_add_inter₀
{α : Type u_4}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{t : Set α}
(s : Set α)
(ht : MeasureTheory.NullMeasurableSet t μ)
(h₁ : μ s ≠ ⊤ := by finiteness)
(h₂ : μ t ≠ ⊤ := by finiteness)
:
theorem
MeasureTheory.measureReal_union_add_inter₀'
{α : Type u_4}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
(hs : MeasureTheory.NullMeasurableSet s μ)
(t : Set α)
(h₁ : μ s ≠ ⊤ := by finiteness)
(h₂ : μ t ≠ ⊤ := by finiteness)
:
theorem
MeasureTheory.measureReal_union₀
{α : Type u_4}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s t : Set α}
(ht : MeasureTheory.NullMeasurableSet t μ)
(hd : MeasureTheory.AEDisjoint μ s t)
(h₁ : μ s ≠ ⊤ := by finiteness)
(h₂ : μ t ≠ ⊤ := by finiteness)
:
theorem
MeasureTheory.measureReal_union₀'
{α : Type u_4}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s t : Set α}
(hs : MeasureTheory.NullMeasurableSet s μ)
(hd : MeasureTheory.AEDisjoint μ s t)
(h₁ : μ s ≠ ⊤ := by finiteness)
(h₂ : μ t ≠ ⊤ := by finiteness)
:
theorem
MeasureTheory.measureReal_add_measureReal_compl₀
{α : Type u_4}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{s : Set α}
(hs : MeasureTheory.NullMeasurableSet s μ)
:
theorem
MeasureTheory.measureReal_union
{α : Type u_4}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s₁ s₂ : Set α}
(hd : Disjoint s₁ s₂)
(h : MeasurableSet s₂)
(h₁ : μ s₁ ≠ ⊤ := by finiteness)
(h₂ : μ s₂ ≠ ⊤ := by finiteness)
:
theorem
MeasureTheory.measureReal_union'
{α : Type u_4}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s₁ s₂ : Set α}
(hd : Disjoint s₁ s₂)
(h : MeasurableSet s₁)
(h₁ : μ s₁ ≠ ⊤ := by finiteness)
(h₂ : μ s₂ ≠ ⊤ := by finiteness)
:
theorem
MeasureTheory.measureReal_inter_add_diff
{α : Type u_4}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{t : Set α}
(s : Set α)
(ht : MeasurableSet t)
(h : μ s ≠ ⊤ := by finiteness)
:
theorem
MeasureTheory.measureReal_diff_add_inter
{α : Type u_4}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{t : Set α}
(s : Set α)
(ht : MeasurableSet t)
(h : μ s ≠ ⊤ := by finiteness)
:
theorem
MeasureTheory.measureReal_union_add_inter
{α : Type u_4}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{t : Set α}
(s : Set α)
(ht : MeasurableSet t)
(h₁ : μ s ≠ ⊤ := by finiteness)
(h₂ : μ t ≠ ⊤ := by finiteness)
:
theorem
MeasureTheory.measureReal_union_add_inter'
{α : Type u_4}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
(hs : MeasurableSet s)
(t : Set α)
(h₁ : μ s ≠ ⊤ := by finiteness)
(h₂ : μ t ≠ ⊤ := by finiteness)
:
theorem
MeasureTheory.measureReal_symmDiff_eq
{α : Type u_4}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s t : Set α}
(hs : MeasureTheory.NullMeasurableSet s μ)
(ht : MeasureTheory.NullMeasurableSet t μ)
(h₁ : μ s ≠ ⊤ := by finiteness)
(h₂ : μ t ≠ ⊤ := by finiteness)
:
theorem
MeasureTheory.measureReal_symmDiff_le
{α : Type u_4}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(s t u : Set α)
(h₁ : μ s ≠ ⊤ := by finiteness)
(h₂ : μ t ≠ ⊤ := by finiteness)
:
theorem
MeasureTheory.measureReal_add_measureReal_compl
{α : Type u_4}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
[MeasureTheory.IsFiniteMeasure μ]
(h : MeasurableSet s)
:
theorem
MeasureTheory.measureReal_biUnion_finset₀
{ι : Type u_1}
{α : Type u_4}
{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_4}
{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_4}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_6}
(s : Finset β)
{f : α → β}
(hf : ∀ y ∈ s, MeasurableSet (f ⁻¹' {y}))
(h : ∀ a ∈ s, μ (f ⁻¹' {a}) ≠ ⊤ := by finiteness)
:
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 α}
[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_4}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s₁ s₂ : Set α}
(h : μ.real (s₁ ∩ s₂) = 0)
(h' : μ s₁ ≠ ⊤ := by finiteness)
:
theorem
MeasureTheory.measureReal_diff_null
{α : Type u_4}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s₁ s₂ : Set α}
(h : μ.real s₂ = 0)
(h' : μ s₂ ≠ ⊤ := by finiteness)
:
theorem
MeasureTheory.measureReal_add_diff
{α : Type u_4}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
(hs : MeasurableSet s)
(t : Set α)
(h₁ : μ s ≠ ⊤ := by finiteness)
(h₂ : μ t ≠ ⊤ := by finiteness)
:
theorem
MeasureTheory.measureReal_diff'
{α : Type u_4}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{t : Set α}
(s : Set α)
(hm : MeasurableSet t)
(h₁ : μ s ≠ ⊤ := by finiteness)
(h₂ : μ t ≠ ⊤ := by finiteness)
:
theorem
MeasureTheory.measureReal_diff
{α : Type u_4}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s₁ s₂ : Set α}
(h : s₂ ⊆ s₁)
(h₂ : MeasurableSet s₂)
(h₁ : μ s₁ ≠ ⊤ := by finiteness)
:
theorem
MeasureTheory.le_measureReal_diff
{α : Type u_4}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s₁ s₂ : Set α}
(h : μ s₂ ≠ ⊤ := by finiteness)
:
theorem
MeasureTheory.measureReal_diff_lt_of_lt_add
{α : Type u_4}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s t : Set α}
(hs : MeasurableSet s)
(hst : s ⊆ t)
(ε : ℝ)
(h : μ.real t < μ.real s + ε)
(ht' : μ t ≠ ⊤ := by finiteness)
:
theorem
MeasureTheory.measureReal_diff_le_iff_le_add
{α : Type u_4}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s t : Set α}
(hs : MeasurableSet s)
(hst : s ⊆ t)
(ε : ℝ)
(ht' : μ t ≠ ⊤ := by finiteness)
:
theorem
MeasureTheory.measureReal_eq_measureReal_of_null_diff
{α : Type u_4}
{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_4}
{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)
:
theorem
MeasureTheory.measureReal_eq_measureReal_smaller_of_between_null_diff
{α : Type u_4}
{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_4}
{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_4}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
[MeasureTheory.IsFiniteMeasure μ]
(h₁ : MeasurableSet s)
:
theorem
MeasureTheory.measureReal_union_congr_of_subset
{α : Type u_4}
{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)
:
theorem
MeasureTheory.sum_measureReal_le_measureReal_univ
{ι : Type u_1}
{α : Type u_4}
{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_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))
:
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 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_4}
{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_4}
{β : Type u_5}
{x✝ : MeasurableSpace α}
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SigmaFinite ν]
(s : Set α)
(t : Set β)
:
theorem
MeasureTheory.ext_iff_measureReal_singleton
{S : Type u_3}
[Fintype S]
[MeasurableSpace S]
{μ1 μ2 : MeasureTheory.Measure S}
[MeasureTheory.IsFiniteMeasure μ1]
[MeasureTheory.IsFiniteMeasure μ2]
:
Extension for the positivity tactic: applications of μ.real are nonnegative.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
measureReal_preimage_fst_singleton_eq_sum
{S : Type u_4}
{T : Type u_5}
{x✝ : MeasurableSpace S}
[MeasurableSingletonClass S]
[Fintype T]
{x✝¹ : MeasurableSpace T}
[MeasurableSingletonClass T]
(μ : MeasureTheory.Measure (S × T))
[MeasureTheory.IsFiniteMeasure μ]
(x : S)
:
theorem
measureReal_preimage_snd_singleton_eq_sum
{S : Type u_4}
{T : Type u_5}
[Fintype S]
{x✝ : MeasurableSpace S}
[MeasurableSingletonClass S]
{x✝¹ : MeasurableSpace T}
[MeasurableSingletonClass T]
(μ : MeasureTheory.Measure (S × T))
[MeasureTheory.IsFiniteMeasure μ]
(y : T)
: