Integrate analytic functions in the smooth hierarchy

Stream: PR reviews

[Sébastien Gouëzel]

I have a crazy refactor in the works. Currently, you can speak of C^n functions (for n : ℕ) or C^∞ (the exponent space is ℕ∞). I want to change to a model where the exponent space is WithTop ℕ∞, to be able to speak in the same language of C^n, C^∞ and C^ω functions.

Reason: when doing differential geometry (say, defining Lie brackets of vector fields, for instance to define the Lie algebra of a Lie group), a key point is that second derivatives are symmetric. Over reals or complexes, this is true for C^2 functions. Over a general normed field, this is only true for analytic functions. So, when doing differential geometry, Bourbaki says: fix some n which is anything if you're over the real or complex, and which is ω otherwise. Then the following holds...

In mathlib, if we want to avoid duplicating everything, I think the way to go is to implement the refactor, and have a typeclass [IsAllowedExponent 𝕜 n] in some theorems, which holds over any field for n = ω, and for any n over reals or complexes.

The refactor is hard: one needs to change a lot of import order and add a bunch of things on analytic functions within sets. From the mathematical point of view, things are also quite nasty when one wants to avoid completeness assumptions. But in the end it looks to me it has to be done if we want to get a satisfactory theory.

I'm not done yet, but here are the first PRs in the line.

TLDR: if you want Lie algebras in mathlib some day, done right, can you have a look at the following PRs?

#16720 splits ContDiff.Defs into two files. No new mathematical content, just splitting a big file into two smaller files.

#16725 changes the definition of AnalyticWithinAt to let it match a little more closely ContDiffWithinAt, and expands just a little bit the API to let the files compile.

#16383 introduces a new Prop-valued typeclass to discuss whether a given normed field is R or C.

[Johan Commelin]

:octopus: Wow! That sounds like a hard nut to crack. Will definitely review those PRs right now.

[Sébastien Gouëzel]

Thanks a lot for the lightning fast reviews! Next two PRs are

#16752, dropping completeness assumption in the proof that the composition of analytic functions on domains is analytic there -- it's now a different proof, as the other one couldn't be extended.

#16753, on analytic functions in Pi spaces.

[Johan Commelin]

Both look totally fine to me. But maybe someone who uses this part of the library a bit more than me should also take a look

[Yury G. Kudryashov]

I left 2 comments on #16753, going to bed now.

[Sébastien Gouëzel]

Thanks for the reviews!

The next PRs in the line are:

#16842, a short one (+40 lines) adding a few missing API lemmas to files low in the hierarchy

#16843, adding API to AnalyticWithinAt. Long (363), but essentially trivial

#16844, showing that a continuous linear map into continuous multilinear maps is analytic

[Johan Commelin]

[Jz Pan]

Sébastien Gouëzel said:

a key point is that second derivatives are symmetric

A stupid question: what about making this property as a typeclass?

[Sébastien Gouëzel]

A typeclass of what? It's not just the field, it also depends on the functions you are considering. And you want this property to be stable over a whole class of functions -- for instance, take the Lie bracket of two vector fields, you want the resulting Lie bracket to also have symmetric second derivatives. And also to not depend on a given fixed universe.

[Jz Pan]

Sorry, I don't know. (I haven't looked at your PR so probably what I say here is nonsense.) Maybe for functions. Just like saying a function has up to nth derivatives, you can also define a Prop says a function has symmetric second derivatives? Sorry I'm not familiar with the analytic part of API in mathlib.

[Sébastien Gouëzel]

An easy one in #16891 (splitting a file to keep a manageable size, no new material at all)

[Johan Commelin]

Easy =>

[Sébastien Gouëzel]

Another easy one in #16972, moving things around between files in the Analytic folder so that it makes more sense. No declaration added or removed, according to the declarations diff script.

[Yury G. Kudryashov]

:up: merged by @Jireh Loreaux

[Sébastien Gouëzel]

Next one in #16985 again expands the API around analytic functions. Again pretty short (+150/-36), with nothing complicated.

[Yury G. Kudryashov]

I've just noticed that

• the docstring of docs#AnalyticWithinOn mentions s and t, while only t is used in the definition;
• we don't have this *On/*WithinOn for Continuous and Differentiable

[Yury G. Kudryashov]

Do you plan to change the latter?

[Sébastien Gouëzel]

