# Zulip Chat Archive

## Stream: triage

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

#### 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?

#### 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?

#### 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.

#### 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

#### 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.

#### 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 `𝕜`

".

#### 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