# 描述統計：保留重數計算平均數、中位數、全距與眾數集合

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-descriptive-statistics/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-descriptive-statistics-01 · production-20261019-adopted-96



## 目標與範圍

對觀測列 D=(4,10,1,3,8,1,6,3)，保留重複值，求觀測數 n、算術平均、中位數、全距與本輪約定的眾數集合；證明一般性質「最小值 ≤ 平均 ≤ 最大值」並用它核對；最後說明若先去重會得到不同（錯誤）的平均與中位數。

只處理非空有限的整數觀測列與 MKO 定義的四個摘要；完整證明平均數介於最小值與最大值之間。不處理樣本變異數、其他分位數或圖表，不從摘要推論母體、機率律或因果，也不否定其他教材「無眾數」的用語；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- numeric_evaluation
- finite_sum_rules
- frac_rules
- order_basics
- finite_counting_basics


- G1 — D=(4,10,1,3,8,1,6,3) 是原創合成的整數觀測列；它是列表，保留順序與重複值，不是去重集合（MKO 假設 a1、a2）。
- G2 — 眾數集合約定：所有出現次數達最大值的數，按遞增列出、每值一次（MKO 陳述與假設 a3）。
- G3 — 本題只作描述摘要，不假定 D 是某母體的獨立樣本（MKO 假設 a3）。


- D=(d_i)_{i=1}^{n} — 保留順序與重數的觀測列
- n — 觀測數
- \bar d — 算術平均
- s_{(k)} — 排序後第 k 個值
- f(v) — 值 v 在 D 中出現的次數
- m,\ M — 最小值與最大值





## 規則與來源


- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- finite_sum_rules · prerequisite — 有限和：Σ_{i=1}^{0} a_i=0、Σ_{i=1}^{n+1} a_i=Σ_{i=1}^{n} a_i + a_{n+1}；Σ(a_i+b_i)=Σa_i+Σb_i；Σ c·a_i=c·Σa_i。
- frac_rules · prerequisite — 分數運算（分母皆非零）：a/c+b/c=(a+b)/c；(a/b)(c/d)=(ac)/(bd)；(a/b)/(c/d)=(ad)/(bc)（另需 c≠0）；a/b=(ak)/(bk)（k≠0）。
- order_basics · prerequisite — 實數的序：任兩數恰有 u<v、u=v、u>v 之一；u<v 且 v<w 推出 u<w；u<v 推出 u+w<v+w；u<v 且 w>0 推出 uw<vw；u<v 且 w<0 推出 uw>vw。
- finite_counting_basics · prerequisite — 有限計數：互斥有限集合 A、B 有 |A∪B|=|A|+|B|；|A×B|=|A|·|B|；有限集之間存在雙射 ⇔ 元素個數相同。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- nat_induction · prerequisite — 數學歸納原理：對從 n₀ 起的命題族 P(n)，若 P(n₀) 成立，且對每個 n≥n₀ 都有 P(n)⇒P(n+1)，則所有 n≥n₀ 都有 P(n)。
- mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。
- divides_def · prerequisite — 整除：對整數 a、b，a∣b 表示存在整數 k 使 b=ak。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- mko_descstat_def · cited — 給非空有限實數觀測列 D，算術平均為 Σdi/n；排序後奇數 n 的中位數是中央值，偶數 n 是中間兩值的平均；全距為最大值減最小值。本輪眾數集合約定為所有出現頻率達最大值的數，按遞增列出；各數均只出現一次時，全部不同觀測值都是此約定的頻率最大者。 · mko-descriptive-statistics
- perm_invariance · prerequisite — 重新排列有限列表的項不改變其和，也不改變每個值的出現次數（有限和的一般交換律，可由 add_assoc、add_comm 歸納得到）。
- L_mean_bounds · lemma — 對非空有限實數列 (d_i)_{i=1}^{n}，若 m≤d_i≤M 對每個 i 成立，則 m≤(Σd_i)/n≤M。





## 逐步主鏈

S01 · definition操作前

D=(d_i)_{i=1}^{n},\ n>0

操作後

\bar d=\tfrac{1}{n}\sum_{i=1}^{n}d_i,\ \tilde d,\ R=\max D-\min D,\ \operatorname{Mo}(D)

條件：n>0

規則：mko_descstat_def · 依賴：G1, G2

葉節點依據：mko_descstat_def + def_unfold

寫出 MKO 的四個定義：平均是總和除以 n；中位數在排序後取（奇數 n 取中央值，偶數 n 取中間兩值的平均）；全距是最大值減最小值；眾數集合依 G2 的約定。所有計算都在保留重數的列表上做。



S02 · implies操作前

D=(4,10,1,3,8,1,6,3)

