Continuity of ContinuousLinearMap.mk/toFun

Stream: mathlib4

[Tomas Skrivan]

Part of #24095 that allows writing continuous linear maps as for example fun x =>L[R] 3*x + 2*x I need to prove these two theorems:

import Mathlib

theorem ContinuousLinearMap.mk_continuous
    {R : Type*} [NormedField R]
    {M : Type*} [TopologicalSpace M] [AddCommGroup M] [Module R M]
    {M₂ : Type*} [TopologicalSpace M₂] [AddCommGroup M₂] [Module R M₂]
    {M₃ : Type*} [TopologicalSpace M₃] [AddCommGroup M₃] [Module R M₃] [IsTopologicalAddGroup M₃]
    (f : M → M₂ → M₃)
    (hfy : ∀ x, IsLinearMap R (f x ·))
    (hf : Continuous ↿f) :
    Continuous (fun x =>
      { toFun := (f x ·),
        map_add' := (hfy x).1,
        map_smul' := (hfy x).2,
        cont := by fun_prop : M₂ →L[R] M₃ }) := by
  sorry

theorem ContinuousLinearMap.continuous_apply
    {R : Type*} [NormedField R]
    {M : Type*} [TopologicalSpace M]
    {M₂ : Type*} [TopologicalSpace M₂] [AddCommGroup M₂] [Module R M₂]
    {M₃ : Type*} [TopologicalSpace M₃] [AddCommGroup M₃] [Module R M₃]
    [IsTopologicalAddGroup M₃] [ContinuousConstSMul R M₃]
    (f : M → M₂ →L[R] M₃) (y : M₂)
    (hf : Continuous f) :
    Continuous (fun x : M => f x y) := by
  sorry

I'm not even sure if they are provable as currently stated. I could probably hack together proof over normed spaces but I'm suspecting they might be true more generally. Any help with these theorems would be appreciated.

[Sébastien Gouëzel]

For the second one, with slightly different assumptions:

theorem ContinuousLinearMap.continuous_apply
    {R : Type*} [NormedField R]
    {M : Type*} [TopologicalSpace M]
    {M₂ : Type*} [TopologicalSpace M₂] [AddCommGroup M₂] [Module R M₂]
    {M₃ : Type*} [TopologicalSpace M₃] [AddCommGroup M₃] [Module R M₃]
    [IsTopologicalAddGroup M₃] [ContinuousSMul R M₂]
    (f : M → M₂ →L[R] M₃) (y : M₂)
    (hf : Continuous f) :
    Continuous (fun x : M => f x y) :=
  (continuous_eval_const y).comp hf

[Sébastien Gouëzel]

The other one looks wrong to me: pointwise convergence should not entail norm convergence for operators, and hf is essentially pointwise convergence, and your conclusion is essentially norm convergence.

[Sébastien Gouëzel]

Here is a counterexample to the first one. Take $M=\{1/n\}_{n \ge 1} \cup \{0\}$ and $M_2$ the space of real sequences tending to 0, with the sup norm, and $M_3 = \mathbb{R}$. Let $f 0 = 0$, and let $f (1/n)$ be the linear form taking a sequence to its $n$-th coordinates. Then $(x, u) \mapsto f (x, u)$ is continuous (because at any given $u$ large enough coordinates are small), but $x \mapsto f x$ is not continuous in the operator topology (because any $f (1/n)$ is far from $f 0$, as can be seen on the sequence equal to $1$ at $n$ and $0$ elsewhere).

[Tomas Skrivan]

For the first one, what if you also assume linearity in x?

[Tomas Skrivan]

(It might take me a while to parse your counterexample which might answer my question)

[Tomas Skrivan]

But I think the first one should be provable if f is bilinear and continuous over normed spaces, no?

[Sébastien Gouëzel]

It shouldn't make a difference if it's linear in x or not. Even if f is bilinear and its uncurried form is continuous, over a normed vector space, it doesn't imply continuity in the operator norm.

[Sébastien Gouëzel]

(When the space is finite-dimensional over the reals, though, everything is fine, because norm-continuity and pointwise-continuity are equivalent)

[Tomas Skrivan]

I see, I clearly do not understand the math here. What I want is some condition on (f : M → M₂ → M₃) such that I can turn it into M →L[R] M₂ →L[R] M₃. Maybe bilinearity and boundeness of the uncurried f?

[Sébastien Gouëzel]

The standard condition, if f is bilinear, is the existence of C such that $\|f (x, y)\| \le C \|x\| \cdot \|y\|$.

[Tomas Skrivan]

Can it be somehow formulated such that it is solvable by fun_prop or other tactic?

[Sébastien Gouëzel]

I don't think in a general space there is a good strategy that is amenable to fun_prop. However, doing it in finite-dimensional vector spaces would probably be already useful: when you build something with an explicit formula, essentially all the time you will be in finite dimension -- and in PhysLean my guess is that this will also be the main situation. Let me try to craft a theorem like that.

[Sébastien Gouëzel]

Here it is:

theorem ContinuousLinearMap.mk_continuous
    {𝕜 : Type*} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
    {M : Type*} [TopologicalSpace M]
    {M₂ : Type*} [NormedAddCommGroup M₂] [NormedSpace 𝕜 M₂]
    {M₃ : Type*} [NormedAddCommGroup M₃] [NormedSpace 𝕜 M₃]
    [FiniteDimensional 𝕜 M₂]
    (f : M → M₂ → M₃)
    (hfy : ∀ x, IsLinearMap 𝕜 (f x ·))
    (hf : Continuous ↿f) :
    Continuous (fun x =>
      { toFun := (f x ·),
        map_add' := (hfy x).1,
        map_smul' := (hfy x).2,
        cont := by fun_prop : M₂ →L[𝕜] M₃ }) :=
  continuous_clm_apply.2 (fun y ↦ by simp; fun_prop)

The assumptions are certainly not optimal (one shouldn't need a normed space, a topological vector space should be enough) but that's what we currently have in continuous_clm_apply.

[Tomas Skrivan]

Thanks, this looks nice! Finite dimensional version should cover most use cases for now and we can always generalize later