Smoothness of `equiv.prod_assoc`

Stream: Is there code for X?

[Oliver Nash]

Do we have the fact that the natural map (E × F) × G → E × F × G is smooth anywhere?

[Oliver Nash]

If not, is the following reasonable:

import analysis.calculus.times_cont_diff

variables (𝕜 E F G : Type*) [nondiscrete_normed_field 𝕜]
variables [normed_group E] [normed_space 𝕜 E]
variables [normed_group F] [normed_space 𝕜 F]
variables [normed_group G] [normed_space 𝕜 G]

-- Assumptions here can be relaxed of course
noncomputable def linear_isometry_equiv_prod_assoc : (E × F) × G ≃ₗᵢ[𝕜] E × F × G :=
{ to_fun    := equiv.prod_assoc E F G,
  inv_fun   := (equiv.prod_assoc E F G).symm,
  map_add'  := by simp,
  map_smul' := by simp,
  norm_map' :=
    begin
      rintros ⟨⟨e, f⟩, g⟩,
      simp only [linear_equiv.coe_mk, equiv.prod_assoc_apply, prod.norm_def, max_assoc],
    end,
  .. equiv.prod_assoc E F G, }

@[simp] lemma coe_linear_isometry_equiv_prod_assoc :
  (linear_isometry_equiv_prod_assoc 𝕜 E F G : (E × F) × G → E × F × G) = equiv.prod_assoc E F G :=
rfl

lemma times_cont_diff_prod_assoc :
  times_cont_diff 𝕜 ⊤ $ equiv.prod_assoc E F G :=
(coe_linear_isometry_equiv_prod_assoc 𝕜 E F G) ▸
(linear_isometry_equiv_prod_assoc 𝕜 E F G).times_cont_diff

[Patrick Massot]

It looks good to me, but @Heather Macbeth or @Sebastien Gouezel can probably comment.

[Floris van Doorn]

This should be an easy consequence of docs#times_cont_mdiff.prod_mk and docs#times_cont_diff_fst and similar.
However, if you need this property for something that is not specifically about reordering/reassociating arguments, I have serious concerns that you are taking an efficient route here.

[Floris van Doorn]

The note
https://leanprover-community.github.io/mathlib_docs/notes.html#continuity%20lemma%20statement
ensures you usually don't have to worry about these issues for continuous, but it applies equally well to times_cont_diff.
If you need this to apply some times_cont_diff lemma to your case, can you use the tips in that library note to generalize said lemma?

[Oliver Nash]

Thanks for the remarks!

[Floris van Doorn]

Oh, I missed the m in docs#times_cont_mdiff.prod_mk. We need some analogue times_cont_diff.prod_mk

[Oliver Nash]

I am aware of the proof avoiding the linear isometry, I just like my approach since I feel like it's more fundamental but I have no strong feelings.

[Oliver Nash]

Regarding the concern that I may be taking an inefficient route, all I want is to know that the evaluation map $Hom_A(E, F) \times E \to F$ is smooth where $E, F$ are normed spaces and $Hom_A(E, F)$ is the space of continuous affine maps.

[Oliver Nash]

I decided to obtain this by factoring this evaluation map as: $Hom_A(E, F) × E ≃ (F × Hom_L(E, F)) × E ≃ F × Hom_L(E, F) × E → F × F → F$

[Oliver Nash]

where $Hom_L(E, F)$ is the space of continuous linear maps, and the final arrow is addition.

[Oliver Nash]

Right in the middle you can see where I need smoothness of associativity. I'm open to suggestions!

[Oliver Nash]

In any case, I'll study your remarks and thank you for proving them.

[Oliver Nash]

Floris van Doorn said:

Oh, I missed the m in docs#times_cont_mdiff.prod_mk. We need some analogue times_cont_diff.prod_mk

docs#times_cont_diff.prod_map

[Floris van Doorn]

that's not quite the same.

[Floris van Doorn]

compare docs#continuous.prod_mk vs docs#continuous.prod_map

[Oliver Nash]

Right, I see.

[Floris van Doorn]

I'm think that the library note applies to your situation, but I'm not sure. What is the lemma that
$Hom_L(E, F) × E → F$
is smooth? The library note probably applies to that lemma.

[Oliver Nash]

I'm actually really interested to learn about how this library note applies here so I'm delighted you're interested.

[Oliver Nash]

Floris van Doorn said:

I'm think that the library note applies to your situation, but I'm not sure. What is the lemma that
$Hom_L(E, F) × E → F$
is smooth? The library note probably applies to that lemma.

I don't think this literally exists in the library but it almost does. See here: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Smoothness.20of.20linear.20evaluation.20map/near/259864674

[Floris van Doorn]

substitute every occurrence of continuous in my library note to times_cont_diff, and the advice is probably still good.

[Oliver Nash]

Understood, I note you even say this in the note itself.

[Floris van Doorn]

Yeah, that lemma should be formulated something like times_cont_diff f -> times_cont_diff g -> times_cont_diff λ x, (f x) (g x) where f : X -> (E →L[𝕜] F) and g : X -> E

[Oliver Nash]

Excellent, this is exactly the sort of example I needed to see. I will use this formalisation (and tag you on the relevant PR) in due course.

[Floris van Doorn]

From your version of the lemma, the proof of this version should be something like times_cont_diff_continuous_linear_eval.comp $ hf.prod_mk hg (using the non-existent prod_mk)

[Oliver Nash]

I have to go for a run now so I've proposed an approach here: #10165