微積分基本定理：連續前提與有向端點

數學敘述

設 f:R→R 連續，a∈R，G(x)=∫_a^x f(t)dt 使用有向定積分，則 G 在R處處可微且 G'(x)=f(x)。若 F:R→R 可微並在R滿足 F'=f，則對任意實數端點a、b，∫_a^b f(t)dt=F(b)−F(a)。這裡採全R的充分前提，避免將單側端點導數或一般可積函數混入。

代表公式（精確 TeX）

D(G,x)

成立條件

• 被積函數在全R連續；題庫限定1至4個升冪安全整數係數的多項式，即至多3次。候選原函數限1至5個正分母有理係數。
• 有向積分允许反向及相同端點；G(a)=0不意味G'(a)=0。移動上下限是全R仿射式，導數為f(u(x))u'(x)−f(l(x))l'(x)。
• 候選F'=f逐係數核對，不以有限取樣宣稱相等。候選不成立不否定其他原函數存在；一般FTC未附形式Evidence。

符號作用域

• D — 在指定實點的導數
• G — 連續函數的有向積分累積函數
• x — 實數求導中心

直觀、定義與常見誤解

累積函數在起點取0，導數卻取f(a)；函數值與瞬時變化不能混同。上下限在某點重合，也不保證該點導數0，因二者速度可能不同。

第二部分先核對F'=f，再算端點差。加常數不改此差；端點反向改符號。題庫用精確多項式係數與有理數，未將有限代數核對升格為一般定理形式證明。

起點積分值0就導數0、上下限重合就导數0，或忽略原函數前提。

已採用的推導導讀

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

前置知識

• 實函數在一點的導數與差商 — 保留導數存在性及兩側極限。
• 有限區間上的多項式定積分 — 有向端點與連續可積切片。
• 實函數的點值與連續 — 全R連續是此處充分前提。
• 多項式原函數與常數選擇 — F'=f的合法原函數前提。
• 多項式的和、乘積與合成微分 — 移動仿射上下限的鏈式規則。

驗證界線

此為有明示充分前提的定理候選；有限多項式計算可重算，一般FTC及Riemann／Mathlib區間積分橋仍待形式證明。

not_formalized

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

下一個義務

固定Mathlib版綁定 intervalIntegral.integral_hasDerivAt_right 與 integral_eq_sub_of_hasDerivAt，補連續可積、Riemann一致性及端點方向的型別橋。

同源結構化資料

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