PR #4798: feat(analysis/normed_space/dual): dual inner pr...

Stream: triage

[Random Issue Bot]

Today I chose PR 4798 for discussion!

feat(analysis/normed_space/dual): dual inner product space
Created by @None (@hrmacbeth) on 2020-10-27
Labels: WIP, merge-conflict

Is this PR still relevant? Any recent updates? Anyone making progress?

[Heather Macbeth]

The idea here was to put an inner product space structure on the dual of an inner product space, by
(1) proving that the dual norm satisfies the parallelogram law
(2) proving and then applying the Fréchet–von Neumann–Jordan theorm
Then I realised that I wasn't sure how to prove (1), so I'm not sure the construction works.

But the PR does contain about half of the proof of (2) (mostly written by @Ruben Van de Velde), and it would be useful to finish it off -- I don't have time, but it would be a fun task if someone wants a project. Should I change the title of the PR to "Fréchet–von Neumann–Jordan theorm" and delete the material about the dual space?

[Bryan Gin-ge Chen]

Dividing a stalled PR into smaller bits seems like a good way of moving things forward in general. Maybe the other idea can go in an issue, to be resolved if someone sees how to get it to work or that it can't work.

[Ruben Van de Velde]

The standard proof of smul_left seems to be by continuity; if someone knows of a direct proof / wants to give hints on how to make the continuity argument in lean, I could probably finish that part

[Frédéric Dupuis]

Another way to split this up would be to put the inner product space structure on the dual via the completion of the space instead of going via the parallelogram law.

[Frédéric Dupuis]

For the proof of smul_left, I think we would want to first prove an induction principle for is_R_or_C, saying something like "if a statement about a continuous function is true for (an appropriate subset of) 𝕜 with rational real and imaginary parts, then it is true for all 𝕜".

[Random Issue Bot]

Today I chose PR 4798 for discussion!

feat(analysis/normed_space/dual): dual inner product space
Created by @None (@hrmacbeth) on 2020-10-27
Labels: WIP, merge-conflict

Is this PR still relevant? Any recent updates? Anyone making progress?

[Random Issue Bot]

Today I chose PR 4798 for discussion!

feat(analysis/normed_space/dual): dual inner product space
Created by @Heather Macbeth (@hrmacbeth) on 2020-10-27
Labels: WIP, merge-conflict

Is this PR still relevant? Any recent updates? Anyone making progress?

[Ruben Van de Velde]

!3#4798 was delegated, but not to me. If someone wants to give it a push... :)