Introduce a class for `Continuous DFunLike.coe`?

Stream: maths

[Yury G. Kudryashov]

In #17319 (draft, no docs, no instances) I introduce two typeclasses saying Continuous fun f : F ↦ DFunLike.coe f and Continuous fun (f, x) : F × X ↦ DFunLike.coe f x, respectively. I suggest that we use them instead of lemmas like docs#ContinuousMap.continuous_eval_const etc

• Better names (for the classes and/or theorems) are very welcome.
• Comments on the design are more than welcome.

[Anatole Dedecker]

I’ll have a look at the PR but just from your message this seems like a good idea, especially since type aliases for topologies on function spaces (e.g operator spaces) are almost surely going to multiply

[Yury G. Kudryashov]

How should I call the theorem saying Continuoud DFunLike.coe? I have 3 ideas, and each is bad for some reason.

• continuous_dfunLikeCoe mention implementation detail (DFunLike) in the name;
• continuous_toFun conflicts with ContinuousMap.continuous_toFun etc (technically, it doesn't, but I don't want to have confusion here);
• continuous_coeFn has traces of a no longer existing Lean 3 name.

[Daniel Weber]

docs#CoeFun does exist in Lean 4

[Eric Wieser]

An argument against such a typeclass is that we don't have anything similar to generalize over coe_add, coe_neg etc lemmas

[Yury G. Kudryashov]

IMHO, the main reason not to have a typeclass for coe_add at the moment is that we can't make it a rfl lemma, so we'll have to repeat it for specific types anyway.

[Yaël Dillies]

Note however that such a typeclass would be very useful for reproducing kernel Hilbert spaces: !3#16351

[Jireh Loreaux]

Yaël, I still think the right approach to that is what I suggested in this comment though.

[Yaël Dillies]

Yeah, that's the other option, but in a sense isn't the point of a RHKS typeclass to make that canonical embedding into functions be the coercion to function?

[Jireh Loreaux]

Is that not what I said in that comment? nevermind, I see your point.

[Yaël Dillies]

Tell me if I'm wrong, but I think I've noticed something more serious with your suggestion, Jireh. You say

You can then set up a fun_like instance in the natural way. I think if the first one doesn't work, then the second is definitely the way to go unless I'm missing something.

But no you cannot, because 𝕜 only appears left of the colon in the instance [RKHS 𝕜 H] : FunLike H X V that you are suggesting

[Yury G. Kudryashov]

Can K be an outParam here?

[Yaël Dillies]

That's a question that only people who use RHKS in real life (@Shing Tak Lam ?) can answer. Eg don't we ever need that a ℂ-RKHS is a ℝ-RKHS?

[Yury G. Kudryashov]

BTW, do we need to make a decision about RKHS in order to make a decision about class ContinuousEvalConst?

[Jireh Loreaux]

I would expect making 𝕜 an outParam is probably okay, but :shrug: (does semiOutParam not work?). I don't think this should affect decisions about ContinuousEvalConst. I'm not planning to work on RKHS anytime soon, and I think Shing Tak Lam is unavailable for working on Lean.

[Yury G. Kudryashov]

BTW, with recent migration towards FunLike + mixin it may be a better idea to have calss RKHS ... [FunLike F X V] : Prop

[Yury G. Kudryashov]

@Eric Wieser About coe_add etc: I think that we should have these it would be nice to have these, but I don't know how to do it without introducing too many extra TC searches.