# 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 $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.

Last updated: May 19 2021 at 02:10 UTC