Zulip Chat Archive

Stream: Is there code for X?

Topic: Hilbert space is isometric to its dual


view this post on Zulip Tomas Skrivan (Oct 26 2020 at 14:54):

Is somewhere in mathlib proven that the map v → ⟪v, ⬝ ⟫ is isometry between a Hilbert space and its dual?

view this post on Zulip Yury G. Kudryashov (Oct 26 2020 at 14:58):

There is a PR about this.

view this post on Zulip Yury G. Kudryashov (Oct 26 2020 at 14:58):

@Frédéric Dupuis :up:

view this post on Zulip Frédéric Dupuis (Oct 26 2020 at 15:55):

#4379, more precisely. It's currently waiting on how we're going to handle conjugate-linear maps. @Yury G. Kudryashov , are you planning to go ahead with the linear_map (f : R →+* S) E F idea that was discussed a few days ago?

view this post on Zulip Yury G. Kudryashov (Oct 26 2020 at 16:01):

I have a few refactors in line, and every time I switch branches I choose one of them and advance it a little:

  • bundle direction into affine_subspace;
  • review affine combinations by introducing the free affine space {f : α →₀ R | f.sum (λ a b, b) = 1};
  • redefine convexity for affine spaces;
  • use bundled homs for polynomial.eval etc;
  • glue mv_power_series to analytic maps;
  • redefine some free constructions using docs#con to get the universal property almost for free;
  • add smul_comm_class and migrate some parts of the library to it.

view this post on Zulip Yury G. Kudryashov (Oct 26 2020 at 16:03):

I guess, I'm not going to work on refactoring linear_maps for at least a week, so probably it's better to merge your PR without waiting for this refactor.

view this post on Zulip Heather Macbeth (Oct 26 2020 at 16:55):

I wonder whether it's worth refactoring #4379 (again! Sorry, Frédéric), so that it mostly does the real case, and does it in a way that will be directly generalizable to the conjugate-linear setting now that we have a theory for what that setting will look like.

view this post on Zulip Heather Macbeth (Oct 26 2020 at 16:56):

If this seems like a good idea, I can try this, since I don't want Frédéric to have to spend any more time on this.

view this post on Zulip Heather Macbeth (Oct 26 2020 at 16:57):

Maybe also get rid of the development of conjugate vector spaces, if we think that ultimately these will be treated in mathlib using smul_comm_class?

view this post on Zulip Frédéric Dupuis (Oct 26 2020 at 17:17):

Yeah, if we get conjugate-linear maps soon(ish) we definitely want this code to be based on that. I think the best thing to do would be to remove the conjugate semimodule code and merge it.

view this post on Zulip Heather Macbeth (Oct 26 2020 at 21:44):

@Frédéric Dupuis I would like to change your definition of the dual of a Hilbert space, so that the inner product is given by the polarization identity:

instance : has_inner 𝕜 (normed_space.dual 𝕜 E) :=
{ inner := λ x y, 4⁻¹ * ((𝓚 x + y) * (𝓚 x + y) - (𝓚 x - y) * (𝓚 x - y)
            + is_R_or_C.I * (𝓚 x + (@is_R_or_C.I 𝕜 _)  y) * (𝓚 x + (@is_R_or_C.I 𝕜 _)  y)
            - is_R_or_C.I * (𝓚 x - (@is_R_or_C.I 𝕜 _)  y) * (𝓚 x - (@is_R_or_C.I 𝕜 _)  y)) }

rather than copied over from the primal inner product by means of the equivalence:

instance : has_inner 𝕜 (normed_space.dual 𝕜 E) :=
{ inner := λ x y, to_primal y, to_primal x }

as you had written. The advantage is that the new definition works for inner product spaces without a completeness hypothesis. What do you think?

view this post on Zulip Heather Macbeth (Oct 26 2020 at 21:46):

This also would mean that the statement that "the mapping from E to its dual is an isometry" has content, rather than following by definition.