操作後

n=8>0

條件：無

規則：finite_counting_basics · 依賴：G1

葉節點依據：finite_counting_basics

逐項計數，D 有 8 個位置，重複的 1 與 3 各占兩個位置，所以 n=8，不是不同值的個數 6。n>0，平均與中位數有定義。



S03 · equivalent操作前

\sum_{i=1}^{8}d_i

操作後

4+10+1+3+8+1+6+3=36

條件：無

規則：finite_sum_rules · 依賴：G1, finite_sum_rules

葉節點依據：finite_sum_rules + numeric_evaluation

依有限和的遞迴規則逐項加入，部分和依次為 4、14、15、18、26、27、33、36。值 1 與值 3 各出現兩次，每筆觀測都加入一次。



S04 · equivalent操作前

\bar d=\tfrac{36}{8}

操作後

\bar d=\tfrac{9}{2}

條件：8\neq 0

規則：frac_rules · 依賴：S01, S02, S03

葉節點依據：frac_rules + numeric_evaluation

平均 = 36/8。分子分母同除以 gcd(36,8)=4（frac_rules，a/b=(ak)/(bk)，k≠0）得 9/2；gcd(9,2)=1，已是最簡分數（MKO 假設 a2）。核對：8·(9/2)=36，即各觀測與平均之差的總和為 36−8·(9/2)=0。



S05 · implies操作前

(4,10,1,3,8,1,6,3)

操作後

(s_{(k)})_{k=1}^{8}=(1,1,3,3,4,6,8,10)

條件：無

規則：perm_invariance · 依賴：G1, perm_invariance

葉節點依據：perm_invariance + finite_counting_basics

把 D 由小到大排列。核對它只改順序：在兩個列表中，1 與 3 各出現 2 次，4、6、8、10 各 1 次，總數 8；總和仍是 36。依 MKO 假設 a1，排序只改順序，不刪去重複值。



S06 · equivalent操作前

\tilde d,\ n=8\ \text{even}

操作後

\tilde d=\tfrac{s_{(4)}+s_{(5)}}{2}=\tfrac{3+4}{2}=\tfrac{7}{2}

條件：n\ \text{even}

規則：mko_descstat_def · 依賴：S01, S02, S05

葉節點依據：mko_descstat_def + frac_rules + numeric_evaluation

n=8 是偶數，中間兩個位置是 n/2=4 與 n/2+1=5。排序後 s_(4)=3、s_(5)=4，中位數是兩者的平均 (3+4)/2=7/2。它介於 3 與 4 之間，不是任何一筆觀測。



S07 · equivalent操作前

R=\max D-\min D

操作後

R=10-1=9

條件：無

規則：mko_descstat_def · 依賴：S01, S05

葉節點依據：mko_descstat_def + order_basics + numeric_evaluation

排序後最小值是第一項 1，最大值是最後一項 10；排序不改變觀測的集合，所以它們也是 D 的最小值與最大值。全距 10−1=9。



S08 · implies操作前

f(v)\ \text{for } v\in\{1,3,4,6,8,10\}

操作後

f(1)=2,\ f(3)=2,\ f(4)=f(6)=f(8)=f(10)=1

條件：無

規則：finite_counting_basics · 依賴：G1, S05, finite_counting_basics

葉節點依據：finite_counting_basics + numeric_evaluation

逐值計數出現次數。核對：2+2+1+1+1+1=8=n，每筆觀測恰好被算一次。計頻率時必須保留觀測重數（MKO 第二段）。



S09 · implies操作前

\max_v f(v)=2

操作後

\operatorname{Mo}(D)=\{1,3\}

條件：無

規則：mko_descstat_def · 依賴：S08, G2

葉節點依據：mko_descstat_def + order_basics

最大頻率是 2，達到它的值有 1 與 3。依 G2 的約定，兩者都屬於眾數集合，按遞增列出、每值一次：{1,3}。漏掉並列者是 MKO 列出的誤解。



S10 · theorem_application操作前

1\le d_i\le 10\ \text{for every } i

操作後

1\le \tfrac{9}{2}\le 10

條件：n=8>0

規則：L_mean_bounds · 依賴：S04, S07, L_mean_bounds

葉節點依據：L_mean_bounds + numeric_evaluation

每筆觀測都介於最小值 1 與最大值 10 之間，依引理 L_mean_bounds（m=1、M=10），平均 9/2 必須介於 1 與 10 之間；確實 1≤9/2≤10。這是對 S04 的合理性核對，不能取代 S03、S04 的計算。引理在 S10.1 到 S10.3 證明。



S11 · implies操作前

\bar d=\tfrac{9}{2},\ \tilde d=\tfrac{7}{2}

操作後

\bar d\notin D,\ \tilde d\notin D

條件：無

規則：numeric_evaluation · 依賴：S04, S06, G1

葉節點依據：numeric_evaluation + divides_def

9/2 是最簡分數且分母為 2（9 除以 2 餘 1），不是整數；D 的每筆觀測都是整數，所以平均不是任何一筆觀測。同理 7/2 不是整數，中位數也不是任何一筆觀測。MKO 第一段：平均不一定是某筆觀測，偶數個資料的中位數可能在中間兩值之間。



S12 · implies操作前

\{1,3,4,6,8,10\}\ \text{(deduplicated)}

操作後

\tfrac{32}{6}=\tfrac{16}{3}\neq\tfrac{9}{2},\quad \tfrac{4+6}{2}=5\neq\tfrac{7}{2}

條件：無

規則：mko_descstat_def · 依賴：S04, S06, G1

葉節點依據：mko_descstat_def + numeric_evaluation

若先把 D 去重成 {1,3,4,6,8,10}（6 個值），平均會是 (1+3+4+6+8+10)/6=32/6=16/3，中位數會是 (4+6)/2=5，兩者都和 S04、S06 不同。所以去重確實改變結果，違反 MKO 假設 a1；正確答案以保留重數的 D 為準。去重不改變非空有限觀測列的最小值與最大值，所以全距必定不變（本例為10−1=9）；但這不表示去重對平均、中位數與頻率等摘要無害。



S13 · implies操作前

\text{tasks of the goal}

操作後

n=8,\ \bar d=\tfrac{9}{2},\ \tilde d=\tfrac{7}{2},\ R=9,\ \operatorname{Mo}(D)=\{1,3\}

條件：無

規則：and_intro_elim · 依賴：S02, S04, S06, S07, S09, S10, G3

葉節點依據：and_intro_elim

合併：n=8，平均 9/2，中位數 7/2，全距 9，眾數集合 {1,3}；平均通過 1≤9/2≤10 的核對。依 G3，這些數只描述 D 本身，不推出母體平均、機率模型或因果結論。







## 局部子步與引理

S10.1 · implies操作前

m\le d_i\ \text{for every } i

操作後

nm=\sum_{i=1}^{n}m\le\sum_{i=1}^{n}d_i

條件：無

規則：finite_sum_rules · 依賴：finite_sum_rules, order_basics

葉節點依據：finite_sum_rules + order_basics + nat_induction

對項數 k 由 0 到 n 逐步加入：k=0 時兩邊都是 0。若 Σ_{i≤k} m ≤ Σ_{i≤k} d_i，又 m≤d_{k+1}，依 order_basics（兩邊各加一個數，再用傳遞：u≤v、w≤z ⇒ u+w≤v+w≤v+z）得 Σ_{i≤k+1} m ≤ Σ_{i≤k+1} d_i。依數學歸納到 k=n。左邊 n 個 m 相加等於 nm（finite_sum_rules，Σ c·1=c·n）。



S10.2 · implies操作前

nm\le\sum_{i=1}^{n}d_i,\ n>0

操作後

m\le\tfrac{1}{n}\sum_{i=1}^{n}d_i=\bar d

條件：n>0

規則：order_basics · 依賴：S10.1, order_basics, mul_inverse_nonzero

葉節點依據：order_basics + mul_inverse_nonzero + frac_rules

n>0，所以 1/n 存在且 1/n>0。依 order_basics，不等式兩邊同乘正數 1/n 方向不變：m=(nm)/n≤(Σd_i)/n=d̄。



S10.3 · implies操作前

d_i\le M\ \text{for every } i

操作後

\bar d\le M

條件：n>0

規則：order_basics · 依賴：S10.1, S10.2

葉節點依據：order_basics + finite_sum_rules + mul_inverse_nonzero

與 S10.1、S10.2 相同的論證，把不等式方向換成 d_i≤M：Σd_i≤nM，再同乘 1/n>0 得 d̄≤M。S10.1 到 S10.3 合起來證得引理 L_mean_bounds。







## 逐步反向審查


