Zulip Chat Archive

Stream: maths

Topic: FTC-2 on open set


view this post on Zulip 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 arcsinx \arcsin x and 1x2 \sqrt{1 - x^2} are not well defined at the limits of integration. So I needed a new flavour of FTC-2 where ff' is differentiable over (a,b)(a,\, b) instead of [a,b][ 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) (a,\, b), split at the midpoint into (a,a+b2](a, \frac{a+b}{2}] and [a+b2,b)[\frac{a+b}{2}, b), then apply a flavour of integral_eq_sub_of_has_deriv_right, then I should be basically home dry.

view this post on Zulip 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).

view this post on Zulip 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 [An,b)[A_n, b).

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

view this post on Zulip Yury G. Kudryashov (Jan 11 2021 at 03:39):

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

view this post on Zulip Heather Macbeth (Jan 11 2021 at 03:41):

I think the point is that, while it's true that 12(x1x2+arcsin(x))\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?

view this post on Zulip Yury G. Kudryashov (Jan 11 2021 at 03:47):

You can apply l'Hopital

view this post on Zulip Yury G. Kudryashov (Jan 11 2021 at 03:48):

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

view this post on Zulip Yury G. Kudryashov (Jan 11 2021 at 03:48):

Or use some theorem from extend_deriv

view this post on Zulip Yury G. Kudryashov (Jan 11 2021 at 03:49):

E.g., docs#has_deriv_at_interval_left_endpoint_of_tendsto_deriv

view this post on Zulip Heather Macbeth (Jan 11 2021 at 03:53):

Ah, nice! @James Arthur :up:

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Benjamin Davidson (Jan 14 2021 at 04:55):

Solved! #5733


Last updated: May 18 2021 at 07:19 UTC