Zulip Chat Archive

Stream: Is there code for X?

Topic: linear dependence of more than dimension


view this post on Zulip Bhavik Mehta (Jun 03 2020 at 16:58):

If I have k vectors in a vector space with dimension <k, they're linearly dependent - what's the closest thing in mathlib to this?

view this post on Zulip Johan Commelin (Jun 03 2020 at 16:59):

What kind of statement would you like?

view this post on Zulip Johan Commelin (Jun 03 2020 at 17:00):

Some sort of lc that is nonzero, but whose sum evaluates to 0, via lc.total?

view this post on Zulip Johan Commelin (Jun 03 2020 at 17:00):

I haven't touched this part of the library since the refactor last year... so maybe everything is different now.

view this post on Zulip Johan Commelin (Jun 03 2020 at 17:01):

I think lc is maybe gone, but there is now finsupp.total?

view this post on Zulip Bhavik Mehta (Jun 03 2020 at 17:01):

I'd be happy with that, ¬ linear_independent R v would be fine too

view this post on Zulip Johan Commelin (Jun 03 2020 at 17:13):

I think this would work https://leanprover-community.github.io/mathlib_docs/linear_algebra/finsupp.html#finsupp.total

view this post on Zulip Bhavik Mehta (Jun 03 2020 at 17:15):

I don't see how to relate this to the dimension though

view this post on Zulip Johan Commelin (Jun 03 2020 at 17:15):

https://leanprover-community.github.io/mathlib_docs/linear_algebra/basis.html#exists_subset_is_basis

view this post on Zulip Johan Commelin (Jun 03 2020 at 17:15):

If your family is lin.indep, use :up: to extend it to a basis

view this post on Zulip Johan Commelin (Jun 03 2020 at 17:16):

After that, use the def of dimension to get a contradiction

view this post on Zulip Bhavik Mehta (Jun 03 2020 at 17:16):

Ah I see, thanks

view this post on Zulip Johan Commelin (Jun 03 2020 at 17:16):

Are you using [finite_dimensional K V]?

view this post on Zulip Johan Commelin (Jun 03 2020 at 17:17):

Or do you want to prove it using cardinals and infinite dimensional spaces?

view this post on Zulip Chris Hughes (Jun 03 2020 at 17:17):

is_basis.le_span looks okay.

view this post on Zulip Bhavik Mehta (Jun 03 2020 at 17:18):

I'm in a finite dimensional space

view this post on Zulip Johan Commelin (Jun 03 2020 at 17:18):

docs#is_basis.le_span

view this post on Zulip Bhavik Mehta (Jun 03 2020 at 17:20):

That looks harder than using the definition of dimension I think... (to me at least, before trying)

view this post on Zulip Chris Hughes (Jun 03 2020 at 17:25):

But there's actually a non trivial theorem here right? You need the fact that two bases have the same cardinality.

view this post on Zulip Bhavik Mehta (Jun 03 2020 at 17:26):

I don't think so, my new basis that Johan suggests to construct is bigger than the dimension, which contradicts the definition of dimension directly

view this post on Zulip Chris Hughes (Jun 03 2020 at 17:28):

The dimension is the cardinality of the smallest basis, so having one bigger isn't obviously a contradiction.

view this post on Zulip Reid Barton (Jun 03 2020 at 17:29):

I would be inclined to use dim_le_injective plus something

view this post on Zulip Chris Hughes (Jun 03 2020 at 17:30):

I think it probably needs to be made into a lemma

view this post on Zulip Reid Barton (Jun 03 2020 at 17:30):

linear_independent is already basically saying that the associated linear map is injective

view this post on Zulip Reid Barton (Jun 03 2020 at 17:30):

but maybe the API isn't quite in place for this

view this post on Zulip Reid Barton (Jun 03 2020 at 17:32):

Anyways yeah, there should be a lemma like dim_span with an inequality in the conclusion

view this post on Zulip Reid Barton (Jun 03 2020 at 17:32):

What's with dim_span anyways? Shouldn't it be a statement about cardinal.mk ι?

view this post on Zulip Reid Barton (Jun 03 2020 at 17:33):

I know they're the same, but if we went to the effort to use a family then it seems like we should talk about the cardinality of the family (i.e. the indexing set) and not the image of the family, right?

view this post on Zulip Johan Commelin (Jun 03 2020 at 17:34):

I think the refactor into families was pretty painful

view this post on Zulip Johan Commelin (Jun 03 2020 at 17:34):

So in some places they might have chosen to avoid extra refactor

view this post on Zulip Johan Commelin (Jun 03 2020 at 17:35):

What we need is linear_independent.le_dim

view this post on Zulip Johan Commelin (Jun 03 2020 at 17:35):

Where is dim_span?

view this post on Zulip Reid Barton (Jun 03 2020 at 17:35):

https://leanprover-community.github.io/mathlib_docs/linear_algebra/dimension.html#dim_span

view this post on Zulip Johan Commelin (Jun 03 2020 at 17:36):

Thanks!

view this post on Zulip Reid Barton (Jun 03 2020 at 17:42):

dim_finsupp (or better, dim_free once we have that language) also looks like a missing lemma

view this post on Zulip Reid Barton (Jun 03 2020 at 17:43):

oh maybe it's hiding elsewhere

view this post on Zulip Reid Barton (Jun 03 2020 at 17:44):

Interesting that noncomputable doesn't show up in the docs

view this post on Zulip Johan Commelin (Jun 03 2020 at 17:58):

Reid Barton said:

Interesting that noncomputable doesn't show up in the docs

@Rob Lewis :up:

We could typeset all the declarations that don't have the noncomputable tag in some faded gray... [/jk]

view this post on Zulip Gabriel Ebner (Jun 03 2020 at 18:06):

I vote for yellow-black danger stripes, these are surprisingly easy to do in CSS:
noncomputable_bg.png

view this post on Zulip Reid Barton (Jun 03 2020 at 18:07):

Upon reflection it's not quite noncomputable that I care about, but rather "naked choice"

view this post on Zulip Reid Barton (Jun 03 2020 at 18:07):

or arguably other bad things like equality at Type, though that's even harder to detect

view this post on Zulip Reid Barton (Jun 03 2020 at 18:07):

https://leanprover-community.github.io/mathlib_docs/linear_algebra/finsupp_vector_space.html#equiv_of_dim_eq_dim was the declaration that jumped out at me as odd

view this post on Zulip Yakov Pechersky (Sep 02 2020 at 19:54):

Similar to Bhavik's question, what's the proper way to state viRd,i=1,,N,viv_i \in \mathbb{R}^d, i = 1, \ldots, N, v_i linearly dependent?

view this post on Zulip Yakov Pechersky (Sep 02 2020 at 19:59):

import data.matrix.basic
import linear_algebra.basis
import linear_algebra.finite_dimensional
import data.real.basic

variables (N d : )

local notation `V` := (fin d  )
variables (v : fin N  V)

variables (lin_dep : ¬ linear_independent  v)

view this post on Zulip Yakov Pechersky (Sep 02 2020 at 19:59):

Like so?

view this post on Zulip Anne Baanen (Sep 03 2020 at 10:19):

That seems to be the canonical way, also used in docs#linear_dependent_iff


Last updated: May 07 2021 at 21:10 UTC