Zulip Chat Archive

Stream: maths

Topic: measurable derivative/integral


view this post on Zulip Yury G. Kudryashov (Aug 05 2020 at 23:00):

Is it true that fderiv of a measurable function f : E → F is a measurable function uncurry (fderiv f) : E × E → F? I can prove this for the directional derivative dir_deriv f a v = deriv (λ t, f (a + t * v)) 0, so the question is whether the set {x | differentiable_at f x} is measurable. It is for E = \R. What about other domains?

view this post on Zulip Heather Macbeth (Aug 05 2020 at 23:16):

Is this the same, or have I overlooked a hypothesis?
https://math.stackexchange.com/questions/905083/characterization-of-sets-of-differentiability

view this post on Zulip Yury G. Kudryashov (Aug 06 2020 at 01:03):

This answers "It is for E=RE = \mathbb R"

view this post on Zulip Sebastien Gouezel (Aug 06 2020 at 14:40):

It is true that the derivative of a function (measurable or not) is measurable when the target space is complete, as a map from EE to the space of continuous linear maps from EE to FF. Let me give a proof.

view this post on Zulip Sebastien Gouezel (Aug 06 2020 at 14:44):

Let me first show that the set of differentiability points is measurable. For r,s,ϵ>0r, s, \epsilon>0, let A(r,s,ϵ)A(r, s, \epsilon) denote the set of points xx for which there exist a continuous linear map LL (a "candidate derivative") and two numbers r(r/2,r)r' \in (r/2, r) and s(s/2,s)s'\in (s/2, s) such that, for all y,zB(x,r)y, z \in B(x,r'), one has f(z)f(y)L(zy)ϵr\|f(z) - f(y) - L(z-y)\| \leq \epsilon r, and for all y,zB(x,s)y, z \in B(x,s') one has f(z)f(y)L(zy)ϵs\|f(z)-f(y) - L (z-y)\| \leq \epsilon s.

view this post on Zulip Sebastien Gouezel (Aug 06 2020 at 14:45):

It is clear that A(r,s,ϵ)A(r,s,\epsilon) is open: indeed, if xx belongs to this set, then any nearby point also does, upon reducing a little bit rr' and ss' (and keeping the same LL). I claim that the set of differentiability points is equal to D=mnp,qnA(2p,2q,2m)D = \bigcap_m \bigcup_n \bigcap_{p, q\ge n} A(2^{-p}, 2^{-q}, 2^{-m}), from which the measurability follows readily.

view this post on Zulip Sebastien Gouezel (Aug 06 2020 at 14:49):

We have two inclusions to show. Let us start with the easy one: if xx is a point of differentiability, then it belongs to DD. Fix some ϵ=2m>0\epsilon = 2^{-m} > 0. Let LL be the derivative of ff at xx. For small enough rr, one has for all yB(x,r)y\in B(x, r) the inequality f(y)f(x)L(yx)(ϵ/2)yx(ϵ/2)r\|f(y) - f(x) - L(y-x)\| \leq (\epsilon/2) \|y-x\| \leq (\epsilon/2) r. Subtracting the corresponding inequality at zB(x,r)z \in B(x,r), one obtains f(z)f(y)L(zy)ϵr\|f(z)-f(y) - L(z-y)\| \leq \epsilon r. This shows that xA(ϵ,2p,2q)x \in A(\epsilon, 2^{-p},2^{-q}) whenever pp and qq are large enough, as requested.

view this post on Zulip Sebastien Gouezel (Aug 06 2020 at 14:54):

The other inclusion is a little bit harder. Take xDx\in D, we have to show that ff is differentiable at xx. In particular, we should exhibit in some way its derivative. The main remark is that the candidate derivative is essentially unique: if two continuous linear maps LL and LL' satisfy f(z)f(y)L(zy)ϵr\|f(z) -f(y) - L(z-y)\| \leq \epsilon r (and the same for LL') for all y,zB(x,r/2)y,z \in B(x,r/2) for some r>0r>0, then LL4ϵ\|L-L'\| \leq 4 \epsilon (take any hh, and apply the previous inequalities to y=xy=x and z=x+(r/2)(h/h)z= x + (r/2) (h/\|h\|)).

