Zulip Chat Archive

Stream: maths

Topic: inner_product_space and normed_algebra


Eric Wieser (Apr 18 2022 at 11:25):

Do we have a way of indicating that a type is both a docs#inner_product_space and a docs#normed_ring? The former extends has_norm, so [normed_ring R] [inner_product_space R] isn't possible.

The closest I can find is docs#is_R_or_C, but this is too strong for docs#quaternion

Yaël Dillies (Apr 18 2022 at 12:04):

Maybe is_R_or_C will generalize to such a typeclass? That would be nice, because is_R_or_C is a weird dump of atoms (and I think $$\Q$$ and $$\Q[i]$$ satisfy it as well.

Kevin Buzzard (Apr 18 2022 at 12:09):

is_R_or_C is a way of saying "is an archimedean local field" (a field complete with respect to an archimedean norm).

Eric Wieser (May 02 2022 at 13:11):

The context of the question is docs#matrix.frobenius_nnnorm_mul, which feels like it should be true on the quaternions too

Eric Wieser (Mar 14 2023 at 16:36):

Eric Wieser said:

[docs#inner_product_space] extends has_norm, so [normed_ring R] [inner_product_space R] isn't possible.

I've created #18583 as an attempt at removing this extends, though I don't expect it to pass CI just yet. port-status#analysis/inner_product_space/basic is far enough away that this could still be possible.

Jireh Loreaux (Mar 14 2023 at 17:30):

So is the elaboration issue not a problem anymore?

Eric Wieser (Mar 14 2023 at 17:37):

Frédéric Dupuis said:

I run into some very annoying elaboration issues where I have to constantly spoonfeed it 𝕜 and/or α in lemmas that rewrite norms in terms of inner products, even though the relevant instance is directly present in the context.

is still a problem, but the old solution didn't help you if you wanted both a real- and complex- valued inner product on a normed_add_comm_group α. I don't agree that I need to spoon-feed it α, but indeed 𝕜 still has to be passed in lots of places

Jireh Loreaux (Mar 14 2023 at 17:43):

How bad is this elaboration problem (i.e., are you needing to make edits for it in 2 places, 2 dozen, or 2 hundred)?

Your normed_ring or normed_algebra reasoning is more convincing to me than having both real and complex inner products. It seems like there are just so few situations when you have a complex inner product, but you want the real one, and in those cases I would be inclined to simply locally disable the complex instance.

Eric Wieser (Mar 14 2023 at 17:45):

I guess you could count the net change in numbers of 𝕜s in the diff

Eric Wieser (Mar 14 2023 at 17:47):

My guess is that it would be around 100 places where 𝕜 has to be specified explicitly where it previously didn't

Eric Wieser (Mar 15 2023 at 02:04):

#18583 is green (ignoring style) and +360 −303 (edit: +330 −281). At least 128 of the modified lines are just adding new typeclass arguments, and probably another 100 are adding _s to existing elaboration hacks.

Eric Wieser (Mar 15 2023 at 02:05):

I've spun off two dependencies to try and remove some of these, so that they don't have to be modified in the diff

Eric Wieser (Mar 17 2023 at 22:32):

It turns out that this refactor has now made the linter aware that there were some lemmas that didn't use the inner product structure at all. I've spun out #18605, and added a much longer description to #18583


Last updated: Dec 20 2023 at 11:08 UTC