[Merged by Bors] - feat(analysis/calculus/times_cont_diff): smoothness of f : E → Π i, F i

[urkud]

Also add helper lemmas/definitions about multilinear maps.

---

[sgouezel]

All the times_cont_diff code is perfect, and can be merged right away. However, I am not convinced by the times_cont_mdiff part since you are not dealing with functions taking values in product manifolds. Do you think it is worth going directly for the right generality, or that in any case we will need to duplicate the API since there is no way to handle all situations simultaneously?

[sgouezel]

Is there really no way to have Lean find this instance by itself?

[urkud]

I tried and failed.

[sgouezel]

I am not sure about this: I understand that this is precisely what you need for your Whitney-like embedding theorem (with functions taking values in a product space), but I feel doing directly in the right generality can avoid a lot of code duplication later on.

[urkud]

In a not-yet-PRd part of the branch I duplicate the lemmas about manifold product for the case of E × F with the identity model. I see no reasonable way to avoid duplication of API. Of course, I can define the identity diffeomorphism between E × F or Π i, E i with two models, but this won't give us a nice dot notation.

[sgouezel]

I don't mean between two and many. I mean that, for many, you have the situation of model with corners I' i : H i -> E i, and then you want to consider model_with_corners.pi I' and use this one to formulate pi lemmas.

[urkud]

I will add lemmas about model_pi in another PR but they won't give me lemmas about 𝓘(𝕜, Π i, F i) for free. Same with model_prod: I had to add lemmas like smooth.prod_space to deal with 𝓘(𝕜, E × F) (I'll PR these lemmas later today). Possibly we can add typeclasses [is_prod_model] and [is_pi_model] that verify that a model on M × N is actually equal to IE.prod IF, then formulate theorems about prod for these lemmas, and similarly for pi.

[urkud]

But I can't come up (yet?) with classes/instances that will handle, e.g., M → Π i, E i × F i.

[urkud]

Probably it's better to add [is_trivial_model I] with instances for the trivial model, model_prod, and model_pi. Then we can have times_cont_mdiff_at.to_trivial_right etc. But this doesn't give us lemmas like times_cont_mdiff_at_pi_space for free (I mean, without stating them).

[sgouezel]

I like the idea of is_prod_model and is_pi_model. I don't understand the is_trivial_model idea, though: one can take products of non-trivial models, and I'd still like the theorems on smoothness into products to apply in this situation. Do you prefer that we merge this now and postpone the improvement to a later PR, or would you agree to adapt the current PR to cover already the more general situation?

[urkud]

See #6681

[urkud]

What should be the definition/instances of is_prod_model/is_pi_model so that they cover cases like Π i, E i × F i? As for is_trivial_model I meant something like is_trivial_model (I : smooth_model_with_corners k E H) [charted_space E H] := (is_trivial_model : I = 𝓘(...)) (is_trivial_charted : ...). Then we can have to_model_self_left/to_model_self_right/of_model_self_left/of_model_self_right operations on smooth etc.

P.S.: I would prefer to have this and #6681 merged before we agree on the correct design of model_prod H H' <-> H × H'.

[sgouezel]

ok. Let's merge this and refactor later if/when needed. A difficulty I see is that you also want these statements for euclidean_space ℝ (fin n)(which is our "standard" model forn`-dimensional real manifolds, but currently your lemmas don't apply because the distance in the target is not the same).

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests