English
The uniform distribution on a finite set has the expected outer measure equal to the reciprocal of the cardinalities ratio.
Русский
Равномерное распределение по конечному множеству имеет внешнюю меру нормальной доли равной обратной доле кардинала множества.
LaTeX
$$$\text{toOuterMeasure_uniformOfFinset_apply}: (uniformOfFinset s hs).toOuterMeasure t = \#\{x \in s | x \in t\} / \#s$$$
Lean4
@[simp]
theorem toOuterMeasure_uniformOfFinset_apply : (uniformOfFinset s hs).toOuterMeasure t = #({x ∈ s | x ∈ t}) / #s :=
calc
(uniformOfFinset s hs).toOuterMeasure t = ∑' x, if x ∈ t then uniformOfFinset s hs x else 0 :=
toOuterMeasure_apply (uniformOfFinset s hs) t
_ = ∑' x, if x ∈ s ∧ x ∈ t then (#s : ℝ≥0∞)⁻¹ else 0 :=
(tsum_congr fun x => by simp_rw [uniformOfFinset_apply, ← ite_and, and_comm])
_ = ∑ x ∈ s with x ∈ t, if x ∈ s ∧ x ∈ t then (#s : ℝ≥0∞)⁻¹ else 0 :=
(tsum_eq_sum fun _ hx => if_neg fun h => hx (Finset.mem_filter.2 h))
_ = ∑ x ∈ s with x ∈ t, (#s : ℝ≥0∞)⁻¹ :=
(Finset.sum_congr rfl fun x hx =>
by
have this : x ∈ s ∧ x ∈ t := by simpa using hx
simp only [this, and_self_iff, if_true])
_ = #({x ∈ s | x ∈ t}) / #s := by simp only [div_eq_mul_inv, Finset.sum_const, nsmul_eq_mul]