view this post on Zulip Frédéric Dupuis (Oct 26 2020 at 21:47):

That makes sense -- I hadn't thought about the completeness issue. I guess you'll have to prove the is_R_or_C polarization identity first though, only the real case is there now and I've been too lazy so far to generalize it :-)

view this post on Zulip Heather Macbeth (Oct 26 2020 at 21:48):

Yep, I am halfway there after a solid hour's work, it is not pleasant! :)

view this post on Zulip Frédéric Dupuis (Oct 26 2020 at 21:52):

I have no doubt -- that's why I haven't done it...!

view this post on Zulip Heather Macbeth (Oct 26 2020 at 21:58):

I was half-hoping that there were some mysteries of is_R_or_C which you would explain to me and which would improve things ....

view this post on Zulip Frédéric Dupuis (Oct 26 2020 at 22:01):

Not really -- it mostly just works like . So at least it shouldn't be any more annoying than proving the complex polarization identity directly.

view this post on Zulip Frédéric Dupuis (Oct 26 2020 at 22:03):

The one thing that is more annoying than is that coercions from reals have to be done manually, so norm_cast doesn't work.

view this post on Zulip Heather Macbeth (Oct 26 2020 at 22:06):

Yep, just figured that out half an hour ago :)

view this post on Zulip Heather Macbeth (Oct 26 2020 at 22:07):

(I wonder if it would be possible to get norm_cast working for is_R_or_C? Need to ask someone who knows about tactics.)

view this post on Zulip Frédéric Dupuis (Oct 26 2020 at 22:11):

I looked into it at the time, and I strongly suspect that the answer is no. We can't have proper coercions, because that causes a circular issue with the 𝕜=ℝ case, and norm_cast really needs coercions from what I could gather from the code. Maybe it's possible to create a specialized version of norm_cast where we replace the coercions by the manual one in is_R_or_C, but I'm afraid that's above my pay grade at the moment :-)

view this post on Zulip Heather Macbeth (Oct 26 2020 at 22:11):

I see, very interesting!

view this post on Zulip Yury G. Kudryashov (Oct 26 2020 at 23:11):

Does docs#has_lift_t work?

view this post on Zulip Yury G. Kudryashov (Oct 26 2020 at 23:12):

This is a coercion that requires an explicit up arrow.

view this post on Zulip Frédéric Dupuis (Oct 26 2020 at 23:50):

Hmm... maybe? It's worth looking into -- for some reason I've never run into these before.

view this post on Zulip Yury G. Kudryashov (Oct 27 2020 at 00:24):

It is (mis)used for coercion of a finset to a set.

view this post on Zulip Frédéric Dupuis (Oct 27 2020 at 01:30):

#check (show has_lift_t  , by apply_instance)

fails. Doesn't look good...

view this post on Zulip Yury G. Kudryashov (Oct 27 2020 at 02:06):

I think that you can define it and it'll work.

view this post on Zulip Frédéric Dupuis (Oct 27 2020 at 03:00):

instance : has_lift  K := of_real
#check (show has_lift_t  , by apply_instance)

This still fails -- I have no idea why...

view this post on Zulip Yury G. Kudryashov (Oct 27 2020 at 03:18):

#mwe?

view this post on Zulip Frédéric Dupuis (Oct 27 2020 at 03:54):

class is_R_or_C (K : Type*)  :=
(of_real :   K)

namespace is_R_or_C

variables {K : Type*} [is_R_or_C K]

instance : has_lift  K := of_real
#check (show has_lift_t  , by apply_instance)

end is_R_or_C

view this post on Zulip Mario Carneiro (Oct 27 2020 at 03:56):

the has_lift instance is not ok

view this post on Zulip Mario Carneiro (Oct 27 2020 at 03:56):

because it causes has_lift_t to loop

view this post on Zulip Frédéric Dupuis (Oct 27 2020 at 03:56):

