internlm/Lean-Github huggingface dataset:
Theorem: MeasureTheory.measureReal_biUnion_finset_le
Proof state before:
case insert
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t : Set α
f : β → Set α
x : β
s : Finset β
hx : x ∉ s
IH : μ.real (⋃ b ∈ s, f b) ≤ ∑ p ∈ s, μ.real (f p)
⊢ μ.real (⋃ b ∈ insert x s, f b) ≤ ∑ p ∈ insert x s, μ.real (f p)
Tactic:
simp only [hx, Finset.mem_insert, iUnion_iUnion_eq_or_left, not_false_eq_true,
  Finset.sum_insert]
Proof state after:
case insert
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t : Set α
f : β → Set α
x : β
s : Finset β
hx : x ∉ s
IH : μ.real (⋃ b ∈ s, f b) ≤ ∑ p ∈ s, μ.real (f p)
⊢ μ.real (f x ∪ ⋃ x ∈ s, f x) ≤ μ.real (f x) + ∑ p ∈ s, μ.real (f p)
Theorem: MeasureTheory.measureReal_biUnion_finset_le
Proof state before:
case insert
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t : Set α
f : β → Set α
x : β
s : Finset β
hx : x ∉ s
IH : μ.real (⋃ b ∈ s, f b) ≤ ∑ p ∈ s, μ.real (f p)
⊢ μ.real (f x ∪ ⋃ x ∈ s, f x) ≤ μ.real (f x) + ∑ p ∈ s, μ.real (f p)
Tactic:
exact (measureReal_union_le _ _).trans (by gcongr)
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_biUnion_finset_le
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t : Set α
f : β → Set α
x : β
s : Finset β
hx : x ∉ s
IH : μ.real (⋃ b ∈ s, f b) ≤ ∑ p ∈ s, μ.real (f p)
⊢ μ.real (f x) + μ.real (⋃ x ∈ s, f x) ≤ μ.real (f x) + ∑ p ∈ s, μ.real (f p)
Tactic:
gcongr
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_iUnion_fintype_le
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
inst✝ : Fintype β
f : β → Set α
⊢ μ.real (⋃ b, f b) ≤ ∑ p : β, μ.real (f p)
Tactic:
convert measureReal_biUnion_finset_le Finset.univ f
Proof state after:
case h.e'_3.h.e'_4.h.e'_3.h
ι : Type u_1
α : Type u_2
β : Type u_3
x✝¹ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
inst✝ : Fintype β
f : β → Set α
x✝ : β
⊢ f x✝ = ⋃ (_ : x✝ ∈ Finset.univ), f x✝
Theorem: MeasureTheory.measureReal_iUnion_fintype_le
Proof state before:
case h.e'_3.h.e'_4.h.e'_3.h
ι : Type u_1
α : Type u_2
β : Type u_3
x✝¹ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
inst✝ : Fintype β
f : β → Set α
x✝ : β
⊢ f x✝ = ⋃ (_ : x✝ ∈ Finset.univ), f x✝
Tactic:
simp
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_iUnion_fintype
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
inst✝ : Fintype β
f : β → Set α
hn : Pairwise (Disjoint on f)
h : ∀ (i : β), MeasurableSet (f i)
h' : autoParam (∀ (i : β), μ (f i) ≠ ⊤) _auto✝
⊢ μ.real (⋃ b, f b) = ∑ p : β, μ.real (f p)
Tactic:
rw [measureReal_def, measure_iUnion hn h, tsum_fintype, ENNReal.toReal_sum (fun i _hi ↦ h' i)]
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
inst✝ : Fintype β
f : β → Set α
hn : Pairwise (Disjoint on f)
h : ∀ (i : β), MeasurableSet (f i)
h' : autoParam (∀ (i : β), μ (f i) ≠ ⊤) _auto✝
⊢ ∑ a : β, (μ (f a)).toReal = ∑ p : β, μ.real (f p)
Theorem: MeasureTheory.measureReal_iUnion_fintype
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
inst✝ : Fintype β
f : β → Set α
hn : Pairwise (Disjoint on f)
h : ∀ (i : β), MeasurableSet (f i)
h' : autoParam (∀ (i : β), μ (f i) ≠ ⊤) _auto✝
⊢ ∑ a : β, (μ (f a)).toReal = ∑ p : β, μ.real (f p)
Tactic:
rfl
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_union_null
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h₁ : μ.real s₁ = 0
h₂ : μ.real s₂ = 0
⊢ μ.real (s₁ ∪ s₂) = 0
Tactic:
apply le_antisymm _ measureReal_nonneg
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h₁ : μ.real s₁ = 0
h₂ : μ.real s₂ = 0
⊢ μ.real (s₁ ∪ s₂) ≤ 0
Theorem: MeasureTheory.measureReal_union_null
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h₁ : μ.real s₁ = 0
h₂ : μ.real s₂ = 0
⊢ μ.real (s₁ ∪ s₂) ≤ 0
Tactic:
exact (measureReal_union_le s₁ s₂).trans (by simp [h₁, h₂])
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_union_null
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h₁ : μ.real s₁ = 0
h₂ : μ.real s₂ = 0
⊢ μ.real s₁ + μ.real s₂ ≤ 0
Tactic:
simp [h₁, h₂]
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_union_null_iff
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h₁ : autoParam (μ s₁ ≠ ⊤) _auto✝
h₂ : autoParam (μ s₂ ≠ ⊤) _auto✝
⊢ μ.real (s₁ ∪ s₂) = 0 ↔ μ.real s₁ = 0 ∧ μ.real s₂ = 0
Tactic:
have : μ (s₁ ∪ s₂) ≠ ∞ := measure_union_ne_top h₁ h₂
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h₁ : autoParam (μ s₁ ≠ ⊤) _auto✝
h₂ : autoParam (μ s₂ ≠ ⊤) _auto✝
this : μ (s₁ ∪ s₂) ≠ ⊤
⊢ μ.real (s₁ ∪ s₂) = 0 ↔ μ.real s₁ = 0 ∧ μ.real s₂ = 0
Theorem: MeasureTheory.measureReal_union_null_iff
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h₁ : autoParam (μ s₁ ≠ ⊤) _auto✝
h₂ : autoParam (μ s₂ ≠ ⊤) _auto✝
this : μ (s₁ ∪ s₂) ≠ ⊤
⊢ μ.real (s₁ ∪ s₂) = 0 ↔ μ.real s₁ = 0 ∧ μ.real s₂ = 0
Tactic:
refine ⟨fun h => ⟨?_, ?_⟩, fun h => measureReal_union_null h.1 h.2⟩
Proof state after:
case refine_1
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h₁ : autoParam (μ s₁ ≠ ⊤) _auto✝
h₂ : autoParam (μ s₂ ≠ ⊤) _auto✝
this : μ (s₁ ∪ s₂) ≠ ⊤
h : μ.real (s₁ ∪ s₂) = 0
⊢ μ.real s₁ = 0

case refine_2
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h₁ : autoParam (μ s₁ ≠ ⊤) _auto✝
h₂ : autoParam (μ s₂ ≠ ⊤) _auto✝
this : μ (s₁ ∪ s₂) ≠ ⊤
h : μ.real (s₁ ∪ s₂) = 0
⊢ μ.real s₂ = 0
Theorem: MeasureTheory.measureReal_union_null_iff
Proof state before:
case refine_1
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h₁ : autoParam (μ s₁ ≠ ⊤) _auto✝
h₂ : autoParam (μ s₂ ≠ ⊤) _auto✝
this : μ (s₁ ∪ s₂) ≠ ⊤
h : μ.real (s₁ ∪ s₂) = 0
⊢ μ.real s₁ = 0
Tactic:
exact measureReal_mono_null subset_union_left h this
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_union_null_iff
Proof state before:
case refine_2
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h₁ : autoParam (μ s₁ ≠ ⊤) _auto✝
h₂ : autoParam (μ s₂ ≠ ⊤) _auto✝
this : μ (s₁ ∪ s₂) ≠ ⊤
h : μ.real (s₁ ∪ s₂) = 0
⊢ μ.real s₂ = 0
Tactic:
exact measureReal_mono_null subset_union_right h this
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_congr
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
H : s =ᶠ[ae μ] t
⊢ μ.real s = μ.real t
Tactic:
simp [Measure.real, measure_congr H]
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_inter_add_diff₀
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t s : Set α
ht : NullMeasurableSet t μ
h : autoParam (μ s ≠ ⊤) _auto✝
⊢ μ.real (s ∩ t) + μ.real (s \ t) = μ.real s
Tactic:
simp only [measureReal_def]
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t s : Set α
ht : NullMeasurableSet t μ
h : autoParam (μ s ≠ ⊤) _auto✝
⊢ (μ (s ∩ t)).toReal + (μ (s \ t)).toReal = (μ s).toReal
Theorem: MeasureTheory.measureReal_inter_add_diff₀
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t s : Set α
ht : NullMeasurableSet t μ
h : autoParam (μ s ≠ ⊤) _auto✝
⊢ (μ (s ∩ t)).toReal + (μ (s \ t)).toReal = (μ s).toReal
Tactic:
rw [← ENNReal.toReal_add, measure_inter_add_diff₀ s ht]
Proof state after:
case ha
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t s : Set α
ht : NullMeasurableSet t μ
h : autoParam (μ s ≠ ⊤) _auto✝
⊢ μ (s ∩ t) ≠ ⊤

case hb
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t s : Set α
ht : NullMeasurableSet t μ
h : autoParam (μ s ≠ ⊤) _auto✝
⊢ μ (s \ t) ≠ ⊤
Theorem: MeasureTheory.measureReal_inter_add_diff₀
Proof state before:
case ha
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t s : Set α
ht : NullMeasurableSet t μ
h : autoParam (μ s ≠ ⊤) _auto✝
⊢ μ (s ∩ t) ≠ ⊤
Tactic:
exact measure_ne_top_of_subset inter_subset_left h
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_inter_add_diff₀
Proof state before:
case hb
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t s : Set α
ht : NullMeasurableSet t μ
h : autoParam (μ s ≠ ⊤) _auto✝
⊢ μ (s \ t) ≠ ⊤
Tactic:
exact measure_ne_top_of_subset diff_subset h
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_union_add_inter₀
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t s : Set α
ht : NullMeasurableSet t μ
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
⊢ μ.real (s ∪ t) + μ.real (s ∩ t) = μ.real s + μ.real t
Tactic:
have : μ (s ∪ t) ≠ ∞ :=
  ((measure_union_le _ _).trans_lt (ENNReal.add_lt_top.2 ⟨h₁.lt_top, h₂.lt_top⟩ )).ne
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t s : Set α
ht : NullMeasurableSet t μ
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
this : μ (s ∪ t) ≠ ⊤
⊢ μ.real (s ∪ t) + μ.real (s ∩ t) = μ.real s + μ.real t
Theorem: MeasureTheory.measureReal_union_add_inter₀
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t s : Set α
ht : NullMeasurableSet t μ
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
this : μ (s ∪ t) ≠ ⊤
⊢ μ.real (s ∪ t) + μ.real (s ∩ t) = μ.real s + μ.real t
Tactic:
rw [← measureReal_inter_add_diff₀ (s ∪ t) ht this, Set.union_inter_cancel_right, union_diff_right,
  ← measureReal_inter_add_diff₀ s ht h₁]
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t s : Set α
ht : NullMeasurableSet t μ
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
this : μ (s ∪ t) ≠ ⊤
⊢ μ.real t + μ.real (s \ t) + μ.real (s ∩ t) = μ.real (s ∩ t) + μ.real (s \ t) + μ.real t
Theorem: MeasureTheory.measureReal_union_add_inter₀
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t s : Set α
ht : NullMeasurableSet t μ
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
this : μ (s ∪ t) ≠ ⊤
⊢ μ.real t + μ.real (s \ t) + μ.real (s ∩ t) = μ.real (s ∩ t) + μ.real (s \ t) + μ.real t
Tactic:
ac_rfl
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_union_add_inter₀'
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t✝ : Set α
hs : NullMeasurableSet s μ
t : Set α
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
⊢ μ.real (s ∪ t) + μ.real (s ∩ t) = μ.real s + μ.real t
Tactic:
rw [union_comm, inter_comm, measureReal_union_add_inter₀ t hs h₂ h₁, add_comm]
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_union₀
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
ht : NullMeasurableSet t μ
hd : AEDisjoint μ s t
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
⊢ μ.real (s ∪ t) = μ.real s + μ.real t
Tactic:
simp only [Measure.real]
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
ht : NullMeasurableSet t μ
hd : AEDisjoint μ s t
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
⊢ (μ (s ∪ t)).toReal = (μ s).toReal + (μ t).toReal
Theorem: MeasureTheory.measureReal_union₀
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
ht : NullMeasurableSet t μ
hd : AEDisjoint μ s t
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
⊢ (μ (s ∪ t)).toReal = (μ s).toReal + (μ t).toReal
Tactic:
rw [measure_union₀ ht hd, ENNReal.toReal_add h₁ h₂]
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_union₀'
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
hs : NullMeasurableSet s μ
hd : AEDisjoint μ s t
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
⊢ μ.real (s ∪ t) = μ.real s + μ.real t
Tactic:
rw [union_comm, measureReal_union₀ hs (AEDisjoint.symm hd) h₂ h₁, add_comm]
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_add_measureReal_compl₀
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t : Set α
inst✝ : IsFiniteMeasure μ
s : Set α
hs : NullMeasurableSet s μ
⊢ μ.real s + μ.real sᶜ = μ.real univ
Tactic:
rw [← measureReal_union₀' hs aedisjoint_compl_right, union_compl_self]
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_inter_add_diff
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t s : Set α
ht : MeasurableSet t
h : autoParam (μ s ≠ ⊤) _auto✝
⊢ μ.real (s ∩ t) + μ.real (s \ t) = μ.real s
Tactic:
simp only [Measure.real]
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t s : Set α
ht : MeasurableSet t
h : autoParam (μ s ≠ ⊤) _auto✝
⊢ (μ (s ∩ t)).toReal + (μ (s \ t)).toReal = (μ s).toReal
Theorem: MeasureTheory.measureReal_inter_add_diff
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t s : Set α
ht : MeasurableSet t
h : autoParam (μ s ≠ ⊤) _auto✝
⊢ (μ (s ∩ t)).toReal + (μ (s \ t)).toReal = (μ s).toReal
Tactic:
rw [← ENNReal.toReal_add, measure_inter_add_diff _ ht]
Proof state after:
case ha
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t s : Set α
ht : MeasurableSet t
h : autoParam (μ s ≠ ⊤) _auto✝
⊢ μ (s ∩ t) ≠ ⊤

case hb
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t s : Set α
ht : MeasurableSet t
h : autoParam (μ s ≠ ⊤) _auto✝
⊢ μ (s \ t) ≠ ⊤
Theorem: MeasureTheory.measureReal_inter_add_diff
Proof state before:
case ha
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t s : Set α
ht : MeasurableSet t
h : autoParam (μ s ≠ ⊤) _auto✝
⊢ μ (s ∩ t) ≠ ⊤
Tactic:
exact measure_ne_top_of_subset inter_subset_left h
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_inter_add_diff
Proof state before:
case hb
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t s : Set α
ht : MeasurableSet t
h : autoParam (μ s ≠ ⊤) _auto✝
⊢ μ (s \ t) ≠ ⊤
Tactic:
exact measure_ne_top_of_subset diff_subset h
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_symmDiff_eq
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
⊢ μ.real (s ∆ t) = μ.real (s \ t) + μ.real (t \ s)
Tactic:
simp only [Measure.real]
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
⊢ (μ (s ∆ t)).toReal = (μ (s \ t)).toReal + (μ (t \ s)).toReal
Theorem: MeasureTheory.measureReal_symmDiff_eq
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
⊢ (μ (s ∆ t)).toReal = (μ (s \ t)).toReal + (μ (t \ s)).toReal
Tactic:
rw [← ENNReal.toReal_add, measure_symmDiff_eq hs ht]
Proof state after:
case ha
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
⊢ μ (s \ t) ≠ ⊤

case hb
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
⊢ μ (t \ s) ≠ ⊤
Theorem: MeasureTheory.measureReal_symmDiff_eq
Proof state before:
case ha
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
⊢ μ (s \ t) ≠ ⊤
Tactic:
exact measure_ne_top_of_subset diff_subset h₁
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_symmDiff_eq
Proof state before:
case hb
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
⊢ μ (t \ s) ≠ ⊤
Tactic:
exact measure_ne_top_of_subset diff_subset h₂
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_symmDiff_le
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t✝ s t u : Set α
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
⊢ μ.real (s ∆ u) ≤ μ.real (s ∆ t) + μ.real (t ∆ u)
Tactic:
rcases eq_top_or_lt_top (μ u) with hu|hu
Proof state after:
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t✝ s t u : Set α
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
hu : μ u = ⊤
⊢ μ.real (s ∆ u) ≤ μ.real (s ∆ t) + μ.real (t ∆ u)

case inr
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t✝ s t u : Set α
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
hu : μ u < ⊤
⊢ μ.real (s ∆ u) ≤ μ.real (s ∆ t) + μ.real (t ∆ u)
Theorem: MeasureTheory.measureReal_symmDiff_le
Proof state before:
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t✝ s t u : Set α
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
hu : μ u = ⊤
⊢ μ.real (s ∆ u) ≤ μ.real (s ∆ t) + μ.real (t ∆ u)
Tactic:
have : μ (s ∆ u) = ∞ := measure_symmDiff_eq_top h₁ hu
Proof state after:
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t✝ s t u : Set α
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
hu : μ u = ⊤
this : μ (s ∆ u) = ⊤
⊢ μ.real (s ∆ u) ≤ μ.real (s ∆ t) + μ.real (t ∆ u)
Theorem: MeasureTheory.measureReal_symmDiff_le
Proof state before:
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t✝ s t u : Set α
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
hu : μ u = ⊤
this : μ (s ∆ u) = ⊤
⊢ μ.real (s ∆ u) ≤ μ.real (s ∆ t) + μ.real (t ∆ u)
Tactic:
simp only [measureReal_def, this, ENNReal.top_toReal]
Proof state after:
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t✝ s t u : Set α
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
hu : μ u = ⊤
this : μ (s ∆ u) = ⊤
⊢ 0 ≤ (μ (s ∆ t)).toReal + (μ (t ∆ u)).toReal
Theorem: MeasureTheory.measureReal_symmDiff_le
Proof state before:
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t✝ s t u : Set α
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
hu : μ u = ⊤
this : μ (s ∆ u) = ⊤
⊢ 0 ≤ (μ (s ∆ t)).toReal + (μ (t ∆ u)).toReal
Tactic:
exact add_nonneg ENNReal.toReal_nonneg ENNReal.toReal_nonneg
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_symmDiff_le
Proof state before:
case inr
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t✝ s t u : Set α
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
hu : μ u < ⊤
⊢ μ.real (s ∆ u) ≤ μ.real (s ∆ t) + μ.real (t ∆ u)
Tactic:
apply le_trans _ (measureReal_union_le (s ∆ t) (t ∆ u))
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t✝ s t u : Set α
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
hu : μ u < ⊤
⊢ μ.real (s ∆ u) ≤ μ.real (s ∆ t ∪ t ∆ u)
Theorem: MeasureTheory.measureReal_symmDiff_le
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t✝ s t u : Set α
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
hu : μ u < ⊤
⊢ μ.real (s ∆ u) ≤ μ.real (s ∆ t ∪ t ∆ u)
Tactic:
apply measureReal_mono (symmDiff_triangle s t u) ?_
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t✝ s t u : Set α
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
hu : μ u < ⊤
⊢ μ (s ∆ t ⊔ t ∆ u) ≠ ⊤
Theorem: MeasureTheory.measureReal_symmDiff_le
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t✝ s t u : Set α
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
hu : μ u < ⊤
⊢ μ (s ∆ t ⊔ t ∆ u) ≠ ⊤
Tactic:
exact measure_union_ne_top (measure_symmDiff_ne_top h₁ h₂) (measure_symmDiff_ne_top h₂ hu.ne)
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_biUnion_finset₀
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t : Set α
s : Finset ι
f : ι → Set α
hd : (↑s).Pairwise (AEDisjoint μ on f)
hm : ∀ b ∈ s, NullMeasurableSet (f b) μ
h : autoParam (∀ b ∈ s, μ (f b) ≠ ⊤) _auto✝
⊢ μ.real (⋃ b ∈ s, f b) = ∑ p ∈ s, μ.real (f p)
Tactic:
simp only [measureReal_def, measure_biUnion_finset₀ hd hm, ENNReal.toReal_sum h]
Proof state after:
no goals
Theorem: MeasureTheory.sum_measureReal_preimage_singleton
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t : Set α
s : Finset β
f : α → β
hf : ∀ y ∈ s, MeasurableSet (f ⁻¹' {y})
h : autoParam (∀ a ∈ s, μ (f ⁻¹' {a}) ≠ ⊤) _auto✝
⊢ ∑ b ∈ s, μ.real (f ⁻¹' {b}) = μ.real (f ⁻¹' ↑s)
Tactic:
simp only [measureReal_def, ← sum_measure_preimage_singleton s hf, ENNReal.toReal_sum h]
Proof state after:
no goals