linear dependence of more than dimension

Stream: Is there code for X?

[Bhavik Mehta]

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?

[Johan Commelin]

What kind of statement would you like?

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Bhavik Mehta]

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

[Johan Commelin]

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

[Bhavik Mehta]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Bhavik Mehta]

Ah I see, thanks

[Johan Commelin]

Are you using [finite_dimensional K V]?

[Johan Commelin]

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

[Chris Hughes]

is_basis.le_span looks okay.

[Bhavik Mehta]

I'm in a finite dimensional space

[Johan Commelin]

docs#is_basis.le_span

[Bhavik Mehta]

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

[Chris Hughes]

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

[Bhavik Mehta]

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

[Chris Hughes]

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

[Reid Barton]

I would be inclined to use dim_le_injective plus something

[Chris Hughes]

I think it probably needs to be made into a lemma

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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?

[Johan Commelin]

I think the refactor into families was pretty painful

[Johan Commelin]

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

[Johan Commelin]

What we need is linear_independent.le_dim

[Johan Commelin]

Where is dim_span?

[Reid Barton]

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

[Johan Commelin]

Thanks!

[Reid Barton]

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

[Reid Barton]

oh maybe it's hiding elsewhere

[Reid Barton]

Interesting that noncomputable doesn't show up in the docs

[Johan Commelin]

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]

[Gabriel Ebner]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Yakov Pechersky]

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

[Yakov Pechersky]

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)

[Yakov Pechersky]

Like so?

[Anne Baanen]

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