A `ContinuousConstMul` class

Stream: mathlib4

[Jireh Loreaux]

In functional analysis, more specifically operator algebras, one often considers topologies weaker than the norm topology. There are a plethora of these, and virtually none of them satisfy docs#ContinuousMul because multiplication is not jointly continuous, but it is continuous in each variable separately. Sometimes multiplication is jointly continuous on bounded sets.

In fact, this separate continuity of multiplication is really the correct hypothesis for a bunch of places where we use ContinuousMul. E.g., it is the proper assumption for docs#Set.isClosed_centralizer, but it's also the correct one for working with topological algebras. Of course, one way to spell this separate continuity is ContinuousConstSMul α α and ContinuousConstSMul αᵐᵒᵖ α, but this is painful because it means (a) you need to write down both classes whenever you want to prove something about it, and (b) all the generic lemmas are about • instead of *. I think this is very inconvenient. So, I was going to create a new class ContinuousConstMul α which assumes continuity in each variable (not just one, because that never arises in practice), but when I went to do so, I saw that the docstring for ContinuousMul explicitly recommends ContinuousConstSMul!

I think this is terrible for anything but the absolute most basic use cases. I would like to add this ContinuousConstMul class and change the spelling recommendation. Do I have support?

[Jireh Loreaux]

I am planning not to to_additive-ize this, because I think separate continuity of addition never arises in practice where one does not already have joint continuity.

[Yoh Tanimoto]

Defining a new class seems a good idea. what about SeparatelyContinuousMul?

[Jireh Loreaux]

That's fine, I don't really care about the name.

[Eric Wieser]

I would be inclined to additivize anyway, just for the sake of Additive X etc

[Eric Wieser]

I think you'll run into trouble if you try to additivize a proof that uses instContinuousMul.toSeparatelyContinuousMul.continuous_mul_const if SeparatelyContinuousAdd doesn't exist

[Jireh Loreaux]

Yes, I've already decided to do that but for other resasons, just so that I can let @[to_additive] write the pre-existing add_const lemmas instead of writing them myself.

[Jireh Loreaux]

Note that Additive X will almost never come up in practice outside of the generic lemmas, because all these things where you have a separate but not jointly continuous mul have a ring structure anyway

[Yaël Dillies]

Can the naming convention follow whatever is done for docs#MeasurableMul ?

[Jireh Loreaux]

That would be much more disruptive, because the meaning of ContinuousMul would change under everyone's feet.

[Yury G. Kudryashov]

Another option is to rename MeasurableMul to SeparatelyMeasurableMul and set a reminder to rename MeasurableMul_2 to MeasurableMul after ~6 months.

[Jireh Loreaux]

If we want to unify the names, let's worry about it later and do it the way Yury suggested with a delay. For that we'll need to decide whether we prefer Separately + Mul or Mul + Mul\_2

[Jireh Loreaux]

#35589

[Yaël Dillies]

Jireh Loreaux said:

That would be much more disruptive, because the meaning of ContinuousMul would change under everyone's feet.

I understand, but this sort of naming mismatch is of the most annoying kind. Relatedly, did you know that now is probably the last time in history where ContinuousMul is used so little? :grinning_face_with_smiling_eyes:

[Jireh Loreaux]

no, why is that?

[Jireh Loreaux]

And again, I'm not saying we can't rename them, but let's not shift it under everyone's feet with no good deprecation mechanism or time in-between.

[Yaël Dillies]

Jireh Loreaux said:

no, why is that?

I just mean that mathlib keeps on growing and that the earlier a refactor can be done the better

[Eric Wieser]

I think that effect is probably worth considering on the timescale of a few months, but less important for the question of "should this be one PR or two PRs"

[Eric Wieser]

At any rate this ought to be an easy deprecation to do later; no names will change besides the typeclass itself (and instances which are exempt)

[Jireh Loreaux]

This is merged. So if you would like to bikeshed about coordinating naming, I'm happy to do so.

[Matthew Ballard]

Where did the performance improvement come from?

[Jireh Loreaux]

:shrug: