pointwise limits of linear maps

Stream: general

[Jireh Loreaux]

does mathlib already know that pointwise limits of linear maps are linear (in a TVS)? If so, where is that? I expected to find it in topology/algebra/module but I didn't see it there.

[Jireh Loreaux]

For what it's worth, this is the version I am thinking of:

import topology.algebra.module

open_locale topological_space
open filter

variables {M₁ M₂ R α : Type*}
variables [semiring R] [add_comm_monoid M₁] [add_comm_monoid M₂]
variables [module R M₁] [module R M₂]
variables [topological_space M₂] [t2_space M₂] [has_continuous_add M₂]
variables [topological_space R] [has_continuous_smul R M₂]

definition linear_map_of_pointwise_tendsto {g : α → M₁ →ₗ[R] M₂} {l : filter α}
[l.ne_bot] {f : M₁ → M₂} (h : ∀ x : M₁, tendsto (λ a : α, g a x) l (𝓝 (f x))) : M₁ →ₗ[R] M₂ :=
{ to_fun := f,
  map_add' := λ x y, by
    { refine tendsto_nhds_unique (h (x + y)) _,
      have : (λ a, g a (x + y)) = (λ a, g a x + g a y), from funext (λ a, (g a).map_add' x y),
      rw this,
      exact tendsto.add (h x) (h y) },
  map_smul' := λ r x, by
    { refine tendsto_nhds_unique (h (r • x)) _,
      have : (λ a, g a (r •  x)) = (λ a, r • (g a x)), from funext (λ a, (g a).map_smul' r x),
      rw this,
      exact tendsto.const_smul (h x) r } }

[Yury G. Kudryashov]

I don't think that we have it as a separate definition. There is a proof of this fact inside src#continuous_linear_map.complete_space. Once you add a standalone definition, please replace let Glin : ... := ... with this new definition.

[Jireh Loreaux]

Sure, do you think topology/algebra/module is the correct place to add this?

[Yury G. Kudryashov]

Yes. And I think that we should have a version for add_monoid_homs too.

[Heather Macbeth]

@Jireh Loreaux By the way, I like to use the slightly shorter

(h : tendsto (λ a x, g a x) l (𝓝 f))

to express pointwise convergence, rather than

(h : ∀ x, tendsto (λ a, g a x) l (𝓝 (f x)))

You can get back and forth between the two forms using docs#tendsto_pi_nhds.