internlm/Lean-Github huggingface dataset:
Theorem: MeasureTheory.measureReal_diff_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₁ ∩ s₂) = 0
h' : autoParam (μ s₁ ≠ ⊤) _auto✝
⊢ μ.real (s₁ \ s₂) = μ.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 : Set α
h : μ.real (s₁ ∩ s₂) = 0
h' : autoParam (μ s₁ ≠ ⊤) _auto✝
⊢ (μ (s₁ \ s₂)).toReal = (μ s₁).toReal
Theorem: MeasureTheory.measureReal_diff_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₁ ∩ s₂) = 0
h' : autoParam (μ s₁ ≠ ⊤) _auto✝
⊢ (μ (s₁ \ s₂)).toReal = (μ s₁).toReal
Tactic:
rw [measure_diff_null']
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₁ ∩ s₂) = 0
h' : autoParam (μ s₁ ≠ ⊤) _auto✝
⊢ μ (s₁ ∩ s₂) = 0
Theorem: MeasureTheory.measureReal_diff_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₁ ∩ s₂) = 0
h' : autoParam (μ s₁ ≠ ⊤) _auto✝
⊢ μ (s₁ ∩ s₂) = 0
Tactic:
apply (measureReal_eq_zero_iff _).1 h
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₁ ∩ s₂) = 0
h' : autoParam (μ s₁ ≠ ⊤) _auto✝
⊢ μ (s₁ ∩ s₂) ≠ ⊤
Theorem: MeasureTheory.measureReal_diff_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₁ ∩ s₂) = 0
h' : autoParam (μ s₁ ≠ ⊤) _auto✝
⊢ μ (s₁ ∩ s₂) ≠ ⊤
Tactic:
exact measure_ne_top_of_subset inter_subset_left h'
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_diff_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' : autoParam (μ s₂ ≠ ⊤) _auto✝
⊢ μ.real (s₁ \ s₂) = μ.real s₁
Tactic:
rcases eq_top_or_lt_top (μ s₁) with H|H
Proof state after:
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h : μ.real s₂ = 0
h' : autoParam (μ s₂ ≠ ⊤) _auto✝
H : μ s₁ = ⊤
⊢ μ.real (s₁ \ s₂) = μ.real s₁