view this post on Zulip Sebastien Gouezel (Aug 06 2020 at 14:57):

Let ϵ=2m\epsilon=2^{-m}. The assumption that xx belongs to DD ensures that, for p,qp,q larger than some n=n(m)n=n(m), then xx belongs to A(2p,2q,ϵ)A(2^{-p}, 2^{-q}, \epsilon), yielding a candidate derivative L(p,q,ϵ)L(p, q, \epsilon). The almost uniqueness argument above shows that L(p,q,ϵ)L(p,q,\epsilon) is within 4ϵ4\epsilon of L(n,q,ϵ)L(n, q, \epsilon) (using the fact that both these candidate derivatives work in a ball of radius roughly 2q2^{-q}), which is itself withing 4ϵ4\epsilon of L(n,n,ϵ)L(n, n, \epsilon) (same argument using the ball of radius 2n2^{-n}).

view this post on Zulip Sebastien Gouezel (Aug 06 2020 at 15:00):

Let L(m)=L(n(m),n(m),2m)L(m) = L(n(m), n(m), 2^{-m}). The same argument shows that L(m)L(m) and L(m)L(m') are within distance 202m20 \cdot 2^{-m} of each other when mmm' \geq m, as they are both candidate derivatives on a common ball of very small radius. It follows that L(m)L(m) is a Cauchy sequence, converging to a continuous linear operator LL by completeness. It follows readily that LL is a derivative of ff at xx.

view this post on Zulip Sebastien Gouezel (Aug 06 2020 at 15:02):

This concludes the proof of the measurability of the set of differentiability points. The measurability of the differential is proved similarly. One should show that, for any closed set BB in the space of continuous linear maps from EE to FF, the set of points xx where ff is differentiable with derivative in BB is measurable. This set can be described exactly as before, requiring additionally in the definition of AA that the candidate derivative LL belongs to BB.

view this post on Zulip Sebastien Gouezel (Aug 06 2020 at 15:03):

(And no, I am not going to formalize this now :-)

view this post on Zulip Yury G. Kudryashov (Aug 09 2020 at 04:06):

Why do you need both pp and qq (or rr and ss)?

view this post on Zulip Yury G. Kudryashov (Nov 10 2020 at 22:35):

@Sebastien Gouezel It seems that your construction deals with strict differentiability, not Frechet differentiability.

view this post on Zulip Yury G. Kudryashov (Nov 10 2020 at 22:36):

I can modify it to prove that any continuous function has measurable derivative.

view this post on Zulip Yury G. Kudryashov (Nov 10 2020 at 22:37):

But I can't get rid of the continuity assumption

view this post on Zulip Yury G. Kudryashov (Nov 10 2020 at 22:43):

Now I can. I'll write down details once I come back home

view this post on Zulip Sebastien Gouezel (Nov 11 2020 at 08:48):

It's funny, I am precisely working on this now! I can confirm that it's for usual differentiability (strict differentiability is much easier). I'll PR something in a few hours, hopefully.

view this post on Zulip Sebastien Gouezel (Nov 11 2020 at 08:49):

(The proof of measurability of the differentiability set is already there in the branch deriv_measurable, I'm working on the measurability of the derivative)

view this post on Zulip Yury G. Kudryashov (Nov 11 2020 at 09:01):

Branch measurable-fderiv has the proof

view this post on Zulip Yury G. Kudryashov (Nov 11 2020 at 09:02):

#4972

view this post on Zulip Yury G. Kudryashov (Nov 11 2020 at 09:04):

What should we do with 2 proofs?

view this post on Zulip Yury G. Kudryashov (Nov 11 2020 at 09:07):

I'm sorry for not announcing my intent to formalize this before starting to write the code.

view this post on Zulip Sebastien Gouezel (Nov 11 2020 at 09:10):

It's funny! Let me finish my proof, and then I will learn a lot by reading yours!

view this post on Zulip Yury G. Kudryashov (Nov 11 2020 at 09:22):

The first difference is that I'm using ≤ ε * ||y - x|| and shells while you're using ≤ ε * r and balls.

view this post on Zulip Yury G. Kudryashov (Nov 11 2020 at 09:31):

Not sure which approach is simpler.

view this post on Zulip Yury G. Kudryashov (Nov 11 2020 at 09:32):

But this means that merging proofs is not an option; we'll have to choose one of them for mathlib.

view this post on Zulip Sebastien Gouezel (Nov 11 2020 at 09:40):

I think we'll go for your proof because it is already complete, and because you have been able to separate things more cleanly than I do (I have a monster proof of 170 lines, while you have been able to cut it in pieces). I'd like to eliminate the continuity requirement from your argument, though, because it doesn't show up in mine.

I have PR'ed mine at #4974 (not for merging). I'll salvage the supporting lemmas because they can be useful anyway!

view this post on Zulip Sebastien Gouezel (Nov 11 2020 at 09:42):

One thing I like better in mine, also, is the file-level docstring in which I give a high-level overview of the proof :)

view this post on Zulip Yury G. Kudryashov (Nov 11 2020 at 09:42):

I see that you have a better version of #4970

view this post on Zulip Yury G. Kudryashov (Nov 11 2020 at 09:43):

I don't think that we can avoid continuity argument in my proof without changing it from shells to balls.

view this post on Zulip Yury G. Kudryashov (Nov 11 2020 at 09:44):

Because the assumption about y ∈ B(x, R) \ B(x, r) says nothing about x' in nhds x.

view this post on Zulip Sebastien Gouezel (Nov 11 2020 at 09:48):

Yury G. Kudryashov said:

I see that you have a better version of #4970

Yes, you have a useless assumption. Can you remove it from #4970?

view this post on Zulip Yury G. Kudryashov (Nov 11 2020 at 09:51):

Probably I'm too sleepy. Which assumption is useless?

view this post on Zulip Yury G. Kudryashov (Nov 11 2020 at 09:51):

I saw that you have more additions to the same file but didn't pay attention to the list of assumptions.

view this post on Zulip Yury G. Kudryashov (Nov 11 2020 at 09:52):

Indeed, I'm too sleepy. We don't need 0 ≤ y.

view this post on Zulip Yury G. Kudryashov (Nov 11 2020 at 09:55):

I can remove it once I wake up (or you can PR your diff to algebra/archimedean)

view this post on Zulip Sebastien Gouezel (Nov 11 2020 at 09:57):

Good night! I'll review while you sleep.

view this post on Zulip Sebastien Gouezel (Nov 11 2020 at 13:39):

Comparing the two proofs, I think I like mine better because it gives a lower complexity in the Borel scale for the differentiability set (it shows that the differentiability set is a countable intersection of union of intersection of open sets, while yours give something like intersection of union of intersection of union of something which is measurable, but not open). But I like better the way you have presented the proof. I could refactor my proof based on some ideas in yours, to have the best of both worlds. What do you think?

(And apologies also for not telling you I was going to work on this. I was tired of doing boring stuff, so I took one day off to play with Lean :-)

view this post on Zulip Yury G. Kudryashov (Nov 11 2020 at 15:32):

You can do whatever you prefer. I just want the statements to be in mathlib soon.

view this post on Zulip Yury G. Kudryashov (Nov 11 2020 at 15:33):

I am formalizing Stokes' Theorem, and need measurable (fderiv k f) at one of the steps.

view this post on Zulip Yury G. Kudryashov (Nov 11 2020 at 15:55):

BTW, my proof can be easily modified to match complexity in the Borel scale.

view this post on Zulip Yury G. Kudryashov (Nov 11 2020 at 15:56):

You just replace continuous_at f x with the actual inequality we use later in the proof.

view this post on Zulip Sebastien Gouezel (Nov 11 2020 at 16:08):

ok, let me do the refactoring.

view this post on Zulip Sebastien Gouezel (Nov 11 2020 at 22:16):

#4974 is ready for review. I have copied some parts from #4972.


Last updated: May 19 2021 at 02:10 UTC