Defining ContDiff functions

Stream: general

[Vincent Beffara]

I would like to have a type for functions f : R -> R satisfying ContDiff R 2 f and there are many ways to define this, what would be the better choice in practice / the most idiomatic between these two?

structure CD_option_1 where
  toFun : R -> R
  smooth : ContDiff R 2 toFun

def CD_option_2 : AddSubgroup (R -> R) where
  carrier := {f | ContDiff R 2 f}
  -- whatever is needed to show that it is a subgroup

The second one seems to do a lot of boilerplate things automatically, but the first one enables dot notation which I was not able to get with the second one. Or perhaps I am missing a third option?

[Yaël Dillies]

See the thread about RingOfIntegers for a third option:

def CD_Option_3 : Type _ := CD_Option_2

[Vincent Beffara]

Thanks for the suggestion! In the end I went with this,

def CD_ (n : ℕ) (E : Type*) [NormedAddCommGroup E] [NormedSpace ℝ E] : Subspace ℝ (ℝ → E) where
  carrier := {f | ContDiff ℝ n f}
  zero_mem' := by change ContDiff ℝ n (fun _ => 0) ; apply contDiff_const
  add_mem' hf hg := hf.add hg
  smul_mem' c f hf := hf.const_smul c

abbrev CD (n : ℕ) (E : Type*) [NormedAddCommGroup E] [NormedSpace ℝ E] : Type _ := CD_ n E

because def was hiding too much of the boilerplate that I was hoping to get (and the tradeoff is that it inherits the wrong topology).

[Sébastien Gouëzel]

Vincent Beffara said:

(and the tradeoff is that it inherits the wrong topology).

Isn't this tradeoff too expensive? I mean, getting the wrong topology should be a no-go, because it's something you will never be able to fix (unless you hide your definition behind a type synonym, but then you will need to add back the boilerplate).

[Vincent Beffara]

After defining the semi norms I wanted I just provided instances for uniform space and topological space to override those found through the subtype path, and it seems to work for now. I agree that it feels rather brittle.

[Vincent Beffara]

And it does go against the principle of uniqueness of instances

[Vincent Beffara]

OK so the boilerplate to do is not that heavy, going from abbrev to def involves just this:

variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {k n : ℕ} {R : ℝ} {𝕜 : Type*} [RCLike 𝕜]

def CD_ (n : ℕ) (E : Type*) [NormedAddCommGroup E] [NormedSpace ℝ E] : Subspace ℝ (ℝ → E) where
  carrier := {f | ContDiff ℝ n f}
  zero_mem' := by change ContDiff ℝ (↑n) (fun _ => 0) ; apply contDiff_const
  add_mem' hf hg := hf.add hg
  smul_mem' c f hf := hf.const_smul c

def CD (n : ℕ) (E : Type*) [NormedAddCommGroup E] [NormedSpace ℝ E] : Type _ := CD_ n E

instance : AddCommGroup (CD n E) := by simp only [CD] ; infer_instance
noncomputable instance : Module ℝ (CD n E) := by simp only [CD] ; infer_instance

@[ext] lemma CD.ext (f g : CD n E) (h : f.1 = g.1) : f = g := by
  cases f ; cases g ; simp at * ; simp [h]

@[simp] lemma CD.add_def {f g : CD n E} : (f + g).1 = f.1 + g.1 := rfl

@[simp] lemma CD.smul_def {f : CD n E} : (R • f).1 = R • f.1 := rfl

[Sébastien Gouëzel]

Nice! I would probably avoid simp in the instance definition, as you never know if it will do something complicated (although in this case apparently it doesn't), and use something like

instance : AddCommGroup (CD n E) := inferInstanceAs (AddCommGroup (CD_ n E))

Also, you should probably register a FunLike instance, a ContinuousMapClass instance, and do this for a general source space instead of the real line :-)