inner_product_space and normed_algebra

Stream: maths

[Eric Wieser]

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]

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]

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]

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

[Eric Wieser]

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]

So is the elaboration issue not a problem anymore?

[Eric Wieser]

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]

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]

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

[Eric Wieser]

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

[Eric Wieser]

#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]

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]

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