OK, so basically the same reason we couldn't have the coercion either.

view this post on Zulip Frédéric Dupuis (Oct 27 2020 at 03:56):

That's a shame.

view this post on Zulip Mario Carneiro (Oct 27 2020 at 03:57):

you could make it a has_{coe|lift}_t instance

view this post on Zulip Frédéric Dupuis (Oct 27 2020 at 03:59):

Really? I'm pretty sure I tried making this a has_coe_t instance directly a while back and it failed.

view this post on Zulip Frédéric Dupuis (Oct 27 2020 at 04:02):

And if I recall correctly, it was you who convinced me I should give up and do coercions manually :-)

view this post on Zulip Frédéric Dupuis (Oct 27 2020 at 04:03):

Indeed it was: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/has_coe.20.E2.84.9D.20.E2.84.9D/near/207775998

view this post on Zulip Mario Carneiro (Oct 27 2020 at 04:05):

right... we don't have reflexive coe_t instances

view this post on Zulip Mario Carneiro (Oct 27 2020 at 04:07):

I think it should be possible to modify norm_cast to work with things other than coe

view this post on Zulip Yury G. Kudryashov (Oct 27 2020 at 04:07):

Are reflexive has_coe_t instances bad, or only has_coe?

view this post on Zulip Yury G. Kudryashov (Oct 27 2020 at 04:07):

A version of #mwe that works

class is_R_or_C (K : Type*)  :=
(of_real :   K)

namespace is_R_or_C

variables {K : Type*} [is_R_or_C K]

instance : has_lift  K := of_real
#check (show has_lift_t  , by apply_instance)

end is_R_or_C

view this post on Zulip Mario Carneiro (Oct 27 2020 at 04:08):

it looks identical to @Frédéric Dupuis 's

view this post on Zulip Heather Macbeth (Oct 27 2020 at 05:17):

Heather Macbeth said:

Yep, I am halfway there after a solid hour's work, it is not pleasant! :)

I posted a WIP PR, #4798, anyone in the mood for some algebra problems is welcome to take over some of the sorries!

view this post on Zulip Gabriel Ebner (Oct 27 2020 at 08:20):

This should really, really be has_coe_t or has_lift_t. Otherwise you get loops, as Mario's pointed out. This works:

import data.real.basic

class is_R_or_C (K : Type*)  :=
(of_real :   K)

instance : is_R_or_C  := id

namespace is_R_or_C

variables {K : Type*} [is_R_or_C K]

instance : has_coe_t  K := of_real

variable (x : )
#check (x : )
#check (coe x : )

end is_R_or_C

view this post on Zulip Ruben Van de Velde (Oct 27 2020 at 08:22):

I pushed a fix for the easiest sorry

view this post on Zulip Mario Carneiro (Oct 27 2020 at 08:25):

@Gabriel Ebner Should we add a general reflexive instance for has_lift_t and/or has_coe_t?

view this post on Zulip Gabriel Ebner (Oct 27 2020 at 08:27):

Like docs#coe_base?

view this post on Zulip Mario Carneiro (Oct 27 2020 at 08:28):

That's just the singleton case

view this post on Zulip Mario Carneiro (Oct 27 2020 at 08:28):

it implies that has_coe_t is the transitive closure of has_coe, but I am thinking about the reflexive transitive closure

view this post on Zulip Gabriel Ebner (Oct 27 2020 at 08:28):

Ah, I see.

view this post on Zulip Gabriel Ebner (Oct 27 2020 at 08:29):

Type class-wise, I don't think there would be any issues. Except for non-commuting diamonds.

view this post on Zulip Gabriel Ebner (Oct 27 2020 at 08:30):

But I don't think coercions should be used in this way. If you explicitly write (x : α), then you never need the reflexive instance.

view this post on Zulip Mario Carneiro (Oct 27 2020 at 08:31):

