Zulip Chat Archive

Stream: maths

Topic: FTC-2


view this post on Zulip Yury G. Kudryashov (Aug 14 2020 at 16:22):

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

view this post on Zulip Sebastien Gouezel (Aug 14 2020 at 17:25):

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

view this post on Zulip Jujian Zhang (Aug 14 2020 at 18:58):

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 :=

view this post on Zulip Jujian Zhang (Aug 14 2020 at 18:58):

Is this ok?

view this post on Zulip Yury G. Kudryashov (Aug 14 2020 at 20:28):

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

view this post on Zulip Yury G. Kudryashov (Aug 14 2020 at 20:29):

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

view this post on Zulip Yury G. Kudryashov (Aug 14 2020 at 20:30):

I want something at least as strong as this

view this post on Zulip Yury G. Kudryashov (Aug 14 2020 at 20:36):

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

view this post on Zulip Sebastien Gouezel (Aug 14 2020 at 20:53):

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)

view this post on Zulip Yury G. Kudryashov (Aug 14 2020 at 21:27):

Is there a simple proof?

view this post on Zulip Yury G. Kudryashov (Aug 14 2020 at 21:28):

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

view this post on Zulip Sebastien Gouezel (Aug 15 2020 at 21:08):

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


Last updated: May 19 2021 at 02:10 UTC