Zulip Chat Archive

Stream: Is there code for X?

Topic: Identify span of vector with field


view this post on Zulip Heather Macbeth (Jun 08 2020 at 03:47):

I have some draft code for the topological dual of a normed space, including the corollary of Hahn-Banach needed for the isometric inclusion in the double dual. (Hopefully this is not stepping on @Yury G. Kudryashov 's toes.) For the Hahn-Banach corollary, I wrote out many, many facts which might well exist already, somewhere in the linear algebra libraries. Summary to follow. Any pointers?

view this post on Zulip Heather Macbeth (Jun 08 2020 at 03:47):

Summary: If E is a vector space over 𝕜 and x is a nonzero element, we can identify span x with 𝕜. Moreover, if E is a normed space, this identification preserves norms.

view this post on Zulip Heather Macbeth (Jun 08 2020 at 03:51):

I rolled-my-own span for now, because I could not find a library entry for the natural map from 𝕜 to span x.

view this post on Zulip Johan Commelin (Jun 08 2020 at 04:23):

Couldn't you reuse the existing span, but add the natural map?

view this post on Zulip Yury G. Kudryashov (Jun 08 2020 at 04:35):

derivs use linear_map.id.smul_right x for span_map. Possibly we should have a def for this.

view this post on Zulip Yury G. Kudryashov (Jun 08 2020 at 04:36):

Instead of using def span please add lemma span_map_range : range (span_map x) = span {x}.

view this post on Zulip Yury G. Kudryashov (Jun 08 2020 at 04:38):

I'm not going to formalize any corollaries of Hahn-Banach in the nearest future.

view this post on Zulip Heather Macbeth (Jun 08 2020 at 05:02):

Great, I will do this tomorrow. I will put span_map and friends in linear_algebra.basic, and perhaps the facts about the norm-preserving properties of span_map belong in normed_space.basic. Any opinions on conventionalizing the names? The maps needing baptism are span_map, its linear_equiv version (currently span_equiv), its inverse (currently coord), and its inverse considered as a bounded linear map (currently coord_bdd).

view this post on Zulip Yury G. Kudryashov (Jun 08 2020 at 05:03):

I have no ideas. @Sebastien Gouezel ?

view this post on Zulip Johan Commelin (Jun 08 2020 at 05:07):

It would be good if we could think of something that will also give the natural map for span {x,y}

view this post on Zulip Johan Commelin (Jun 08 2020 at 05:07):

But everything I can think of becomes ugly

view this post on Zulip Heather Macbeth (Jun 08 2020 at 05:08):

Yes, absolutely. Please tell me if you think of something! I will pick it up tomorrow.


Last updated: May 07 2021 at 22:14 UTC