Continuous Bilinear Maps

Stream: mathlib4

[Alex Meiburg]

I needed to prove the following theorem, and it was harder than I expected.

theorem continuous_stupid {M N : Type*}
  [NormedAddCommGroup M] [Module ℝ M] [ContinuousSMul ℝ M] [FiniteDimensional ℝ M]
  [NormedAddCommGroup N] [Module ℝ N]
  (f : N →L[ℝ] M →L[ℝ] ℝ) :
    Continuous fun (x : N × M) ↦ f x.1 x.2 :=
  have h_eval : Continuous (fun p : (M →L[ℝ] ℝ) × M ↦ p.1 p.2) := by
    have h_sum : Continuous (fun p : (M →L[ℝ] ℝ) × M ↦
        ∑ i, p.1 (Module.finBasis ℝ M i) * ((Module.finBasis ℝ M).repr p.2) i) := by
      refine continuous_finset_sum _ fun i _ ↦ .mul (by fun_prop) ?_
      exact ((Module.finBasis ℝ M).coord i).continuous_of_finiteDimensional.comp continuous_snd;
    convert h_sum with x
    rw [ ← (Module.finBasis ℝ M).sum_repr x.2, map_sum]
    simp [mul_comm]
  h_eval.comp <| .prodMk (f.continuous.comp continuous_fst) continuous_snd

which is defeq to the following theorem

theorem continuous_stupid' {M N : Type*}
  [NormedAddCommGroup M] [Module ℝ M] [ContinuousSMul ℝ M] [FiniteDimensional ℝ M]
  [NormedAddCommGroup N] [Module ℝ N]
  (f : N →L[ℝ] M →L[ℝ] ℝ) :
    Continuous (Function.uncurry (f · ·)) :=
  continuous_stupid f

Basically at no point was fun_prop able to help, or continuity, and I couldn't find any relevant theorems in Mathlib much either. This makes me think that I'm doing something wrong - that maybe this is a theorem I "shouldn't want" for some reason or another.

Or, if it's a "good" theorem, should it be PR'ed?

[Weiyi Wang]

I just searched by guessing names. How close is this to docs#ContinuousLinearMap.uncurryBilinear ?

[Alex Meiburg]

Oh, actually I think the conclusion is identical to ContinuousLinearMap.continuous₂. But that version requires NormedSpace.

[Sébastien Gouëzel]

Your version is using ContinuousSMul and FiniteDimensional, but this is enough to guarantee the space is normable. So your statement follows from the one we already have. Also, I think that the natural statement is really the one one normed spaces (it's not true for general topological vector spaces).

[Sébastien Gouëzel]

In fact your statement is a little bit strange since you assume a norm and ContinuousSMul. I think this already implies normed space, even without the finite dimensional assumption. But I can't think of a setting where this is a natural assumption.

[Kevin Buzzard]

You could prove that everything in sight has the $\R$-module topology and then invoke docs#IsModuleTopology.continuous_bilinear_of_finite_right

[Michael Rothgang]

@Patrick Massot also proved a similar statement for our Levi-Civita project:
https://github.com/leanprover-community/mathlib4/blob/a809b7383778833093c30118a169119fa00bc30d/Mathlib/Geometry/Manifold/VectorBundle/Misc.lean#L49 has

def IsBilinearMap.toContinuousLinearMap
    {𝕜 : Type*} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
    {E : Type*} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E]
    [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [FiniteDimensional 𝕜 E]
    [T2Space E]
    {F : Type*} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F]
    [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] [FiniteDimensional 𝕜 F]
    [T2Space F]
    {G : Type*} [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G]
    [IsTopologicalAddGroup G] [ContinuousSMul 𝕜 G]
    {f : E → F → G} (h : IsBilinearMap 𝕜 f) : E →L[𝕜] F →L[𝕜] G :=
  IsLinearMap.mk' (fun x : E ↦ h.toLinearMap x |>.toContinuousLinearMap)
      (by constructor <;> (intros;simp)) |>.toContinuousLinearMap

[Anatole Dedecker]

Kevin, as Sébastien says, the right generality for this is that of normed/normable spaces, in which case your approach doesn't work.

[Michael Rothgang]

(deleted)

[Michael Rothgang]

Looking again, this is very similar to docs#ContinuousLinearMap.continuous₂: is the right solution to generalise that one to not require a choice of norm?

[Anatole Dedecker]

My instinct reacting to this is "why on earth would you work with E →L[𝕜] F →L[𝕜] G if you're not in a normed setting", because using this to represent continuous bilinear map is really wrong in general

[Anatole Dedecker]

Michael Rothgang said:

Looking again, this is very similar to docs#ContinuousLinearMap.continuous₂: is the right solution to generalise that one to not require a choice of norm?

Indeed we may be lacking a typeclass for normable spaces I guess. In the meantime I guess a temporary specialization to finite dimensional spaces would be acceptable.

[Yury G. Kudryashov]

Anatole Dedecker said:

My instinct reacting to this is "why on earth would you work with E →L[𝕜] F →L[𝕜] G if you're not in a normed setting", because using this to represent continuous bilinear map is really wrong in general

Should we add ContinuousBilinearMap?

[Etienne Marion]

Yury G. Kudryashov said:

Should we add ContinuousBilinearMap?

I actually have many draft PRs about that because we needed it for the Brownian motion project, for example #26315, but I kind of struggled with the level of generality that would be required, because in the project we only need it for $\mathbb{R}$ but we use positive semidefinite forms which makes sense more generally, and then I got busy so I did not reach a conclusion.

[Anatole Dedecker]

I think this would be a good addition. We can technically represent it as ContinuousMultilinearMap R ![X, Y] Z, but I think this will be too annoying to use

[Yury G. Kudryashov]

Also, it only works if X and Y are in the same universe.

[Moritz Doll]

Yury G. Kudryashov said:

Should we add ContinuousBilinearMap?

I would like to have that, because for the Schwartz space and tempered distributions this comes up frequently

[Alex Meiburg]

Sébastien Gouëzel said:

In fact your statement is a little bit strange since you ...

Alright, this is the kind of thing I was expecting to hear, that my typeclasses were strange in some way or another and that was making it harder.

[Patrick Massot]

I don’t have time to read all messages in detail, but I can already why we are working in a normable setting without having a norm. In differential geometry we don’t want to fix a norm on the tangent spaces, although we know they are normable.

[Anatole Dedecker]

I don’t think the question here is about Normed/Normable, the latter should exist and the theorems we’ve talked about should work in that setting. My point was only to emphasize that one should not ask too much of these theorems, and the general rule of thumb is « either you assume Normed/Normable, or you don’t use the currying trick »