Questions about ContinuousLinearMapWOT

Stream: maths

[Anatole Dedecker]

Arriving after the battle here, but I just noticed the addition of docs#ContinuousLinearMapWOT (thanks @Frédéric Dupuis !) and I have a few questions/suggestions about design decisions.
1) The naming is a bit inconsistent with docs#UniformConvergenceCLM. I don't have a strong opinion about which is better (and WOT is definitely a more standard acronym that CLM) but we should probably decide on some convention since these topologies are going to multiply.
2) Intuitively I would have defined the topology using the docs#WeakBilin machinery, by putting E →WOT[𝕜] F in duality with E ⊗[𝕜] (F →L[𝕜] 𝕜). Thinking back about it it's probably useless extra work, but the thing that worries me is that we currently have to predicate for "the canonical topology on this space is the weak one for this duality". Probably the best is to add the latter rather than redefine ContinuousLinearMapWOT.
3) Is there a reason to restrict to a normed codomain ? I mean it's a bit silly to put a weak space on the codomain since WOT and SOT coincide in that case, but it still seems like an unnecessary restriction. If the only reason was "I don't need it so I won't make my life more complicated" then that's completely fine and I can work on the generalization (I think in any case I'll do a PR to avoid the complicated proof of docs#ContinuousLinearMapWOT.hasBasis_seminorms, which should not be needed thanks to the general facts we have about docs#WithSeminorms)

[Frédéric Dupuis]

No worries about being late to the party -- now I'm the one with less time for Lean, so you can feel free to take over! :-)

1) The naming is a bit inconsistent with docs#UniformConvergenceCLM. I don't have a strong opinion about which is better (and WOT is definitely a more standard acronym that CLM) but we should probably decide on some convention since these topologies are going to multiply.

Yeah, it would be nice to have a more consistent naming scheme. I personally prefer to have a type "mainly" named after what it contains (i.e. continuous linear maps in this case), but I don't have a very strong opinion here.

2) Intuitively I would have defined the topology using the docs#WeakBilin machinery, by putting E →WOT[𝕜] F in duality with E ⊗[𝕜] (F →L[𝕜] 𝕜). Thinking back about it it's probably useless extra work, but the thing that worries me is that we currently have to predicate for "the canonical topology on this space is the weak one for this duality". Probably the best is to add the latter rather than redefine ContinuousLinearMapWOT.

I don't think it's possible to use docs#WeakBilin here, we would actually need a multilinear version of it. The issue is that the weak operator topology on E →L[𝕜] F is induced by the function inducingFn : (E →WOT[𝕜] F) →ₗ[𝕜] E × F⋆ → 𝕜 defined as fun A ⟨x, y⟩ => y (A x); we would need it to be bilinear (i.e. of type (E →WOT[𝕜] F) →ₗ[𝕜] E × F⋆ →ₗ[𝕜] 𝕜) for this to be in the right form for WeakBilin. It does lead to an unfortunate duplication of code though since pretty much all the proofs work the same way.

3) Is there a reason to restrict to a normed codomain ? I mean it's a bit silly to put a weak space on the codomain since WOT and SOT coincide in that case, but it still seems like an unnecessary restriction. If the only reason was "I don't need it so I won't make my life more complicated" then that's completely fine and I can work on the generalization (I think in any case I'll do a PR to avoid the complicated proof of docs#ContinuousLinearMapWOT.hasBasis_seminorms, which should not be needed thanks to the general facts we have about docs#WithSeminorms)

A lot of typeclass requirements could probably be weakened, yes. You can definitely feel free to work on that!

[Anatole Dedecker]

Yes I was aware of the issue for 2, which is why I was thinking about using tensor products. But I guess the associated extra machinery makes it not worth it.
For the naming I see your point, but I'm not sure about it. As in, WeakOperatorCLM seems very easy to find as well, and the docstring can then take care of explaining more. But in any case the main problem is I don't really know what to name UniformConvergenceCLM which isn't ridiculously long, since UOT for UniformOperatorTopology seems very nonstandard...

[Frédéric Dupuis]

Yeah, I briefly thought about the tensor product solution, but that sounds rather painful... Although if you think it's worth it, feel free to go ahead and refactor it.

I'm not too sure how else to call UniformConvergenceCLM either, in any case I don't really have a very strong opinion like I said. Maybe we can vote on it?

[Jireh Loreaux]

I'm okay with WeakOperatorCLM and StrongOperatorCLM, when we finally get around to fixing up that PR (this is on my TODO list).

[Anatole Dedecker]

I forgot to mention #17492 here.

[Anatole Dedecker]

#18443 does a similar golf for docs#LinearMap.weakBilin_withSeminorms