冪級數收斂半徑
冪級數在中心c周圍具有內部絕對收斂、外部發散的半徑R,邊界點須逐案判定。
mko-power-series-radius-of-convergence · definition · v0.10.0
數學敘述
對sum_{n≥0} a_n(x-c)^n,R可為0、有限正數或infinity。若|x-c|<R則絕對收斂;若|x-c|>R則發散;|x-c|=R時不能由R單獨判定。本輪geometric law固定a_n=q^n;endpoint law固定a_n=R^(-n)/(n+1)^p;prefix boundary的兩序列在0≤n≤N皆為0,之後分別為q_1^(n-N-1)與q_2^(n-N-1)。Ratio test只在相應極限存在時可用,不能當一般定義。有限coefficient prefix不足以決定一般radius,且不得以只支援bounded-real supremum的規則排除R=0或infinity。
代表公式(精確 TeX)
R(f,c)=r
成立條件
- 每個exact family明示對全部n有效的coefficient law:geometric q^n、endpoint R^(-n)/(n+1)^p、factorial extremes或zero-prefix後的geometric tails。
- radius與point位置以exact rational或0/infinity標記處理;endpoint另作獨立classification。
符號作用域
R— 收斂半徑f— 冪級數c— 展開中心r— 擴充非負半徑
直觀、定義與常見誤解
geometric family的完整law是a_n=q^n,故R=1/|q|。
endpoint family用a_n=R^(-n)/(n+1)^p展示兩端可有不同收斂型態。
R=0、R=infinity及兩條共享完整有限prefix但具有不同geometric tails的序列均為定義邊界。
把endpoints自動算入、把ratio limit不存在當R不存在,或由有限係數前綴唯一決定R。
已採用的推導導讀
半徑、端點與完整係數律原始 MKO 保留;導讀有自己的追加式修訂與驗證界線,不代表新 Lean 證明。
前置知識
驗證界線
本輪只對明示coefficient laws給exact證書;一般series仍需limsup或其他完整論證。
not_formalized
這不表示內容錯誤;只表示尚未登錄可重播的計算或形式證據。
下一個義務
加入實指數函數與解析普通生成函數。
同源結構化資料
本頁與互動版共用同一個物件與既有語言 edition;未新增證明或人工審定。
原始 MKO JSON · 純文字 Markdown