区間積分

実数直線上の区間積分は ∫ x in a..b, f x と書きます． これは向きつきの区間積分で，a から b へ積分します．

#check intervalIntegral.integral_of_le
#check intervalIntegral.integral_hasStrictDerivAt_right

section IntervalIntegral

example : ∫ _ : ℝ in (0)..(1), (1 : ℝ) = 1 := by
  norm_num

example (f : ℝ → ℝ) (hf : Continuous f) (a b : ℝ) :
    deriv (fun u => ∫ x : ℝ in a..u, f x) b = f b := by
  exact (intervalIntegral.integral_hasStrictDerivAt_right
    (hf.intervalIntegrable _ _)
    (hf.stronglyMeasurableAtFilter _ _)
    hf.continuousAt).hasDerivAt.deriv

end IntervalIntegral

上の例は微分積分学の基本定理の一方向です． 積分を上端 u の関数と見たとき，その導関数が被積分関数 f になることを述べています．