Measures on affine_space

Stream: maths

[Eric Wieser]

We have docs#measure_space_of_inner_product_space that puts the obvious volume measure on an inner product space. Should we have something similar for docs#normed_add_torsor, defined by subtracting some arbitrary origin from the set and measuring it back in the vector space?

[Eric Wieser]

One obvious trap here is that inner product spaces are normed_add_torsors over themselves

[Yury G. Kudryashov]

So, you can't avoid diamonds.

[Eric Wieser]

I assume you're referencing the previous discussion of diamonds on measures for euclidean_space?

[Eric Wieser]

I think we probably can still put off dealing with diamonds if we de-instance measure_space_of_inner_product_space and replace it with a more general version for affine_spaces over inner product spaces.