## Stream: maths

### Topic: FTC-2 on open set

#### James Arthur (Jan 09 2021 at 16:26):

Hi, I'm working on the area of the unit circle, part of Freek problem 9. I came stuck when I needed to do an integral from -1 to 1 and the derivatives of $\arcsin x$ and $\sqrt{1 - x^2}$ are not well defined at the limits of integration. So I needed a new flavour of FTC-2 where $f'$ is differentiable over $(a,\, b)$ instead of $[ a, b]$. I have a statement, but not a proof.

import measure_theory.interval_integral

open set interval_integral

variables {β E F : Type*} [measurable_space E] [normed_group E] {f : ℝ → E}
{c ca cb : E} {a b z : ℝ} {u v ua ub va vb : β → ℝ} {f' : ℝ → E} [normed_space ℝ E]
[borel_space E] [complete_space E] [topological_space.second_countable_topology E]

theorem FTC_but_with_open_set (hcont : continuous_on f (interval a b))
(hderiv : ∀ x ∈ Ioo (min a b) (max a b), has_deriv_at f (f' x) x)
(hcont' : continuous_on f' (interval a b)) (hmeas' : ae_measurable f') :
∫ y in a..b, f' y = f b - f a :=
begin
sorry
end


Is there a nice and easy way to do this. My current proof goes like this, take $(a,\, b)$, split at the midpoint into $(a, \frac{a+b}{2}]$ and $[\frac{a+b}{2}, b)$, then apply a flavour of integral_eq_sub_of_has_deriv_right, then I should be basically home dry.

#### Heather Macbeth (Jan 09 2021 at 17:06):

I don't know what the cleanest way is to get this fact. But I hope the hypothesis hcont can be weakened to continuous_within_at f (interval a b) a and continuous_within_at f (interval a b) b (the interior continuity should follow from the other hypotheses).

#### Heather Macbeth (Jan 10 2021 at 16:33):

I think one way to do this is to apply the dominated convergence theorem
docs#measure_theory.tendsto_integral_of_dominated_convergence
to approximate ∫ y in a..b, f' y as ∫ y in (A n)..b, f' y  where the sequence A n tends to a, and then apply the original FTC-2 on each of the intervals $[A_n, b)$.

Is there an easier way? @Yury G. Kudryashov @Patrick Massot

#### Yury G. Kudryashov (Jan 11 2021 at 03:39):

Do you need a better FTC-2 or a better has_deriv_within_at?

#### Heather Macbeth (Jan 11 2021 at 03:41):

I think the point is that, while it's true that $\tfrac{1}{2}\left(x\sqrt{1-x^2}+\arcsin(x)\right)$ has right derivative 0 at -1, it's not easy to prove with our current tools. Or is there a way I'm missing?

#### Yury G. Kudryashov (Jan 11 2021 at 03:47):

You can apply l'Hopital

#### Yury G. Kudryashov (Jan 11 2021 at 03:48):

with denominator $g(x)=x+1$

#### Yury G. Kudryashov (Jan 11 2021 at 03:48):

Or use some theorem from extend_deriv

#### Heather Macbeth (Jan 11 2021 at 03:53):

Ah, nice! @James Arthur :up:

#### Benjamin Davidson (Jan 11 2021 at 04:00):

That would certainly be easier than writing a version of FTC-2 for the open set, correct? I couldn't come up with any straightforward way to do the latter. Although if someone does have a good idea for how to prove FTC-2 for the open set I do think it would be a worthwhile addition regardless.

#### Heather Macbeth (Jan 11 2021 at 04:03):

I think the open set version can be deduced from the existing version of FTC-2 plus the theorem that Yury linked! docs#has_deriv_at_interval_left_endpoint_of_tendsto_deriv
And maybe that would be a useful addition (I'll defer to Yury).

#### Benjamin Davidson (Jan 11 2021 at 04:10):

Hmm...I'm a little confused as to how one would apply docs#has_deriv_at_interval_left_endpoint_of_tendsto_deriv here

#### James Arthur (Jan 11 2021 at 09:45):

That sounds brilliant, but is that the only solution? Is there a way to get this FTC-2, which seems a useful result?

#### Yury G. Kudryashov (Jan 11 2021 at 19:07):

You can do it for any function, so you can get FTC-2 (with has_deriv_at instead of has_deriv_within_at)

#### Yury G. Kudryashov (Jan 11 2021 at 19:08):

Just use has_deriv_at_interval_left_endpoint_of_tendsto_deriv to get the missing derivative at the left endpoint.

#### Benjamin Davidson (Jan 14 2021 at 04:55):

Solved! #5733

Last updated: May 18 2021 at 07:19 UTC