I've just fixed the docstring of AnalyticWithinOn, thanks! For the distinction AnalyticOn, AnalyticWithinOn, I think it's mostly a historical accident: analytic functions have a canonical extension to a neighborhood (contrary to continuous or differentiable functions, say), so it seemed at first natural to require that the function coincides around each point of s with this canonical extension, and this leads to AnalyticOn -- which is indeed quite different from ContinuousOn or DifferentiableOn as it does not only depend on the values of the function on the set. Then, we realized that this definition was no good to define analytic manifolds, and so we introduced AnalyticWithinOn, which is the true analogue of ContinuousOn or DifferentiableOn.

In retrospect, it looks to me that the really useful notion is AnalyticWithinOn, and I would be ready to rename it to AnalyticOn (for coherence with the naming of the other notions), and ditch the current AnalyticOn (or use a more complicated name, like AnalyticOnNhds). But there should be consensus for that, and I'm not going to do it in the near future anyway as I've already enough to do with the current ContDiff refactor :-)

[Sébastien Gouëzel]

#17002 unifies results on inversion that were proved separately in complete normed rings, and in normed fields, by introducing a typeclass HasSummableGeomSeries.

[Johan Commelin]

This all looks very sensible to me! Thanks!

[Sébastien Gouëzel]

Contrary to what I said two messages above, I decided it was a good idea to do now the renaming AnalyticOn -> AnalyticOnNhd and AnalyticWithinOn -> AnalyticOn, because the earlier it is done the less we have to deprecate. This is available in #17146 (a little bit long, but almost purely mechanical).

Of course, this is blocking all the other PRs I could make. The refactor is now building (you can have a look in #17152 for fun, but it's now more than +3000 lines so it will take quite some time to get it into mathlib through manageable PRs), so I will have a few PRs to make once #17146 is in.

[Johan Commelin]

The individual commits look great! Thanks

[Sébastien Gouëzel]

Here are the next few PRs towards the refactor (they are all referenced in the project PR #17152):

[Sébastien Gouëzel]

#16985 (+147/-32) expands a little bit the API around analytic functions

[Sébastien Gouëzel]

#17164 (+22) gives a few simple lemmas on WithTop (ENat)

[Sébastien Gouëzel]

#17169 (+683) is the first half of the Faa di Bruno formula. Too long, probably, but combinatorial and repetitive and it doesn't really make sense to split it

[Sébastien Gouëzel]

#17170 (+329/-137) shows that the inverse of an analytic partial homeo is analytic

[Johan Commelin]

Sébastien Gouëzel said:

#17169 (+683) is the first half of the Faa di Bruno formula. Too long, probably, but combinatorial and repetitive and it doesn't really make sense to split it

Do you already have a PR with the second half as well?

[Sébastien Gouëzel]

No because it depends on something that needs #16985. But you can have a look at how the full file will look like in #17152.

[Sébastien Gouëzel]

Thanks a lot for the quick reviews! Next two on the list are:

[Sébastien Gouëzel]

#17218 (+142/-42), moving the fact that the exponential is analytic earlier in the hierarchy

[Sébastien Gouëzel]

#17221 (+339/-18), showing that if a function is analytic on a set so is its derivative, without completeness assumptions

[Yury G. Kudryashov]

Asked for more docs on #17221

[Sébastien Gouëzel]

May I gently ping on #17221 and #17169? There is still quite a long way before the end of the refactor, and I'd rather get it sooner than later into mathlib because it will open the way to a lot of changes in differential geometry.

[Yury G. Kudryashov]

Sorry, I just forgot to delegate #17221

[Yury G. Kudryashov]

About #17169: could you please move OrderedFinpartitions to a file outside of Analysis?

[Yury G. Kudryashov]

Aren't OrderedFinpartions equivalent to docs#Finpartition s of Fin n? If yes (I may be wrong, it's past 1am here), then I think that we shouldn't create 2 separate APIs for the same object.

[Johan Commelin]

@Yaël Dillies do you have comments on these ordered finpartitions?

[Yaël Dillies]

I was literally writing something just now :laughing:

[Yaël Dillies]

I agree with Yury's diagnosis that this is mathematically the same as a Finpartition (univ : Set (Fin n)) or Finpartition (Iio n). What I'm not very clear about is how much the APIs overlap. Right now, they look mostly disjoint.

[Sébastien Gouëzel]

Yes, it's definitely the same thing as Finpartition, but with a pretty different implementation focus: what matters are the embeddings, and the interaction with Fin.cons, and defeqs of all this. I tried first with Finpartition, but it just wasn't suited for the task of the main induction of the proof of Faa di Bruno.

Let me copy part of the docstring of the file, to explain why it should remain in this file:

---

Note that the implementation of OrderedFinpartition is very specific to the Faa di Bruno formula:
as testified by the formula above, what matters is really the embedding of the parts in Fin n,
and moreover the parts have to be ordered by max I₀ < ... < max Iₖ₋₁ for the formula to hold
in the general case where the iterated differential might not be symmetric. The defeqs with respect
to Fin.cons are also important when doing the induction. For this reason, we do not expect this
class to be useful beyond the Faa di Bruno formula, which is why it is in this file instead
of a dedicated file in the Combinatorics folder.

---

If you want to see how it all fits together, I've just opened #17400 which contains the completed file.

[Sébastien Gouëzel]

Now that #17169 has been merged (thanks for the reviews!), the next one on the path to integrating analytic functions in the smooth hierarchy is #17400 (+306/-10), completing the proof of the Faa di Bruno formula.

[Sébastien Gouëzel]

The two next ones are:

[Sébastien Gouëzel]

#18722 (+37/-115), simplifying the proof that the composition of C^n functions are C^n using the Faa di Bruno formula.

[Sébastien Gouëzel]

#18723 (+210/-141) , a very weird PR because I make things more complicated in the definition of HasFTaylorSeriesUp, taking the smoothness parameter in WithTop ℕ∞instead of ℕ∞. This forces me to ask casts at several places, for absolutely no gain, so this PR is making mathlib worse. Of course, it will be used later to integrate analytic functions in the smooth hierarchy...

[Sébastien Gouëzel]

Last preparation PR: #19374 (+155/-80) splits a file, moving the content that depends on the ContDiff definition to other files (so that I can swap the import order later on).

[Sébastien Gouëzel]

The final PR is ready for review in #17152. Unfortunately, it's still kind of a patch bomb (+895/-630). The reason is that once you modify a basic definition (here ContDiff, so that ContDiff 𝕜 ω f means that f is analytic), you have to fix everything downstream, and this has to be done in one single PR. I've tried my best to split what could be split in other PRs, but now this one is essentially irreducible and still too big...

[Yury G. Kudryashov]

Thanks a lot!

[Yury G. Kudryashov]

BTW, what do you think should we do about $C^r$ for non-integer $r$?

[Sébastien Gouëzel]

For now, nothing :-)
More seriously, there are many notions of intermediate smoothness (C^m with Hölder m-th derivative, but also Sobolev smoothness, Besov smoothness, Gevrey smoothness, and so on). I would just build them as independent hierarchies, with theorems saying which implies which.

