FTC-2

Stream: maths

[Yury G. Kudryashov]

Is there any short proof of FTC-2 for Lebesgue integral? I mean, the version that does not assume continuity of f'.

[Sebastien Gouezel]

Can you state more precisely the theorem you're thinking of?

[Jujian Zhang]

theorem ftc' (F f: ℝ -> ℝ) {hF : differentiable ℝ F}  {F_deriv : deriv F = f} {hf : measurable f} {hf1 : continuous f} (a b : ℝ) (h : b ≥ a) :
  (∫ x in a..b, f x) = F b - F a :=

[Jujian Zhang]

Is this ok?

[Yury G. Kudryashov]

Sebastien Gouezel said:

Can you state more precisely the theorem you're thinking of?

Ideally,

theorem FTC2 {F : ℝ → E} {a b : ℝ} (hFd : diferentiable F)
    (hfm : measurable (deriv f))
    (hfi : interval_integrable (deriv F) volume a b) :
  ∫ x in a..b, deriv F x = F b - F a :=
sorry

[Yury G. Kudryashov]

@Jujian Zhang Your version assumes continuity of the derivative. I'd like to avoid this.

[Yury G. Kudryashov]

I want something at least as strong as this

[Yury G. Kudryashov]

I'm reading (Rudin, 7.21) reference from WIki. It proves the theorem for F : ℝ → ℝ.

[Sebastien Gouezel]

The derivative is always measurable (when the target space is complete), as I explained in another thread, so the assumption hfm could be dropped. Otherwise, I agree that your statement is the right one. (Of course, with variations such as differentiability inside the open interval and continuity at the endpoints should be enough)

[Yury G. Kudryashov]

Is there a simple proof?

[Yury G. Kudryashov]

Rudin proves only a version for a real-valued function, and the proof essentially uses the order on ℝ.

[Sebastien Gouezel]

Once you have the theorem for real-valued functions, the general version follows by applying a linear form (coming from Hahn-Banach): if $F b -F a - \int F'$ were nonzero, there would be a linear form $\ell$ mapping it to something nonzero, i.e., $\ell \circ F$ would not satisfy the 1D-version, a contradiction.