case inr
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h : μ.real s₂ = 0
h' : autoParam (μ s₂ ≠ ⊤) _auto✝
H : μ s₁ < ⊤
⊢ μ.real (s₁ \ s₂) = μ.real s₁
Theorem: MeasureTheory.measureReal_diff_null
Proof state before:
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h : μ.real s₂ = 0
h' : autoParam (μ s₂ ≠ ⊤) _auto✝
H : μ s₁ = ⊤
⊢ μ.real (s₁ \ s₂) = μ.real s₁
Tactic:
simp [measureReal_def, H, measure_diff_eq_top H h']
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_diff_null
Proof state before:
case inr
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h : μ.real s₂ = 0
h' : autoParam (μ s₂ ≠ ⊤) _auto✝
H : μ s₁ < ⊤
⊢ μ.real (s₁ \ s₂) = μ.real s₁
Tactic:
exact measureReal_diff_null' (measureReal_mono_null inter_subset_right h h') H.ne
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_add_diff
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
t : Set α
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
⊢ μ.real s + μ.real (t \ s) = μ.real (s ∪ t)
Tactic:
rw [← measureReal_union' (@disjoint_sdiff_right _ s t) hs h₁
  (measure_ne_top_of_subset diff_subset h₂), union_diff_self]
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_diff'
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t s : Set α
hm : MeasurableSet t
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
⊢ μ.real (s \ t) = μ.real (s ∪ t) - μ.real t
Tactic:
rw [union_comm, ← measureReal_add_diff hm s h₂ h₁]
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t s : Set α
hm : MeasurableSet t
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
⊢ μ.real (s \ t) = μ.real t + μ.real (s \ t) - μ.real t
Theorem: MeasureTheory.measureReal_diff'
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t s : Set α
hm : MeasurableSet t
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
⊢ μ.real (s \ t) = μ.real t + μ.real (s \ t) - μ.real t
Tactic:
ring
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_diff
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h : s₂ ⊆ s₁
h₂ : MeasurableSet s₂
h₁ : autoParam (μ s₁ ≠ ⊤) _auto✝
⊢ μ.real (s₁ \ s₂) = μ.real s₁ - μ.real s₂
Tactic:
rw [measureReal_diff' _ h₂ h₁ (measure_ne_top_of_subset h h₁), union_eq_self_of_subset_right h]
Proof state after:
no goals
Theorem: MeasureTheory.le_measureReal_diff
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✝
⊢ μ.real s₁ - μ.real s₂ ≤ μ.real (s₁ \ s₂)
Tactic:
simp only [tsub_le_iff_left]
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✝
⊢ μ.real s₁ ≤ μ.real s₂ + μ.real (s₁ \ s₂)
Theorem: MeasureTheory.le_measureReal_diff
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✝
⊢ μ.real s₁ ≤ μ.real s₂ + μ.real (s₁ \ s₂)
Tactic:
calc
  μ.real s₁ ≤ μ.real (s₂ ∪ s₁) := measureReal_le_measureReal_union_right h
  _ = μ.real (s₂ ∪ s₁ \ s₂) := congr_arg μ.real union_diff_self.symm
  _ ≤ μ.real s₂ + μ.real (s₁ \ s₂) := measureReal_union_le _ _
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_diff_lt_of_lt_add
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
hst : s ⊆ t
ε : ℝ
h : μ.real t < μ.real s + ε
ht' : autoParam (μ t ≠ ⊤) _auto✝
⊢ μ.real (t \ s) < ε
Tactic:
rw [measureReal_diff hst hs ht']
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
hst : s ⊆ t
ε : ℝ
h : μ.real t < μ.real s + ε
ht' : autoParam (μ t ≠ ⊤) _auto✝
⊢ μ.real t - μ.real s < ε
Theorem: MeasureTheory.measureReal_diff_lt_of_lt_add
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
hst : s ⊆ t
ε : ℝ
h : μ.real t < μ.real s + ε
ht' : autoParam (μ t ≠ ⊤) _auto✝
⊢ μ.real t - μ.real s < ε
Tactic:
linarith
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_diff_le_iff_le_add
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
hst : s ⊆ t
ε : ℝ
ht' : autoParam (μ t ≠ ⊤) _auto✝
⊢ μ.real (t \ s) ≤ ε ↔ μ.real t ≤ μ.real s + ε
Tactic:
rw [measureReal_diff hst hs ht', tsub_le_iff_left]
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_eq_measureReal_of_null_diff
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t✝ s t : Set α
hst : s ⊆ t
h_nulldiff : μ.real (t \ s) = 0
h : autoParam (μ (t \ s) ≠ ⊤) _auto✝
⊢ μ.real s = μ.real t
Tactic:
rw [measureReal_eq_zero_iff h] at h_nulldiff
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t✝ s t : Set α
hst : s ⊆ t
h_nulldiff : μ (t \ s) = 0
h : autoParam (μ (t \ s) ≠ ⊤) _auto✝
⊢ μ.real s = μ.real t
Theorem: MeasureTheory.measureReal_eq_measureReal_of_null_diff
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t✝ s t : Set α
hst : s ⊆ t
h_nulldiff : μ (t \ s) = 0
h : autoParam (μ (t \ s) ≠ ⊤) _auto✝
⊢ μ.real s = μ.real t
Tactic:
simp [measureReal_def, measure_eq_measure_of_null_diff hst h_nulldiff]
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_eq_measureReal_of_between_null_diff
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁✝ s₂✝ t s₁ s₂ s₃ : Set α
h12 : s₁ ⊆ s₂
h23 : s₂ ⊆ s₃
h_nulldiff : μ.real (s₃ \ s₁) = 0
h' : autoParam (μ (s₃ \ s₁) ≠ ⊤) _auto✝
⊢ μ.real s₁ = μ.real s₂ ∧ μ.real s₂ = μ.real s₃
Tactic:
have A : μ s₁ = μ s₂ ∧ μ s₂ = μ s₃ :=
  measure_eq_measure_of_between_null_diff h12 h23 ((measureReal_eq_zero_iff h').1 h_nulldiff)
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁✝ s₂✝ t s₁ s₂ s₃ : Set α
h12 : s₁ ⊆ s₂
h23 : s₂ ⊆ s₃
h_nulldiff : μ.real (s₃ \ s₁) = 0
h' : autoParam (μ (s₃ \ s₁) ≠ ⊤) _auto✝
A : μ s₁ = μ s₂ ∧ μ s₂ = μ s₃
⊢ μ.real s₁ = μ.real s₂ ∧ μ.real s₂ = μ.real s₃
Theorem: MeasureTheory.measureReal_eq_measureReal_of_between_null_diff
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁✝ s₂✝ t s₁ s₂ s₃ : Set α
h12 : s₁ ⊆ s₂
h23 : s₂ ⊆ s₃
h_nulldiff : μ.real (s₃ \ s₁) = 0
h' : autoParam (μ (s₃ \ s₁) ≠ ⊤) _auto✝
A : μ s₁ = μ s₂ ∧ μ s₂ = μ s₃
⊢ μ.real s₁ = μ.real s₂ ∧ μ.real s₂ = μ.real s₃
Tactic:
simp [measureReal_def, A.1, A.2]
Proof state after:
no goals
Theorem: MeasureTheory.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 μ
h₁ : MeasurableSet s
⊢ μ.real sᶜ = μ.real univ - μ.real s
Tactic:
rw [compl_eq_univ_diff]
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
inst✝ : IsFiniteMeasure μ
h₁ : MeasurableSet s
⊢ μ.real (univ \ s) = μ.real univ - μ.real s
Theorem: MeasureTheory.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 μ
h₁ : MeasurableSet s
⊢ μ.real (univ \ s) = μ.real univ - μ.real s
Tactic:
exact measureReal_diff (subset_univ s) h₁
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_union_congr_of_subset
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t t₁ t₂ : Set α
hs : s₁ ⊆ s₂
hsμ : μ.real s₂ ≤ μ.real s₁
ht : t₁ ⊆ t₂
htμ : μ.real t₂ ≤ μ.real t₁
h₁ : autoParam (μ s₂ ≠ ⊤) _auto✝
h₂ : autoParam (μ t₂ ≠ ⊤) _auto✝
⊢ μ.real (s₁ ∪ t₁) = μ.real (s₂ ∪ t₂)
Tactic:
simp [measureReal_def]
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t t₁ t₂ : Set α
hs : s₁ ⊆ s₂
hsμ : μ.real s₂ ≤ μ.real s₁
ht : t₁ ⊆ t₂
htμ : μ.real t₂ ≤ μ.real t₁
h₁ : autoParam (μ s₂ ≠ ⊤) _auto✝
h₂ : autoParam (μ t₂ ≠ ⊤) _auto✝
⊢ (μ (s₁ ∪ t₁)).toReal = (μ (s₂ ∪ t₂)).toReal
Theorem: MeasureTheory.measureReal_union_congr_of_subset
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t t₁ t₂ : Set α
hs : s₁ ⊆ s₂
hsμ : μ.real s₂ ≤ μ.real s₁
ht : t₁ ⊆ t₂
htμ : μ.real t₂ ≤ μ.real t₁
h₁ : autoParam (μ s₂ ≠ ⊤) _auto✝
h₂ : autoParam (μ t₂ ≠ ⊤) _auto✝
⊢ (μ (s₁ ∪ t₁)).toReal = (μ (s₂ ∪ t₂)).toReal
Tactic:
rw [measure_union_congr_of_subset hs _ ht]
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t t₁ t₂ : Set α
hs : s₁ ⊆ s₂
hsμ : μ.real s₂ ≤ μ.real s₁
ht : t₁ ⊆ t₂
htμ : μ.real t₂ ≤ μ.real t₁
h₁ : autoParam (μ s₂ ≠ ⊤) _auto✝
h₂ : autoParam (μ t₂ ≠ ⊤) _auto✝
⊢ μ t₂ ≤ μ t₁

ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t t₁ t₂ : Set α
hs : s₁ ⊆ s₂
hsμ : μ.real s₂ ≤ μ.real s₁
ht : t₁ ⊆ t₂
htμ : μ.real t₂ ≤ μ.real t₁
h₁ : autoParam (μ s₂ ≠ ⊤) _auto✝
h₂ : autoParam (μ t₂ ≠ ⊤) _auto✝
⊢ μ s₂ ≤ μ s₁
Theorem: MeasureTheory.measureReal_union_congr_of_subset
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t t₁ t₂ : Set α
hs : s₁ ⊆ s₂
hsμ : μ.real s₂ ≤ μ.real s₁
ht : t₁ ⊆ t₂
htμ : μ.real t₂ ≤ μ.real t₁
h₁ : autoParam (μ s₂ ≠ ⊤) _auto✝
h₂ : autoParam (μ t₂ ≠ ⊤) _auto✝
⊢ μ t₂ ≤ μ t₁
Tactic:
exact (ENNReal.toReal_le_toReal h₂ (measure_ne_top_of_subset ht h₂)).1 htμ
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_union_congr_of_subset
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t t₁ t₂ : Set α
hs : s₁ ⊆ s₂
hsμ : μ.real s₂ ≤ μ.real s₁
ht : t₁ ⊆ t₂
htμ : μ.real t₂ ≤ μ.real t₁
h₁ : autoParam (μ s₂ ≠ ⊤) _auto✝
h₂ : autoParam (μ t₂ ≠ ⊤) _auto✝
⊢ μ s₂ ≤ μ s₁
Tactic:
exact (ENNReal.toReal_le_toReal h₁ (measure_ne_top_of_subset hs h₁)).1 hsμ
Proof state after:
no goals
Theorem: MeasureTheory.sum_measureReal_le_measureReal_univ
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 : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : (↑s).PairwiseDisjoint t
⊢ ∑ i ∈ s, μ.real (t i) ≤ μ.real univ
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✝ : Set α
inst✝ : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : (↑s).PairwiseDisjoint t
⊢ ∑ x ∈ s, (μ (t x)).toReal ≤ (μ univ).toReal
Theorem: MeasureTheory.sum_measureReal_le_measureReal_univ
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 : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : (↑s).PairwiseDisjoint t
⊢ ∑ x ∈ s, (μ (t x)).toReal ≤ (μ univ).toReal
Tactic:
rw [← ENNReal.toReal_sum (fun i hi ↦ measure_ne_top _ _)]
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t✝ : Set α
inst✝ : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : (↑s).PairwiseDisjoint t
⊢ (∑ a ∈ s, μ (t a)).toReal ≤ (μ univ).toReal
Theorem: MeasureTheory.sum_measureReal_le_measureReal_univ
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 : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : (↑s).PairwiseDisjoint t
⊢ (∑ a ∈ s, μ (t a)).toReal ≤ (μ univ).toReal
Tactic:
apply ENNReal.toReal_mono (measure_ne_top _ _)
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t✝ : Set α
inst✝ : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : (↑s).PairwiseDisjoint t
⊢ ∑ a ∈ s, μ (t a) ≤ μ univ
Theorem: MeasureTheory.sum_measureReal_le_measureReal_univ
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 : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : (↑s).PairwiseDisjoint t
⊢ ∑ a ∈ s, μ (t a) ≤ μ univ
Tactic:
exact sum_measure_le_measure_univ h H
Proof state after:
no goals
Theorem: MeasureTheory.exists_nonempty_inter_of_measureReal_univ_lt_sum_measureReal
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ✝ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : μ.real univ < ∑ i ∈ s, μ.real (t i)
⊢ ∃ i ∈ s, ∃ j ∈ s, ∃ (_ : i ≠ j), (t i ∩ t j).Nonempty
Tactic:
apply exists_nonempty_inter_of_measure_univ_lt_sum_measure μ h
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ✝ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : μ.real univ < ∑ i ∈ s, μ.real (t i)
⊢ μ univ < ∑ i ∈ s, μ (t i)
Theorem: MeasureTheory.exists_nonempty_inter_of_measureReal_univ_lt_sum_measureReal
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ✝ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : μ.real univ < ∑ i ∈ s, μ.real (t i)
⊢ μ univ < ∑ i ∈ s, μ (t i)
Tactic:
apply (ENNReal.toReal_lt_toReal (measure_ne_top _ _) _).1
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ✝ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : μ.real univ < ∑ i ∈ s, μ.real (t i)
⊢ (μ univ).toReal < (∑ i ∈ s, μ (t i)).toReal

ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ✝ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : μ.real univ < ∑ i ∈ s, μ.real (t i)
⊢ ∑ i ∈ s, μ (t i) ≠ ⊤
Theorem: MeasureTheory.exists_nonempty_inter_of_measureReal_univ_lt_sum_measureReal
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ✝ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : μ.real univ < ∑ i ∈ s, μ.real (t i)
⊢ (μ univ).toReal < (∑ i ∈ s, μ (t i)).toReal
Tactic:
convert H
Proof state after:
case h.e'_4
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ✝ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : μ.real univ < ∑ i ∈ s, μ.real (t i)
⊢ (∑ i ∈ s, μ (t i)).toReal = ∑ i ∈ s, μ.real (t i)
Theorem: MeasureTheory.exists_nonempty_inter_of_measureReal_univ_lt_sum_measureReal
Proof state before:
case h.e'_4
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ✝ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : μ.real univ < ∑ i ∈ s, μ.real (t i)
⊢ (∑ i ∈ s, μ (t i)).toReal = ∑ i ∈ s, μ.real (t i)
Tactic:
rw [ENNReal.toReal_sum (fun i hi ↦ measure_ne_top _ _)]
Proof state after:
case h.e'_4
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ✝ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : μ.real univ < ∑ i ∈ s, μ.real (t i)
⊢ ∑ a ∈ s, (μ (t a)).toReal = ∑ i ∈ s, μ.real (t i)
Theorem: MeasureTheory.exists_nonempty_inter_of_measureReal_univ_lt_sum_measureReal
Proof state before:
case h.e'_4
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ✝ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : μ.real univ < ∑ i ∈ s, μ.real (t i)
⊢ ∑ a ∈ s, (μ (t a)).toReal = ∑ i ∈ s, μ.real (t i)
Tactic:
rfl
Proof state after:
no goals
Theorem: MeasureTheory.exists_nonempty_inter_of_measureReal_univ_lt_sum_measureReal
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ✝ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : μ.real univ < ∑ i ∈ s, μ.real (t i)
⊢ ∑ i ∈ s, μ (t i) ≠ ⊤
Tactic:
exact (ENNReal.sum_lt_top (fun i hi ↦ measure_ne_top _ _)).ne
Proof state after:
no goals
Theorem: MeasureTheory.nonempty_inter_of_measureReal_lt_add
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ✝ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
s t 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
Tactic:
apply nonempty_inter_of_measure_lt_add μ ht h's h't
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ✝ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
s t u : Set α
ht : MeasurableSet t
h's : s ⊆ u
h't : t ⊆ u
h : μ.real u < μ.real s + μ.real t
hu : autoParam (μ u ≠ ⊤) _auto✝
⊢ μ u < μ s + μ t
Theorem: MeasureTheory.nonempty_inter_of_measureReal_lt_add
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ✝ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
s t u : Set α
ht : MeasurableSet t
h's : s ⊆ u
h't : t ⊆ u
h : μ.real u < μ.real s + μ.real t
hu : autoParam (μ u ≠ ⊤) _auto✝
⊢ μ u < μ s + μ t
Tactic:
apply (ENNReal.toReal_lt_toReal hu _).1
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ✝ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
s t u : Set α
ht : MeasurableSet t
h's : s ⊆ u
h't : t ⊆ u
h : μ.real u < μ.real s + μ.real t
hu : autoParam (μ u ≠ ⊤) _auto✝
⊢ (μ u).toReal < (μ s + μ t).toReal

ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ✝ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
s t 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 ≠ ⊤
Theorem: MeasureTheory.nonempty_inter_of_measureReal_lt_add
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ✝ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
s t u : Set α
ht : MeasurableSet t
h's : s ⊆ u
h't : t ⊆ u
h : μ.real u < μ.real s + μ.real t
hu : autoParam (μ u ≠ ⊤) _auto✝
⊢ (μ u).toReal < (μ s + μ t).toReal
Tactic:
rw [ENNReal.toReal_add (measure_ne_top_of_subset h's hu) (measure_ne_top_of_subset h't hu)]
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ✝ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
s t u : Set α
ht : MeasurableSet t
h's : s ⊆ u
h't : t ⊆ u
h : μ.real u < μ.real s + μ.real t
hu : autoParam (μ u ≠ ⊤) _auto✝
⊢ (μ u).toReal < (μ s).toReal + (μ t).toReal
Theorem: MeasureTheory.nonempty_inter_of_measureReal_lt_add
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ✝ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
s t u : Set α
ht : MeasurableSet t
h's : s ⊆ u
h't : t ⊆ u
h : μ.real u < μ.real s + μ.real t
hu : autoParam (μ u ≠ ⊤) _auto✝
⊢ (μ u).toReal < (μ s).toReal + (μ t).toReal
Tactic:
exact h
Proof state after:
no goals