[Yury G. Kudryashov]

One more question:

consider a function which is C^2 over the reals or complexes, or analytic over a general field

Do these theorems hold for C^2 over a general field, if we use Whitney smoothness?

[Sébastien Gouëzel]

No idea. Isn't Whitney smoothness a finite-dimensional notion, or does it have a meaningful general extension?

Anyway, everyone doing p-adics says that any notion of finite differentiability is bad there, and that one should just use analytic functions (or strengthenings like rigid analytic).

[Yury G. Kudryashov]

I can review your PR tonight (in 10-13h from now).

[Sébastien Gouëzel]

That would be great, but there is no hurry!

[Yury G. Kudryashov]

Delegated. Sorry for a delay. I got distracted by proving d (dω) = 0.

[Sébastien Gouëzel]

Wow, very nice! I love it how everything is coordinate free. For instance, the exterior derivative is .uncurryFin (fderiv ℝ ω x)!

[Yury G. Kudryashov]

Note: @Sam Lindauer, a student of @Johan Commelin, is going to make formalization of de Rham cohomologies a part of his master's thesis, so I'm going to give him an opportunity to work on this project mostly alone, following my suggestions (I want some definitions to work in a proper generality). So, we aren't looking for outside contributions for now.

[Michael Rothgang]

de Rham cohomologies, this is great! :tada: :octopus: :dancers:

[Sébastien Gouëzel]

A side note for @Sam Lindauer then: on vector spaces, it will be important to define from the start the exterior derivative within a set, show that d o d = 0 for the exterior derivative within a set, and so on. The reason is that, even if you're just interested in the usual exterior derivative in a manifold, you need to work in domains in a chart because of manifolds with boundary.

