English
For finite s, the relation holds: uniformOn s (t ∩ u) = uniformOn (s ∩ t) u · uniformOn s t.
Русский
Для конечного s выполняется: uniformOn s (t ∩ u) = uniformOn (s ∩ t) u · uniformOn s t.
LaTeX
$$$uniformOn\\; s\\; (t \\cap u) = uniformOn (s \\cap t)\\; u \\cdot uniformOn\\; s\\; t$$$
Lean4
theorem uniformOn_inter (hs : s.Finite) : uniformOn s (t ∩ u) = uniformOn (s ∩ t) u * uniformOn s t :=
by
by_cases hst : s ∩ t = ∅
·
rw [hst, uniformOn_empty_meas, Measure.coe_zero, Pi.zero_apply, zero_mul, uniformOn_eq_zero_iff hs, ←
Set.inter_assoc, hst, Set.empty_inter]
rw [uniformOn, uniformOn, cond_apply hs.measurableSet, cond_apply hs.measurableSet,
cond_apply (hs.inter_of_left _).measurableSet, mul_comm _ (Measure.count (s ∩ t)), ← mul_assoc,
mul_comm _ (Measure.count (s ∩ t)), ← mul_assoc, ENNReal.mul_inv_cancel, one_mul, mul_comm, Set.inter_assoc]
· rwa [← Measure.count_eq_zero_iff] at hst
· exact (Measure.count_apply_lt_top.2 <| hs.inter_of_left _).ne
