measurable derivative/integral

Stream: maths

[Yury G. Kudryashov]

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?

[Heather Macbeth]

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

[Yury G. Kudryashov]

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

[Sebastien Gouezel]

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

[Sebastien Gouezel]

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

[Sebastien Gouezel]

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

[Sebastien Gouezel]

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

[Sebastien Gouezel]

The other inclusion is a little bit harder. Take $x\in D$, we have to show that $f$ is differentiable at $x$. 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 $L$ and $L'$ satisfy $\|f(z) -f(y) - L(z-y)\| \leq \epsilon r$ (and the same for $L'$) for all $y,z \in B(x,r/2)$ for some $r>0$, then $\|L-L'\| \leq 4 \epsilon$ (take any $h$, and apply the previous inequalities to $y=x$ and $z= x + (r/2) (h/\|h\|)$).

[Sebastien Gouezel]

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

[Sebastien Gouezel]

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

[Sebastien Gouezel]

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 $B$ in the space of continuous linear maps from $E$ to $F$, the set of points $x$ where $f$ is differentiable with derivative in $B$ is measurable. This set can be described exactly as before, requiring additionally in the definition of $A$ that the candidate derivative $L$ belongs to $B$.

[Sebastien Gouezel]

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

[Yury G. Kudryashov]

Why do you need both $p$ and $q$ (or $r$ and $s$)?

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

But I can't get rid of the continuity assumption

[Yury G. Kudryashov]

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

[Sebastien Gouezel]

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.

[Sebastien Gouezel]

(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)

[Yury G. Kudryashov]

Branch measurable-fderiv has the proof

[Yury G. Kudryashov]

#4972

[Yury G. Kudryashov]

What should we do with 2 proofs?

[Yury G. Kudryashov]

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

[Sebastien Gouezel]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

Not sure which approach is simpler.

[Yury G. Kudryashov]

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

[Sebastien Gouezel]

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!

[Sebastien Gouezel]

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

[Yury G. Kudryashov]

I see that you have a better version of #4970

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Sebastien Gouezel]

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?

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Sebastien Gouezel]

Good night! I'll review while you sleep.

[Sebastien Gouezel]

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 :-)

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Sebastien Gouezel]

ok, let me do the refactoring.

[Sebastien Gouezel]

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