How to prove the closedness of the certain set

Stream: mathlib4

[Chenyi Li]

In my proof, I need to prove that the set $\{z | z = A x , x \geq 0\}$ is closed, where $A\in \mathbb{R}^{m \times n}$, $x \in \mathbb{R}^n$ , $z \in \mathbb{R}^m$, $x \geq 0$ denotes every element of $x$ is non-negative. It seems quite obvious, but I can't find some relevant theorems in mathlib4 til now. So how can I prove this? Thank you a lot for your help!

[Notification Bot]

Chenyi Li has marked this topic as resolved.

[Notification Bot]

Chenyi Li has marked this topic as unresolved.

[Kevin Buzzard]

What's the maths proof you'd like to formalise? "It seems quite obvious" isn't a proof.

[Ruben Van de Velde]

And have you stated the theorem in lean?

[Chenyi Li]

lemma matrix_set_close {m n p : ℕ} (B : Matrix (Fin n) (Fin m) ℝ) :
    IsClosed {z | ∃ t : (Fin m) → ℝ, t ≥ 0 ∧ z = B.mulVec t} := by
  sorry

I think this would be a corresponding statement for this natural language theorem.
Or equivalently, this would be the statement in the vector form which just decomposes the matrix into vectors

lemma polyhedra_is_closed {σ : Finset ℕ} : ∀ (b : ℕ → EuclideanSpace ℝ (Fin n)),
    IsClosed {z | ∃ (mu : σ → ℝ), (∀ i, 0 ≤ mu i) ∧ z =
    Finset.sum univ (fun i ↦ mu i • b i)} := by

[Chenyi Li]

Kevin Buzzard said:

What's the maths proof you'd like to formalise? "It seems quite obvious" isn't a proof.

Yes, exactly. What I am formalizing is a part of the proof for KKT conditions for constrained optimization problems. I follow the book Numerical Optimization. In this book, this statement is proved a little bit complicated. In my opinion, we may simplify the original proof.
proof.png

[Andrew Yang]

(deleted)

[Kevin Buzzard]

Is it true that a finitely-generated $\mathbb{R}_{\geq0}$-submodule of a finite-dimensional $\mathbb{R}$-vector space (with the Euclidean topology) is always closed? This would do it.

[Mitchell Lee]

Here is a way that you can not only prove your theorem, but also make some very useful contributions to mathlib.

I would start by defining the nonnegative span of a set of vectors (or more generally, a subset of a module over an ordered semiring). This is a pointed convex cone (docs#ConvexCone). This definition deserves a good API. Read through docs#Submodule.span and copy over as many lemmas as you can.

A convex cone is said to be finitely generated if it is the nonnegative span of a finite set of vectors. It should not be difficult to prove, if your API for the nonnegative span is good, that the image of a finitely generated cone under a linear map is finitely generated. Also, the orthant $\{x \in \mathbb{R}^n : x \geq 0\}$, denoted docs#ConvexCone.positive, is finitely generated. That means that the set you wish to prove is closed is a finitely generated cone.

The "fundamental theorem" of polyhedral geometry, of Minkowski and Weyl, is the following: in a finite dimensional vector space over an ordered field, a convex cone is finitely generated if and only if it is polyhedral (i.e. it is an intersection of finitely many half spaces). In other words: the dual of a finitely generated cone is finitely generated. This is an entirely algebraic fact and the proof should not use any topology whatsoever.

This implies that any finitely generated cone is closed.

[Mitchell Lee]

The proof of Minkowski–Weyl can be made entirely coordinate-free, if you're comfortable with dual spaces and quotients.

[Mitchell Lee]

As Kevin points out, a pointed convex cone is just a submodule over the subsemiring of nonnegative elements; this probably significantly decreases the number of new lemmas that need to be added

[Yaël Dillies]

Mitchell Lee said:

The "fundamental theorem" of polyhedral geometry, of Minkowski and Weyl, is the following: in a finite dimensional vector space over an ordered field, a convex cone is finitely generated if and only if it is polyhedral

This was formalised by @Hyeokjun Kwon. See https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Main.20Theorem.20of.20Polytope.20Theory

[Ruben Van de Velde]

Looking forward to seeing it in mathlib @Hyeokjun Kwon :innocent:

[Yaël Dillies]

Mitchell Lee said:

I would start by defining the nonnegative span of a set of vectors (or more generally, a subset of a module over an ordered semiring). This is a pointed convex cone (docs#ConvexCone). This definition deserves a good API. Read through docs#Submodule.span and copy over as many lemmas as you can.

Pretty sure @Apurva Nakade has got this

[Apurva Nakade]

One direct way to prove this is using the cone version of Caratheodory:
$\{ A x \: : \: x \ge 0 \} = \bigcup_i \{ A_i x \: : \: x \ge 0 \}$
where $A_i$ are the submatrices of $A$ formed using the linearly independent columns. Because $A_i$ are invertible, the right hand side is a finite union of closed cones and hence is closed.

I did not have time to work on my Caratheodory PR. The file with a complete proof is here. If anyone wants to take over this PR please feel free.

[Mitchell Lee]

Should a convex cone be redefined as a Submodule (Nonneg R) M so we get the closure operators and finitely generated predicate for free?

[Mitchell Lee]

(Or maybe it's important for a cone to not include 0 sometimes)

[Yaël Dillies]

That's exactly what docs#PointedCone is

[Mitchell Lee]

Ah, great

[Hyeokjun Kwon]

Ruben Van de Velde said:

Looking forward to seeing it in mathlib Hyeokjun Kwon :innocent:

Yeah, now that the exams are over and gotten some experience of making a PR to Mathlib, I will soon try to add the proof to the Mathlib bit by bit. Don't hold your breath though. (I still don't know my way around the Mathlib in terms of contributing to it)

[Ruben Van de Velde]

Don't hesitate to ask for help if needed!