Linear independence in Mathlib

Stream: mathlib4

[Martin Dvořák]

Has anybody written a review of how linear independence is defined in Mathlib?

Primarily, I would like to know what is the minimal subset of code such that, when I read given subset of code, I will know for sure that Mathlib's definition of linear independence corresponds to my intuition of what linear independence is.

[Filippo A. E. Nuccio]

What do you find unsatisfactory about the doc in the file?

[Martin Dvořák]

Well, the docs tell me what docs should tell me — how I can use it. It even tells me a few extra facts, for example, what inspired the design, which I appreciate.

What it doesn't tell me is which declarations I need to review in order to believe the correctness of the definition.
Hence I'm wondering if somebody else has already needed to review it before, so that I could copy the structure of the argument (with proper academic reference, of course) and just replace the code listings with the very version of Mathlib that I import.

[Kenny Lau]

what is your "intuition of what linear independence"? is it only for fields? comm rings? typically one first hears this term in the context of vector spaces over fields

[Martin Dvořák]

I first knew linear independence in the context of finitely-generated vector spaces over ℝ. Today, I understand linear independence in the context of a module over any semiring.

[Jireh Loreaux]

Does docs#linearIndependent_iff not satisfy you?

[Jireh Loreaux]

docs#linearIndependent_iffₛ is just the semiring variant, but it very nearly says the same thing.

[Martin Dvořák]

This is a good direction, thanks! Most of its prerequisites have been already reviewed in my thesis. If I use the suggested theorem to base my trust upon, I will only need to additionally review →₀ and Finsupp.linearCombination hopefully.

[Martin Dvořák]

I guess I like the version with 0 better.

[Kenny Lau]

a good example to think about is whether 1 : Int and -1 are linearly independent over Nat

[Jireh Loreaux]

Martin, if you want to avoid new declarations, just use docs#lienarIndependent_iff' instead.

[Martin Dvořák]

docs#linearIndependent_iff'

[Martin Dvořák]

Oh yeah, this refence is perfect!!

[Jireh Loreaux]

I'm just confused how you didn't manage to stumble on these yourself? What were you searching for / how were you searching that you didn't find them?

[Martin Dvořák]

Thanks a lot @Jireh Loreaux linearIndependent_iff' is perfect!

[Martin Dvořák]

I certainly knew the theorem when I was working on the code, but I forgor in the meanwhile, and now I am writing my thesis.

[Martin Dvořák]

I think I got it right now. Thanks a lot for help!
image.png

[Jireh Loreaux]

Martin, you say it's defined for a semiring, but give a condition which is only true for rings. Either reference the more general theorem, or simply say linear independence is defined for rings (assuming in your thesis you only ever care about rings).

[Jireh Loreaux]

If you want to be both precise and give the more specific condition, say "linear independence is defined for semirings ... and is equivalent to <reference linearIndependent_iff'ₛ>, and when the scalars are a ring, this can be reduced to the more familiar <reference linearIndependent_iff'>."

[Eric Wieser]

Perhaps also worth noting that linearIndependent_iffₛ is trivially true by definition (the definition is Function.Injective (Finsupp.linearCombination R v))

[Alfredo Moreira-Rosa]

Is there also a definition of multiplicative independence in mathlib ? Maybe named differently ?

[metakuntyyy]

@Martin Dvořák Cool, what thesis are you writing? Any chance we can read it once it's submitted?

[Martin Dvořák]

metakuntyyy said:

Martin Dvořák Cool, what thesis are you writing? Any chance we can read it once it's submitted?

Sure, you can absolutely read it once submitted!

[Martin Dvořák]

Pursuit of Truth and Beauty in Lean 4
Formally Verified Theory of Grammars, Optimization, Matroids

This thesis documents a voyage towards truth and beauty via formal verification of theorems. To this end, we develop libraries in Lean 4 that present definitions and results from diverse areas of MathematiCS. The aim is to create code that is understandable, believable, useful, and elegant. The code should stand for itself as much as possible without a need for documentation; however, this text redundantly documents our code artifacts and provides additional context that isn’t present in the code. This thesis is written for readers who know Lean 4 but are not familiar with any of the topics presented. We manifest truth and beauty in three formalized areas of MathematiCS.

We formalize general grammars in Lean 4 and use grammars to show closure of the class of type-0 languages under four operations: union, reversal, concatenation, and the Kleene star.

Our second stop is the theory of optimization. Farkas established that a system of linear inequalities has a solution if and only if we cannot obtain a contradiction by taking a linear combination of the inequalities. We state and formally prove several Farkas-like theorems over linearly ordered fields in Lean 4. Furthermore, we extend duality theory to the case when some coëfficients are allowed to take “infinite values”. Additionally, we develop the basics of the theory of optimization in terms of the framework called General-Valued Constraint Satisfaction Problems, and we prove that, if a Rational-Valued Constraint Satisfaction Problem template has symmetric fractional polymorphisms of all arities, then its Basic LP relaxation is tight.

Our third stop is matroid theory. Seymour's decomposition theorem is a hallmark result in matroid theory, presenting a structural characterization of the class of regular matroids. We aim to formally verify Seymour theorem in Lean 4. First, we build a library for working with totally unimodular matrices. We define binary matroids and their standard representations, and we prove that they form a matroid in the sense how Mathlib defines matroids. We define regular matroids to be matroids for which there exists a full representation rational matrix that is totally unimodular, and we prove that all regular matroids are binary. We define 1-sum, 2-sum and 3 sum of binary matroids as specific ways to compose their standard representation matrices. We prove that the 1-sum, the 2-sum and the 3-sum of regular matroids are a regular matroid, which concludes the composition direction of the Seymour's theorem. The (more difficult) decomposition direction remains unproved.

In the pursuit of truth, we focus on identifying the trusted code in each project and presenting it faithfully. We emphasize the readability and believability of definitions rather than choosing definitions that are easier to work with. The treatment of beauty is mostly situated within the philosophical framework of Roger Scruton, who emphasizes that beauty is not a mere decoration but, predominantly, beauty is the means for shaping our place in the world and a source of redemption, where beauty can be viewed as a substitute of religion.

[Martin Dvořák]

Alfredo Moreira-Rosa said:

Is there also a definition of multiplicative independence in mathlib ? Maybe named differently ?

I am pretty sure there isn't (if I understand correctly your question).

[Alfredo Moreira-Rosa]

yes something like

$$\prod_{i=1}^{n} x_i^{k_i} = 1 \implies \forall k_i, k_i = 0$$

[Alfredo Moreira-Rosa]

I have proof of this for primes $x_i\in \mathbb{P}$, and $k_i\in \N$ ,$\Z$ or $\mathbb{Q}$, would be nice if i could state it using a predefined multiplicative independence definition and get some other related lemmas for free.

[Aaron Liu]

probably state it using docs#Additive

[Martin Dvořák]

Actually more and more often I base my understanding of definitions on their API rather than on the definition itself. For example, I have just written what Disjoint means as follows:
image.png
I am not proud of not examining the definitions themselves, but currently it seems like a viable compromise.

[Kenny Lau]

Martin Dvořák said:

I am not proud of not examining the definitions themselves

that's the right thing to do! you should never have to unfold a definition