Help with idiomatic definitions

Stream: general

[giacomo gallina]

Hi, I'm trying to formalize some facts about orthogonal polynomials, but I'm not sure of the best and most idiomatic way of defining things. Let me explain:
I have the space of polynomials over ℝ, ℝ[X], and I want to put a scalar product on it. This scalar product is just the L² scalar product using some reasonable measure. Right now I have defined a structure that holds this measure and all its relevant properties, called IntegralScalarProduct.
The easiest way to define orthogonal polynomials is by using Gram Schmidt on {X^n}_(n ∈ ℕ), but to do this I need to have a scalar product on ℝ[X], and I want to be able to change this scalar product in order to get different orthogonal polynomials families. So, what I have done right now, is defining MySpace s := ℝ[X], where s : IntegralScalarProduct, and instantiating InnerProductSpace on MySpace s. In this way, all the theorems take objects in MySpace s, and get access to the scalar product and its properties.
This somewhat works, but often have to do manual conversions between MySpace s and ℝ[X], which is extremely annoying. This wouldn't be a problem if I just instantiated InnerProductSpace on ℝ[X], but then I wouldn't know how to be flexible over the possible scalar products induced by different measures.

Is there a better way to put a user definable scalar product on ℝ[X}?

[Kevin Buzzard]

Make a local instance?

[giacomo gallina]

Thanks, I will try!

[Eric Wieser]

I think putting an inner product space on WithLp 2 (ι →₀ E) would be reasonable, and might help a bit here