Are continuous multilinear maps analytic in mathlib ?

Stream: Is there code for X?

[Sophie Morel]

I was looking at the mathlib files on analytic functions, and at the beginning of that one, I saw the following text:

"In this file we prove that a ContinuousLinearMap defines an analytic function with the formal power series f x = f a + f (x - a). We also prove similar results for multilinear maps."

However, I didn't find a proof that continuous multilinear maps are analytic in that file or its dependencies.

So my question is: does mathlib contain the proof that continuous multilinear maps are analytic ? I ask because I wrote a proof when trying to simplify my proof that continuous multilinear maps are differentiable, and I'm wondering whether to PR it or whether it's useless.

[Junyan Xu]

Apparently there is docs#ContinuousLinearMap.analyticAt_bilinear but not trilinear or higher up.

[Sophie Morel]

Okay ! By the way, we were talking about writing some lemmas for functions that have finite power series. I have a bit more time now, so I'll get to it until you've already started doing something.

[Junyan Xu]

Nope, haven't had time to look deeply into the new stuff on your PR yet ...

[Sophie Morel]

That can wait, no worries ! It's just stuff to prepare for the proof that multilinear maps are analytic. (By the way, I messed up pretty badly yesterday and the branch had to be reset to a previous commit. I hope we didn't delete anybody else's corrections while doing that, I'm really sorry if we did.)

I was already talking about stuff that will be needed to deduce that they are also differentiable without a completeness assumption on the target space.

[Sophie Morel]

Okay, I did "continuously polynomial" functions (= functions that can be written as the sum of a finite formal multilinear series) and proved that are they are infinitely differentiable without a completeness hypothesis on the target space F. It's a first version so maybe I'll think about it a bit more before PRing it, but in any case it's there.

[Junyan Xu]

Thanks! The diff looks quite nice as lemmas come in a natural flow and most proofs are of reasonable size, except for changeOrigin_eval_of_finite in Analytic/Basic, which is longer than the infinite counterpart that assumes completeness. Maybe you combined multiple lemmas into the main proof, or is it really more difficult in this case? If we could unify both proofs that would be even nicer.

Some initial comments:
You could remove the commented out lemmas at the end of Analytic/Basic, since you already made copies of them, and this should reduce the diff.
You could make HasFiniteFPowerSeriesOnBall extends HasFPowerSeriesOnBall and I think you will get HasFiniteFPowerSeriesOnBall.toHasFPowerSeriesOnBall automatically.
Why are the double c in the lemma names cCPolynomialAt/On_const? Should they just be called cPolynomialAt/On_const?

[Sophie Morel]

Thanks for the suggestions ! The double c in some places were typos, and I've hunted them down and hopefully removed them all.
Oops, I thought I had gotten all the commented out lemmas ! Removing them.
Good point about making HasFiniteFPowerSeriesOnBall extend HasFPowerSeriesOnBall.

The proof for changeOrigin_eval_of_finite is easier than the proof of its infinite counterpart, it's only longer because I had to write some parts myself and I'm not as effective as the mathlib authors. There's at least one other proof that is extremely clunky. Most of the other proofs and lemmas flow well because they're a copy-paste of the "analytic" lemmas and proofs with minimal adaptations. :sweat_smile:

[Sophie Morel]

Ah, there's two commented out lemmas at the end of Basic that are still here because I wonder whether they're worth adapting.

[Sophie Morel]

I cleaned up a little. As for the proof of changeOrigin_eval_of_finite, one of the things that takes a long time to prove is summability of some series, where I use the fact that they have finite support but take forever to prove that the support is finite. Here is an example of one these long finiteness proofs, extracted as a MWE so everyone can admire the monster:

import Mathlib.Tactic
import Mathlib.Data.Set.Finite
import Mathlib.Data.Finset.Card

open Set