A good API example for defining a notion in vector spaces, and then pulling it to manifolds using the fact that it is invariant under diffeos, is the Lie bracket of vector fields (where the vector space version is already in mathlib, and the manifold version will soon be -- you can see the overall result in #18396).

[Yury G. Kudryashov]

It's https://github.com/urkud/DeRhamCohomology/issues/5

[Michael Stoll]

I've tried to update Mathlib in a project of mine, where I have a line involving contDiff_succ_iff_deriv.mp <| hf.contDiff (n := 2), where hf : Differentiable ℂ f (and f : ℂ → ℂ), which now breaks with

application type mismatch
  contDiff_succ_iff_deriv.mp (Differentiable.contDiff hf)
argument
  Differentiable.contDiff hf
has type
  ContDiff ℂ 2 f : Prop
but is expected to have type
  ContDiff ?m.41648 (?m.41796 + 1) ?m.41797 : Prop

I assume this has to do with the type of n now being WithTop ℕ∞. What is the intended way to fix this? @Sébastien Gouëzel

[Michael Stoll]

Here is an attempt:

  have := hf.contDiff (n := 2)
  rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at this
  have hf' := (contDiff_succ_iff_deriv.mp <| this).2.differentiable rfl.le

but it runs into the next error

invalid field 'differentiable', the environment does not contain 'And.differentiable'
  (contDiff_succ_iff_deriv.mp this).right
has type
  (1 = ⊤ → AnalyticOn ℂ f Set.univ) ∧ ContDiff ℂ 1 (deriv f)

so I also need to replace .2 by .2.2...

Anyway this rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at this business is very ugly; the unification of 2 and 1 + 1 should be automatic.

[Kevin Buzzard]

They might not be defeq in this exotic type?

[Ruben Van de Velde]

If the proof with from rfl works...

[Sébastien Gouëzel]

Yes, it's definitely a byproduct of the refactor, and I am aware it's not optimal. I haven't found a good way around this either.

It's not clear to me if you're still stuck or if you have solved the issue -- if you're still stuck, I can have a look if you give me a pointer to the project.

[Sébastien Gouëzel]

Another way around, in the specific situation of your message above (but I don't know if it is oversimplified) would be:

  have := hf.contDiff (n := 1 + 1)
  have hf' := (contDiff_succ_iff_deriv.mp <| this).2.differentiable rfl.le

[Michael Stoll]

  have hf' := (contDiff_succ_iff_deriv.mp <| hf.contDiff (n := 1 + 1)).2.2.differentiable le_rfl

works, thanks.
I was wondering whether spelling 2 as 1 + 1 is really necessary. This seems to be a relevant downside of the refactor.
Since it apparently did work with ℕ∞, I'm wondering why it should not be possible to also get it to work with WithTop ℕ∞.

[Yury G. Kudryashov]

It used to use Nat, not ENat, so it worked.

[Yury G. Kudryashov]

So, it's a side effect of a natural generalization of the lemma (I've noticed Nat instead of ENat during review and suggested the edit), not of the refactor.

[Yury G. Kudryashov]

BTW, what are you trying to prove in this line? Possibly, we should add more convenience lemmas.

[Yury G. Kudryashov]

Sébastien Gouëzel said:

#18722 (+37/-115), simplifying the proof that the composition of C^n functions are C^n using the Faa di Bruno formula.

I used it to prove iteratedFDerivWithin_comp and iteratedFDeriv_comp in branch#YK-moreira
I'm going to move it to a separate PR later this week.

[Michael Stoll]

Yury G. Kudryashov said:

BTW, what are you trying to prove in this line? Possibly, we should add more convenience lemmas.

Basically this:

import Mathlib

example {f : ℂ → ℂ} (hf : Differentiable ℂ f) : Differentiable ℂ (deriv f) := sorry

I guess it would make sense to have this as a convenience lemma; it doesn't seem to exist:
@loogle ⊢ Differentiable _ (deriv ?f)

[loogle]

:shrug: nothing found

[Yury G. Kudryashov]

Should we add Differentiable.deriv and DifferentiableOn.deriv?

[Sébastien Gouëzel]

These lemmas should definitely be added, I think.

But a question now is if it's really a good idea to use Differentiable ℂ f as a normal form, or if ContDiff ℂ ω f (which is equivalent to it) would be better suited for the task.