New folder analysis/inner_product_space

Stream: maths

[Heather Macbeth]

The file analysis.normed_space.inner_product is 2900 lines long, and now that conjugate-linear maps are in mathlib it's going to grow more. So I propose making a new folder analysis.inner_product_space.* and splitting the big file into several pieces. Here's a draft: branch#split-inner-product. Comments are welcome!

One benefit is that the main file defining inner product spaces no longer imports deriv and times_cont_diff. (Previously these were imported, for the sake of 200 lines about the derivative of the norm, etc., but now these are in a separate file from the definitions.)

I've done my best sorting out authorship of the split files but feel free to suggest people/contributions I've missed. I currently have:

• analysis.inner_product_space.basic: @Joe for #1248, @Sebastien Gouezel for #3060, @Frédéric Dupuis for #4057
• analysis.inner_product_space.calculus: @Yury G. Kudryashov for #5089, #5600, #6275
• analysis.inner_product_space.projection: @Joe for #1248, @Frédéric Dupuis for #4057, myself for a series of smaller PRs (#5408, #5474, #5543, #5558, #5734, #5876, #8884)

[Heather Macbeth]

I have a few TODOs if people like the main refactor:

• deduce continuity of the inner product directly rather than from differentiability (so it can live in basic rather than calculus)
• split analysis.normed_space.pi_Lp and analysis.normed_space.dual into normed-space and inner-product-space parts.

[Scott Morrison]

This is great! I agree splitting pi_Lp and dual later would be good, but you might just want to get this refactor through asap before conflicts start hitting it.

[Heather Macbeth]

Good point! OK, #9382.

[Heather Macbeth]

Second PR #9388 is now live, to split analysis.normed_space.pi_Lp and analysis.normed_space.dual. Everything was clearly the work of one person except the new analysis.inner_product_space.pi_L2, which I have credited to @Joseph Myers for #2852, @Sebastien Gouezel for #3060, and myself for #5949, #6877.