example (n : ℕ) :
    Set.Finite {p : (k : ℕ) × (l : ℕ) × {s : Finset (Fin (k + l)) // s.card = l} |
    p.1 < n ∧ p.2.1 < n} := by
  set s := {p : (k : ℕ) × (l : ℕ) × {s : Finset (Fin (k + l)) // s.card = l} |
      p.1 < n ∧ p.2.1 < n}
  rw [Set.finite_def]
  apply Nonempty.intro
  set g : s → (k : Finset.range n) × (l : Finset.range n) ×
        {s : Finset (Fin (k + l)) | s.card = l} := (fun p =>
          ⟨⟨p.1.1, Finset.mem_range.mpr p.2.1⟩, ⟨p.1.2.1, Finset.mem_range.mpr p.2.2⟩, p.1.2.2⟩)
  set h : (k : Finset.range n) × (l : Finset.range n) ×
        {s : Finset (Fin (k + l)) | s.card = l} → s :=
        fun p => by refine ⟨⟨p.1, p.2.1, p.2.2⟩, ?_⟩
                    simp only [coe_setOf, mem_setOf_eq]
                    exact ⟨Finset.mem_range.mp p.1.property, Finset.mem_range.mp p.2.1.property⟩
  have h1 : ∀ x, h (g x) = x := by
        intro ⟨p, hp⟩
        simp only [coe_setOf, mem_setOf_eq, Sigma.eta]
  have h2 : ∀ x, g (h x) = x := by
        intro ⟨k, l, t⟩
        simp only [coe_setOf, mem_setOf_eq, id_eq]
  set e : s ≃ (k : Finset.range n) × (l : Finset.range n) ×
        {s : Finset (Fin (k + l)) | s.card = l} :=
        {toFun := g
         invFun := h
         left_inv := h1
         right_inv := h2}
  apply Fintype.ofEquiv _ e.symm

There has to be a better way to do this, but I don't know how.

[Kevin Buzzard]

This was the sort of question I'd ask @Chris Hughes in 2018 and he'd make a mathlib PR and then solve it in one line using decide or apply_instance or some other incantation

[Sophie Morel]

If you asked me to prove this as mathematician, I would say that my set has a map into $\mathbb{N}\times\mathbb{N}$ with finite fibers and finite image, so it is finite. However, I have been searching for such a lemma in mathlib in vain. The closest I found is this, but it assumes that the fibers are empty or singletons, not that they are finite.

[Sophie Morel]

I cannot believe that such a thing would not be there...

[Yaël Dillies]

There's #6449 by @Anatole Dedecker. Not sure why it's abandoned. I can try reviving it now if I manage to get cache.

[Sophie Morel]

A pity that this is abandoned indeed. So if you don't revive it, that means I should learn to work with such incantantions as Tendsto f cofinite cofinite, hmm... Or maybe there is yet another way to do the finiteness proof. It actually comes up twice in the current proof of changeOrigin_eval_of_finite, because I later want to show that {p : (l : ℕ) × {s : Finset (Fin (m + l)) // s.card = l} | p.1 < n} is also finite.

[Sophie Morel]

And I did that in the worst possible way, but copy-pasting the previous finiteness proof and modifying it where needed. :see_no_evil:

[Patrick Massot]

Yaël Dillies said:

There's #6449 by Anatole Dedecker. Not sure why it's abandoned. I can try reviving it now if I manage to get cache.

The answer is not so secret: you get away with playing with Lean full time in Cambridge, but Anatole is doing Orsay's M2 AAG.

[Sophie Morel]

So anyway, I wrote the "if a map has finite fibers and a finite image, then its source is finite" lemma, and it's super easy ?

theorem Set.Finite.of_finite_image_of_finite_fibers {α : Type*} {β : Type*} {s : Set α}
    {f : α → β} (hfin1 : Set.Finite (f '' s)) (hfin2 : ∀ y ∈ f '' s, Set.Finite (f ⁻¹' {y})) :
    Set.Finite s :=
  Set.Finite.subset (Set.Finite.biUnion hfin1 hfin2) (fun x hx ↦ Set.mem_biUnion
  (Set.mem_image_of_mem f hx) (by rw [Set.mem_preimage, Set.mem_singleton_iff]))

Now let's see if applying it will be as easy.

[Anatole Dedecker]

Hi again everyone! Indeed I was quite busy for this whole semester so I didn't have time to work on this. I have some Lean time during the holiday but I want to focus on finishing up Ascoli's theorem since people are waiting for it.
Regarding #6449 specifically, the main reason I left it aside is I realized it would be much better to make it not depend on filters as I originally did. While that is satisfying, it's quite obviously the wrong way to order things, and anyway the filter approach didn't work well to do the relative version Yaël suggested. I think I have some unpushed commits on my computer too :see_no_evil:

[Yaël Dillies]

Yeah I think using filters for things like this and docs#IsMinOn is a bit overpowered and will result in people not using the API because it would involve needing to understand and importing filters.

[Yaël Dillies]

This is too foundational to use fancy machinery, basically.

[Yaël Dillies]

I'm happy to have a look into redoing things the basic way. One thing I was surprised is that your HasFiniteFibersOn was restricting to a set on the domain, not to a set on the codomain. Is there any reason for that?

[Yaël Dillies]

I guess it's more general, since every element of $s$ in the codomain having a finite fiber under $f$ is the same as every element in the codomain having finite fiber with the restriction of $f$ to $f^{-1}(s)$? I'm wondering whether we will actually use this extra generality, since it makes the main lemma I have in mind (proving $f^{-1}(s)$ is finite if $s$ is) harder to apply.

[Anatole Dedecker]

Yaël Dillies said:

I guess it's more general, since every element of $s$ in the codomain having a finite fiber under $f$ is the same as every element in the codomain having finite fiber with the restriction of $f$ to $f^{-1}(s)$?

Yes exactly

[Anatole Dedecker]

I have no opinion about usability there, but docs#Finset.preimage already uses something similar

[Sophie Morel]

Junyan Xu said:

except for changeOrigin_eval_of_finite in Analytic/Basic, which is longer than the infinite counterpart that assumes completeness. Maybe you combined multiple lemmas into the main proof, or is it really more difficult in this case? If we could unify both proofs that would be even nicer.

With the help of several people, I reduced the size of that proof, and it is... still longer than in the infinite case. :sweat_smile: But at least it's something like 52 lines against 46, not like 2-3 times as long.

[Sophie Morel]

I made a PR (#9269) for continuously polynomial functions.