FTC-2 on open set

Stream: maths

[James Arthur]

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]

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]

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]

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

[Heather Macbeth]

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]

You can apply l'Hopital

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

Or use some theorem from extend_deriv

[Yury G. Kudryashov]

E.g., docs#has_deriv_at_interval_left_endpoint_of_tendsto_deriv

[Heather Macbeth]

Ah, nice! @James Arthur :up:

[Benjamin Davidson]

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]

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]

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]

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]

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]

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

[Benjamin Davidson]

Solved! #5733