I agree, but the alternatives don't look great for Frederic's use case

view this post on Zulip Mario Carneiro (Oct 27 2020 at 08:32):

I don't think we will get non-commuting diamonds since f o id = f is definitional

view this post on Zulip Mario Carneiro (Oct 27 2020 at 08:32):

but it might be tricky to prove that all the time

view this post on Zulip Gabriel Ebner (Oct 27 2020 at 08:35):

We already have other reflexive instances (like nat.cast_coe). These would not be definitionally equal to the general one.

view this post on Zulip Gabriel Ebner (Oct 27 2020 at 08:36):

For Fréderic's use case we need a coercion for is_R_or_C anyhow, I'm not sure how a general reflexive instance helps here.

view this post on Zulip Mario Carneiro (Oct 27 2020 at 08:37):

well it would be weird if we had a reflexive instance only for real

view this post on Zulip Gabriel Ebner (Oct 27 2020 at 08:37):

Another (very realistic) option is to convince norm_cast that is_R_or_C.of_real is a coercion (it already knows about has_coe_to_fun, has_coe_to_sort; this is just one more function).

view this post on Zulip Mario Carneiro (Oct 27 2020 at 08:37):

That's my thought

view this post on Zulip Gabriel Ebner (Oct 27 2020 at 08:37):

Mario Carneiro said:

well it would be weird if we had a reflexive instance only for real

We also have it for nat, int, etc.

view this post on Zulip Gabriel Ebner (Oct 27 2020 at 08:39):

Personally, I think I'd prefer coercions over is_R_or_C.of_real.

view this post on Zulip Mario Carneiro (Oct 27 2020 at 08:40):

you've convinced me that [is_R_or_C K] : has_coe_t real K would be no better or worse than nat.has_coe

view this post on Zulip Mario Carneiro (Oct 27 2020 at 08:40):

it's a bit better, since the induced reflexive instance is definitional

view this post on Zulip Frédéric Dupuis (Oct 27 2020 at 13:41):

Well that's great news! I see there's a great docstring in data/nat/cast that gives the recipe...

view this post on Zulip Ruben Van de Velde (Oct 27 2020 at 15:24):

Did a few more - done for now, though

view this post on Zulip Heather Macbeth (Oct 27 2020 at 15:25):

Great!

view this post on Zulip Heather Macbeth (Oct 27 2020 at 15:27):

Regarding the casting: If I understand correctly, there are two proposals: to have a "conditional" coercion [is_R_or_C K] : has_coe_t real K, or to hard-code coercion-like behaviour into norm_cast. Would the second proposal mean that one only had improved behaviour when using norm_cast, whereas the first proposal would apply to any situation where one wants to use casts (in norm_cast or out)? If so, the first seems better.

view this post on Zulip Mario Carneiro (Oct 27 2020 at 15:28):

yes, that's right. In particular, the first option would let you use \u while the second requires some other notation

view this post on Zulip Heather Macbeth (Oct 27 2020 at 15:38):

And the first option would also let one cast like (3:K), right? (Which you can't currently do.)

view this post on Zulip Heather Macbeth (Oct 27 2020 at 16:08):

Or rather, I think you can do this (because 3 is a numeral), but you can't currently take an x of type and cast by saying (x:K). The change would permit that.

view this post on Zulip Frédéric Dupuis (Oct 27 2020 at 16:19):

Yes, I would much prefer the coercion as well.

view this post on Zulip Frédéric Dupuis (Oct 30 2020 at 00:58):

The coercion seems to work! See #4824

view this post on Zulip Frédéric Dupuis (Oct 30 2020 at 00:59):

@Heather Macbeth This PR might make the remaining sorries in #4798 a bit less painful :-)

view this post on Zulip Heather Macbeth (Oct 30 2020 at 01:25):

@Frédéric Dupuis Very cool!


Last updated: May 07 2021 at 21:10 UTC