# Zulip Chat Archive

## Stream: maths

### Topic: measurable derivative/integral

#### 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?

#### 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

#### Yury G. Kudryashov (Aug 06 2020 at 01:03):

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

#### 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 $E$ to the space of continuous linear maps from $E$ to $F$. Let me give a proof.

#### Sebastien Gouezel (Aug 06 2020 at 14:44):

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 (Aug 06 2020 at 14:45):

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 (Aug 06 2020 at 14:49):

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 (Aug 06 2020 at 14:54):

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 (Aug 06 2020 at 14:57):

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 (Aug 06 2020 at 15:00):

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 (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 $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 (Aug 06 2020 at 15:03):

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

#### Yury G. Kudryashov (Aug 09 2020 at 04:06):

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

#### Yury G. Kudryashov (Nov 10 2020 at 22:35):

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

#### Yury G. Kudryashov (Nov 10 2020 at 22:36):

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

#### Yury G. Kudryashov (Nov 10 2020 at 22:37):

But I can't get rid of the continuity assumption

#### Yury G. Kudryashov (Nov 10 2020 at 22:43):

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

#### 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.

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

#### Yury G. Kudryashov (Nov 11 2020 at 09:01):

Branch `measurable-fderiv`

has the proof

#### Yury G. Kudryashov (Nov 11 2020 at 09:02):

#### Yury G. Kudryashov (Nov 11 2020 at 09:04):

What should we do with 2 proofs?

#### 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.

#### 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!

#### 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.

#### Yury G. Kudryashov (Nov 11 2020 at 09:31):

Not sure which approach is simpler.

#### 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.

#### 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!

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

#### Yury G. Kudryashov (Nov 11 2020 at 09:42):

I see that you have a better version of #4970

#### 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.

#### 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`

.

#### 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?

#### Yury G. Kudryashov (Nov 11 2020 at 09:51):

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

#### 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.

#### Yury G. Kudryashov (Nov 11 2020 at 09:52):

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

.

#### 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`

)

#### Sebastien Gouezel (Nov 11 2020 at 09:57):

Good night! I'll review while you sleep.

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

#### 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.

#### 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.

#### Yury G. Kudryashov (Nov 11 2020 at 15:55):

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

#### 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.

#### Sebastien Gouezel (Nov 11 2020 at 16:08):

ok, let me do the refactoring.

#### 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