Finding the correct typeclass for `has_smul`

Stream: general

[Moritz Doll]

I have a complicated structure (Schwartz spaces) on which I want to define scalar multiplication and I fail to find the correct typeclasses to make everything work. The issue is that in order to prove properties for the scalar multiplication I need to take the norm of an element, but
at the same time I want the typeclass system to find instances for nat so that I can build the algebraic structure for free.

Not really #mwe but

import analysis.normed_space.basic
import analysis.calculus.cont_diff
import data.complex.is_R_or_C

variables {R E F : Type*}
variables [normed_add_comm_group E] [normed_space ℝ E]
variables [normed_add_comm_group F] [normed_space ℝ F]

variables (E F)

structure schwartz :=
  (to_fun : E → F) (foo : cont_diff ℝ ⊤ to_fun) -- I spare you the real condition

variables {E F}

namespace schwartz

instance fun_like : fun_like (schwartz E F) E (λ _, F) :=
{ coe := λ f, f.to_fun,
  coe_injective' := sorry }

variables [semiring R] [module R ℝ] [module R F] [smul_comm_class ℝ R F]
variables [has_continuous_const_smul R F] [has_coe R ℝ]

variables (r : R)
#check ∥(r : ℝ)∥ -- Some version of this has to work

instance : has_smul R (schwartz E F) :=
⟨λ c f, ⟨c • f, sorry⟩ ⟩ -- in this sorry I need a definition of ∥c∥

instance : has_add (schwartz E F) :=
⟨λ f g, ⟨f + g, sorry⟩ ⟩

instance : has_zero (schwartz E F) :=
⟨ ⟨0, sorry⟩ ⟩

instance : add_comm_monoid (schwartz E F) :=
fun_like.coe_injective.add_comm_monoid _ rfl (λ _ _, rfl) (λ _ _, rfl)

end schwartz

[Eric Wieser]

I think you might be out of luck

[Eric Wieser]

Presumably you need not only a definition of ∥c∥, but you want docs#norm_smul to be true?

[Eric Wieser]

Ah, I think you can get away with is_scalar_tower R ℝ F

[Eric Wieser]

Because then you can turn the action by R into an action by ℝ

[Eric Wieser]

docs#smul_one_smul

[Sebastien Gouezel]

Do you have examples in mind other than R = ℝ? (or maybe R = complex numbers, in which case is_R_or_C R would be enough?)

[Moritz Doll]

The important examples would be R = ℤ and R = ℕ.

[Moritz Doll]

(deleted)

[Anatole Dedecker]

I think this is the same reason why some lemmas about docs#exp are stated with docs#is_R_or_C although the correct condition would be "the norm of a natural number is itself (as a real)"

[Anatole Dedecker]

e.g docs#exp_series_radius_eq_top

[Moritz Doll]

It seems that I might get away with is_scalar_tower R ℝ F and using ∥r • (1 : ℝ)∥, which feels rather dirty

[Sebastien Gouezel]

For ℤ and ℕ, you don't need anything more because an additive group always has these actions for free.

[Anatole Dedecker]

Yes but that doesn’t give you anything about the norm right ?