Zulip Chat Archive

Stream: maths

Topic: FTC-2


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'.

Sebastien Gouezel (Aug 14 2020 at 17:25):

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

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

Jujian Zhang (Aug 14 2020 at 18:58):

Is this ok?

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

Yury G. Kudryashov (Aug 14 2020 at 20:29):

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

Yury G. Kudryashov (Aug 14 2020 at 20:30):

I want something at least as strong as this

Yury G. Kudryashov (Aug 14 2020 at 20:36):

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

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)

Yury G. Kudryashov (Aug 14 2020 at 21:27):

Is there a simple proof?

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 .

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: Dec 20 2023 at 11:08 UTC