English
Given finite s and t disjoint, and any u, the product-sum identity holds: uniformOn s u · uniformOn (s ∪ t) s + uniformOn t u · uniformOn (s ∪ t) t = uniformOn (s ∪ t) u.
Русский
Для конечных s и t, несовпадающих, выполняется тождество: uniformOn s u · uniformOn (s ∪ t) s + uniformOn t u · uniformOn (s ∪ t) t = uniformOn (s ∪ t) u.
LaTeX
$$$uniformOn\\; s\\; u \\cdot uniformOn\\; (s \\cup t)\\; s + uniformOn\\; t\\; u \\cdot uniformOn\\; (s \\cup t)\\; t = uniformOn\\; (s \\cup t)\\; u$$$
Lean4
theorem uniformOn_disjoint_union (hs : s.Finite) (ht : t.Finite) (hst : Disjoint s t) :
uniformOn s u * uniformOn (s ∪ t) s + uniformOn t u * uniformOn (s ∪ t) t = uniformOn (s ∪ t) u :=
by
rcases s.eq_empty_or_nonempty with (rfl | hs') <;> rcases t.eq_empty_or_nonempty with (rfl | ht')
· simp
· simp [uniformOn_self ht ht']
· simp [uniformOn_self hs hs']
rw [uniformOn, uniformOn, uniformOn, cond_apply hs.measurableSet, cond_apply ht.measurableSet,
cond_apply (hs.union ht).measurableSet, cond_apply (hs.union ht).measurableSet,
cond_apply (hs.union ht).measurableSet]
conv_lhs =>
rw [Set.union_inter_cancel_left, Set.union_inter_cancel_right, mul_comm (Measure.count (s ∪ t))⁻¹,
mul_comm (Measure.count (s ∪ t))⁻¹, ← mul_assoc, ← mul_assoc, mul_comm _ (Measure.count s),
mul_comm _ (Measure.count t), ← mul_assoc, ← mul_assoc]
rw [ENNReal.mul_inv_cancel, ENNReal.mul_inv_cancel, one_mul, one_mul, ← add_mul, ← measure_union,
Set.union_inter_distrib_right, mul_comm]
exacts [hst.mono inf_le_left inf_le_left, (ht.inter_of_left _).measurableSet, Measure.count_ne_zero ht',
(Measure.count_apply_lt_top.2 ht).ne, Measure.count_ne_zero hs', (Measure.count_apply_lt_top.2 hs).ne]
