[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
inst✝ : IsFiniteMeasure μ
hcs : ↑↑μ s ≠ 0
⊢ ↑↑(μ[|s]) Set.univ = 1
[PROOFSTEP]
rw [cond, Measure.smul_apply, Measure.restrict_apply MeasurableSet.univ, Set.univ_inter]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
inst✝ : IsFiniteMeasure μ
hcs : ↑↑μ s ≠ 0
⊢ (↑↑μ s)⁻¹ • ↑↑μ s = 1
[PROOFSTEP]
exact ENNReal.inv_mul_cancel hcs (measure_ne_top _ s)
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
⊢ μ[|∅] = 0
[PROOFSTEP]
simp [cond]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
inst✝ : IsProbabilityMeasure μ
⊢ μ[|Set.univ] = μ
[PROOFSTEP]
simp [cond, measure_univ, Measure.restrict_univ]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t✝ : Set Ω
hms : MeasurableSet s
t : Set Ω
⊢ ↑↑(μ[|s]) t = (↑↑μ s)⁻¹ * ↑↑μ (s ∩ t)
[PROOFSTEP]
rw [cond, Measure.smul_apply, Measure.restrict_apply' hms, Set.inter_comm, smul_eq_mul]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t✝ : Set Ω
hms : MeasurableSet s
t : Set Ω
⊢ ↑↑(μ[|s]) (s ∩ t) = ↑↑(μ[|s]) t
[PROOFSTEP]
rw [cond_apply _ hms, ← Set.inter_assoc, Set.inter_self, ← cond_apply _ hms]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
hms : MeasurableSet s
hcst : ↑↑(μ[|s]) t ≠ 0
⊢ 0 < ↑↑μ (s ∩ t)
[PROOFSTEP]
refine' pos_iff_ne_zero.mpr (right_ne_zero_of_mul _)
[GOAL]
case refine'_1
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
hms : MeasurableSet s
hcst : ↑↑(μ[|s]) t ≠ 0
⊢ ℝ≥0∞
[PROOFSTEP]
exact (μ s)⁻¹
[GOAL]
case refine'_2
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
hms : MeasurableSet s
hcst : ↑↑(μ[|s]) t ≠ 0
⊢ (↑↑μ s)⁻¹ * ↑↑μ (s ∩ t) ≠ 0
[PROOFSTEP]
convert hcst
[GOAL]
case h.e'_2
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
hms : MeasurableSet s
hcst : ↑↑(μ[|s]) t ≠ 0
⊢ (↑↑μ s)⁻¹ * ↑↑μ (s ∩ t) = ↑↑(μ[|s]) t
[PROOFSTEP]
simp [hms, Set.inter_comm, cond]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
inst✝ : IsFiniteMeasure μ
hms : MeasurableSet s
hci : ↑↑μ (s ∩ t) ≠ 0
⊢ 0 < ↑↑(μ[|s]) t
[PROOFSTEP]
rw [cond_apply _ hms]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
inst✝ : IsFiniteMeasure μ
hms : MeasurableSet s
hci : ↑↑μ (s ∩ t) ≠ 0
⊢ 0 < (↑↑μ s)⁻¹ * ↑↑μ (s ∩ t)
[PROOFSTEP]
refine' ENNReal.mul_pos _ hci
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
inst✝ : IsFiniteMeasure μ
hms : MeasurableSet s
hci : ↑↑μ (s ∩ t) ≠ 0
⊢ (↑↑μ s)⁻¹ ≠ 0
[PROOFSTEP]
exact ENNReal.inv_ne_zero.mpr (measure_ne_top _ _)
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
hms : MeasurableSet s
hmt : MeasurableSet t
hcs : ↑↑μ s ≠ ⊤
hci : ↑↑μ (s ∩ t) ≠ 0
⊢ μ[|s][|t] = μ[|s ∩ t]
[PROOFSTEP]
have hcs' : μ s ≠ 0 := (μ.toOuterMeasure.pos_of_subset_ne_zero (Set.inter_subset_left _ _) hci).ne'
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
hms : MeasurableSet s
hmt : MeasurableSet t
hcs : ↑↑μ s ≠ ⊤
hci : ↑↑μ (s ∩ t) ≠ 0
hcs' : ↑↑μ s ≠ 0
⊢ μ[|s][|t] = μ[|s ∩ t]
[PROOFSTEP]
ext u
[GOAL]
case h
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
hms : MeasurableSet s
hmt : MeasurableSet t
hcs : ↑↑μ s ≠ ⊤
hci : ↑↑μ (s ∩ t) ≠ 0
hcs' : ↑↑μ s ≠ 0
u : Set Ω
a✝ : MeasurableSet u
⊢ ↑↑(μ[|s][|t]) u = ↑↑(μ[|s ∩ t]) u
[PROOFSTEP]
simp [*, hms.inter hmt, cond_apply, ← mul_assoc, ← Set.inter_assoc, ENNReal.mul_inv, mul_comm, ← mul_assoc,
  ENNReal.mul_inv_cancel]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t✝ : Set Ω
hms : MeasurableSet s
hcs : ↑↑μ s ≠ 0
hcs' : ↑↑μ s ≠ ⊤
t : Set Ω
⊢ ↑↑(μ[|s]) t * ↑↑μ s = ↑↑μ (s ∩ t)
[PROOFSTEP]
rw [cond_apply μ hms t, mul_comm, ← mul_assoc, ENNReal.mul_inv_cancel hcs hcs', one_mul]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
inst✝ : IsFiniteMeasure μ
hms : MeasurableSet s
hcs : ↑↑μ s ≠ 0
hcs' : ↑↑μ sᶜ ≠ 0
⊢ ↑↑(μ[|s]) t * ↑↑μ s + ↑↑(μ[|sᶜ]) t * ↑↑μ sᶜ = ↑↑μ t
[PROOFSTEP]
rw [cond_mul_eq_inter μ hms hcs, cond_mul_eq_inter μ hms.compl hcs', Set.inter_comm _ t, Set.inter_comm _ t]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
inst✝ : IsFiniteMeasure μ
hms : MeasurableSet s
hcs : ↑↑μ s ≠ 0
hcs' : ↑↑μ sᶜ ≠ 0
⊢ ↑↑μ (t ∩ s) + ↑↑μ (t ∩ sᶜ) = ↑↑μ t
[PROOFSTEP]
exact measure_inter_add_diff t hms
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
inst✝ : IsFiniteMeasure μ
hms : MeasurableSet s
hmt : MeasurableSet t
⊢ ↑↑(μ[|s]) t = (↑↑μ s)⁻¹ * ↑↑(μ[|t]) s * ↑↑μ t
[PROOFSTEP]
by_cases ht : μ t = 0
[GOAL]
case pos
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
inst✝ : IsFiniteMeasure μ
hms : MeasurableSet s
hmt : MeasurableSet t
ht : ↑↑μ t = 0
⊢ ↑↑(μ[|s]) t = (↑↑μ s)⁻¹ * ↑↑(μ[|t]) s * ↑↑μ t
[PROOFSTEP]
simp [cond, ht, Measure.restrict_apply hmt, Or.inr (measure_inter_null_of_null_left s ht)]
[GOAL]
case neg
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
inst✝ : IsFiniteMeasure μ
hms : MeasurableSet s
hmt : MeasurableSet t
ht : ¬↑↑μ t = 0
⊢ ↑↑(μ[|s]) t = (↑↑μ s)⁻¹ * ↑↑(μ[|t]) s * ↑↑μ t
[PROOFSTEP]
rw [mul_assoc, cond_mul_eq_inter μ hmt ht s, Set.inter_comm, cond_apply _ hms]
