有限區間上的多項式定積分

數學敘述

對有限實區間a≤b上的連續多項式f，Riemann定積分是所有合法標記分割和在網格趨0時的共同極限；反向端點定義I(f,a,b)=−I(f,b,a)，a=b時為0。本輪明列受限矩公式 I(x^n,a,b)=(b^(n+1)−a^(n+1))/(n+1)，對f=Σc_k*x^k直接用I(f,a,b)=Σc_k(b^(k+1)−a^(k+1))/(k+1)。

代表公式（精確 TeX）

I(f,a,b)

成立條件

• 題庫端點及係數為安全整數；一般多項式至多3次，單項式c*x^n另限n=0至5，所有這些函數在全R連續並在有限區間可積。
• 定積分是有向、有號量，不必非負；反向區間要換號，不能一律取絕對值當幾何面積。
• 有限左端和只限a≤b、N=1至50，Δx=(b−a)/N，取i=0至N−1的左端點。零長度按0約定；有限和一般不等於積分。

符號作用域

• I — 本輪多項式有向定積分
• f — 指定連續多項式
• a — 有向起點
• b — 有向終點

直觀、定義與常見誤解

不是只讓某一種等分左端和收斂就能替任意函數定義Riemann積分；定義要求合法標記分割的共同極限。本輪只對已指定連續多項式使用明列矩公式。

常數c積分為c(b−a)，單項式與有限多項式使用本物件的精確矩公式。出題端可用同一受限primitive係數端點差作另一算法，主端直接累加矩；不把尚未物化的一般微積分基本定理當作已完成前置或新形式 Evidence。

仿射均勻左端和能直接精確算：Σ(mx_i+c)Δx，其中x_i=a+iΔx。產生端可用等差數列和，主端逐項有理累加。有限和即使在常數特例等於積分，也不升格成所有函數的積分證明。

有限左端和當成積分、反向端點不換號、積分一律當非負面積，或把多項式矩驗收稱為一般FTC完成。

已採用的推導導讀

原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。

前置知識

• 去心實數論域的函數極限 — 極限與有限和不可混同。
• 一元有理係數多項式 — 受限多項式與逐項矩計算。
• 多項式原函數與常數選擇 — 僅對本輪多項式矩核對primitive端點表示。
• 座標矩形與單位格的面積 — 保留有號積分與非負幾何面積之區別，不繼承一般面積proof。

驗證界線

本物件的受限多項式矩與有限和可精確重算；Riemann／intervalIntegral橋及一般微積分基本定理仍未附形式 Evidence。

not_formalized

這不表示內容錯誤；只表示尚未登錄可重播的計算或形式證據。

下一個義務

固定版intervalIntegral.integral_pow與有向端點橋接；Riemann／Lebesgue一致性及一般FTC仍為獨立未封閉義務。

同源結構化資料

本頁與互動版共用同一個物件與既有語言 edition；未新增證明或人工審定。