infer `Module ℝ M` from `Module R M`

Stream: maths

[Tomas Skrivan]

Is there a way to infer Module ℝ M from IsROrC R and Module R M?

This might be XY problem, what I really want is to write an integral of a function to a normed space over R. Maybe I should write everywhere both [NormedSpace R Y] and [NormedSpace ℝ Y]? I don't like that but it is a solution.

mwe

import Mathlib

open MeasureTheory

variable
  {R} [IsROrC R]
  {X} [MeasureSpace X]
  {Y} [NormedAddCommGroup Y] [NormedSpace R Y]

variable (f : X → Y)

/-
failed to synthesize instance
  NormedSpace ℝ Y
-/
#check ∫ x, f x

variable [NormedSpace ℝ Y]

#check ∫ x, f x -- works

[Sébastien Gouëzel]

The standard solution is indeed to add a [NormedSpace ℝ Y] in the context. In applications, though, you can derive explicitly the real normed space structure from the R-normed space structure, but it's not something that can be done by typeclass inference because it couldn't guess the R. Note that, in concrete applications, you won't have anything to do because a complex normed space structure automatically yields a real one.

[Jireh Loreaux]

You could write that instance, but you don't want to, as it will lead to diamonds. What you probably want instead is [NormedSpace ℝ Y] along with an [IsScalarTower ℝ R Y] instance.

[Jireh Loreaux]

(Side note: in Mathlib we generally use 𝕜 or K for the argument to IsROrC, but of course you can do what you want.)

[Tomas Skrivan]

Ok makes sense.

The thing is I'm doing something heretical. I'm writing programs and at the end of the day when I want to run the program I choose R=Float + inconsistend axiom IsROrC Float. So in addition I should add an instance Module Float X → Module ℝ X.

[Tomas Skrivan]

Jireh Loreaux said:

(Side note: in Mathlib we generally use 𝕜 or K for the argument to IsROrC, but of course you can do what you want.)

Yeah I know but it breaks emacs :( it does not like unicode characters like 𝕜 and it breaks parsing/lsp. I would be interested if someone knows how to fix that.

[Jireh Loreaux]

Well, K still works. That's what is used throughout the Data.IsROrC.Basic (or whatever the first file is). But I have no idea about the emacs problem. I've historically used emacs for everything, but now I only use VS Code for Lean.

[Tomas Skrivan]

I should invest some time to set up VS Code properly but overcoming muscle memory is hard :/

[Mauricio Collares]

The lsp-mode encoding issue is being worked around at lean4#2646, but I think that is on hold for the moment

[Mauricio Collares]

There's also an eglot version of lean4-mode, which doesn't support semantic highlighting but doesn't suffer from encoding issues