Zulip Chat Archive

Stream: triage

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


view this post on Zulip Random Issue Bot (Jan 23 2021 at 14:43):

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?

view this post on Zulip Heather Macbeth (Jan 23 2021 at 16:35):

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?

view this post on Zulip Bryan Gin-ge Chen (Jan 23 2021 at 17:32):

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.

view this post on Zulip Ruben Van de Velde (Jan 23 2021 at 17:46):

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

view this post on Zulip Frédéric Dupuis (Jan 23 2021 at 18:32):

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.

view this post on Zulip Frédéric Dupuis (Jan 23 2021 at 18:36):

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 𝕜".

view this post on Zulip Random Issue Bot (Mar 21 2021 at 14:21):

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?


Last updated: May 09 2021 at 15:11 UTC