- S13 · sufficient_goal_reduction · S02, S04, S06, S07, S09, S10, S12 — 目標 G：題目要求的各摘要與核對。足夠條件 H：S02 到 S12 的結論；H⇒G 只用合取。H 由 G1 到 G3 正向推出，沒有把 G 當作前提。
- S12 · premise_audit · S04, S06, numeric_evaluation — 反例只需要一組具體數字（N12 到 N14）；它說明去重一般不保持平均與中位數。
- S11 · premise_audit · S04, S06, divides_def — 只宣稱這兩個摘要不在 D 中；不宣稱平均或中位數一般不能是觀測值。
- S10.3 · premise_audit · S10.1, S10.2, order_basics — 同樣需要逐項上界與 n>0。
- S10.2 · premise_audit · S10.1, order_basics, mul_inverse_nonzero — 必須 n>0：乘負數會反向，n=0 時平均無定義。
- S10.1 · premise_audit · finite_sum_rules, order_basics, nat_induction — 需要每一項都滿足 m≤d_i；只要有一項小於 m，結論可能失敗。不宣稱反向。
- S10 · premise_audit · L_mean_bounds, S07 — 引理需要 n>0 與逐項的上下界；不宣稱反向，即落在 [1,10] 的數不一定是平均。
- S09 · premise_audit · S08, G2, mko_descstat_def — 需要完整的頻率表；只看第一個達到最大頻率的值會漏掉 3。
- S08 · premise_audit · finite_counting_basics, S02 — 頻率總和等於 n 是必要核對（N8）；不宣稱頻率表能還原原本的順序。
- S07 · inverse_equivalence · mko_descstat_def, numeric_evaluation — 精確計算（N7），雙向成立。
- S06 · inverse_equivalence · mko_descstat_def, numeric_evaluation — 依定義展開後是精確計算（N6），雙向成立；位置必須取自排序後的列表。
- S05 · premise_audit · perm_invariance, finite_counting_basics — 需要的是每個值的出現次數相同（N5、N8）；排序後的列表一般不等於原列表，所以只宣稱「同一組觀測」，不宣稱兩列表相等。
- S04 · inverse_equivalence · frac_rules, numeric_evaluation — 反向：分子分母同乘 4 回到 36/8；需要 8≠0 與 4≠0。
- S03 · inverse_equivalence · finite_sum_rules, numeric_evaluation — 精確整數計算（N1），可獨立重算，雙向成立。
- S02 · premise_audit · G1, finite_counting_basics — 計的是列表位置，不是不同值；這正是 MKO 假設 a1 的要求。
- S01 · premise_audit · G1, G2, mko_descstat_def — 此步只寫出定義，不推出新事實；n>0 是平均有定義的前提。





## 錯誤控制與反例

不要先去重MKO 的誤解之一是先去重再算。去重後平均變成 16/3、中位數變成 5（S12），都不是 D 的摘要。重複值是資料的一部分：兩個 1 表示有兩筆觀測等於 1。

並列的最大頻率都要列入1 與 3 都出現 2 次，眾數集合是 {1,3}，不是 {1}。若所有值都只出現一次，依本輪約定全部不同值都在眾數集合中；其他教材可能稱為「無眾數」，這是用語慣例不同，不是矛盾（MKO 假設 a3）。

中位數要在排序後取未排序的 D 第 4、5 項是 3 與 8，平均 11/2，這不是中位數。必須先排序得 (1,1,3,3,4,6,8,10)，再取第 4、5 項 3 與 4，得 7/2（S06）。


- 中位數是 D 的第 4、5 項的平均 (3+8)/2=11/2 → reject — 中位數要在排序後取；排序後第 4、5 項是 3 與 4，中位數 7/2。
- 平均是 (1+3+4+6+8+10)/6=16/3 → reject — 這是去重後的平均；保留重數得 36/8=9/2。
- 眾數集合是 {1} → reject — 3 也出現 2 次，達到最大頻率；眾數集合是 {1,3}。
- D 的平均是 9/2，所以產生 D 的母體平均也是 9/2 → reject — 描述摘要只描述 D，本題沒有母體或抽樣模型（MKO 假設 a3）。





## 結論與限制

對 D=(4,10,1,3,8,1,6,3)：n=8，平均 36/8=9/2，排序後中位數 (3+4)/2=7/2，全距 10−1=9，眾數集合 {1,3}；且 1≤9/2≤10。若先去重會誤得平均 16/3、中位數 5。這些摘要只描述 D，不構成任何母體推論。


- perm_invariance（有限和的一般交換律與排序保留頻率）作為前提使用，未在本稿證明。
- 樣本變異數、其他分位數、圖表與機率矩不在本稿範圍；描述摘要與機率期望的型別區別保留給後續切片。
- MKO 的 formal next（有限列表求和、排序中位與頻數最大集合的橋接）未做。





## 驗證及來源綁定

17 個本稿宣告算術檢查；只支持所列算式。


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: de10c74e217f968eb9b391752651fd9f7f2626b798bfb8e87c9af6eadff7e2e3
- original source SHA-256: de10c74e217f968eb9b391752651fd9f7f2626b798bfb8e87c9af6eadff7e2e3
- Lean: NOT_RUN · independent AI: NOT_MEASURED

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-descriptive-statistics-01.json)