Zulip Chat Archive

Stream: maths

Topic: Minkowski functional for nonreal scalars

Moritz Doll (Jun 21 2022 at 12:02):

I have almost a complete proof for the fact that the topology of every locally convex space is generated by seminorms. One remaining issue is that the Minkowski functional in Lean is only defined over real vector spaces, whereas I thought it should be defined over any [scalar_tower R k E], where k is the normed field and E is the vector space. Were there any issues with defining it more generally? @Yaël Dillies @Bhavik Mehta

Yaël Dillies (Jun 21 2022 at 12:03):

Do you mean [scalar_tower ℝ k E]?

Moritz Doll (Jun 21 2022 at 12:04):

yes, sorry.

Yaël Dillies (Jun 21 2022 at 12:04):

So this means that k will be ℝ or ℂ, right?

Moritz Doll (Jun 21 2022 at 12:06):

yes, one could also use is_R_or_C, but this is way more structure than one actually needs

Yaël Dillies (Jun 21 2022 at 12:07):

Sure, but what does this generalization give us, apart from k = ℂ?

Moritz Doll (Jun 21 2022 at 12:10):

nothing. I found writing it with the scalar tower gives less clutter. You are free to force me to rewrite it once I made the PR :grinning:

Moritz Doll (Jun 21 2022 at 12:11):

but the question is still whether everything works for the Minkowski functional for ℂ or did you run into some problems?

Yaël Dillies (Jun 21 2022 at 12:12):

I think everything works! After all, ℝ ⊆ ℂ, right?

Moritz Doll (Jun 21 2022 at 12:17):

But scalar multiplication is in ℂ not only in ℝ

Moritz Doll (Jun 21 2022 at 12:18):

Oh, I think I see the point: one has to change in lots of places the symmetry condition to balanced and then everything should go through

Moritz Doll (Jun 21 2022 at 15:52):

I proved the fact that the gauge is a seminorm for k = ℂ, but now there is the question whether in mathlib the statement should be unified with the is_R_or_C typeclass (which seems to be not entirely trivial). It seems that is_R_or_C is missing some important lemmas about coercion.