Zulip Chat Archive

Stream: new members

Topic: Finding entry of a matrix with "minimal euclidean valuation"


Jamie Reason (Aug 17 2022 at 12:38):

Hey, I'm trying to show there exists a non-zero element of a non-zero matrix with "minimal valuation" (in the sense of the euclidean valuation function). Lean seems to use an equivalence instead of a valuation where if δ was a valuation function, the relation (euclidean_domain.r) would have property a ≺ b ↔ δ(a) < δ(b).
The exact lemma I want to show is

lemma min_valuation_of_mat {D : Type*} [euclidean_domain D] {n : } (A : matrix (fin n) (fin n) D) (h : A  0) :
 (k l : fin n),  (i j : fin n), (A k l  0)  ( A i j  0  ¬((A i j)  (A k l)) ) := sorry

The pencil and paper proof would be that there must exist a non-zero element (but finitely many) so pick an arbitrary one a and it either has the property or another element exists b with a "smaller valuation", or with the relation that would be b ≺ a. Since finite number of entries, this must terminate.

Does anybody have any good places to start with this? I've tried using by_contra and push_neg but they seem to not progress it.

Notes: although I have not shown the following lemmas, assume they can be used (I believe they should all hold, let me know if you think they don't),

lemma lt_trans {D : Type*} [euclidean_domain D] :  {a b c : D}, (a  b)  (b  c)  (a  c) := λ a b c hab hbc, by sorry
lemma gt_not_eq_zero {D : Type*} [euclidean_domain D] :  {a b : D}, a  b  b  0 := λ a b, by sorry
lemma irrefl {D : Type*} [euclidean_domain D] :  {a : D}, ¬ (a  a) := λ a, by sorry
lemma asymm {D : Type*} [euclidean_domain D] :  {a b : D}, (a  b)  ¬(b  a) := λ a b hab, by sorry

(assumue in euclidean_domain namespace)

Junyan Xu (Aug 17 2022 at 14:46):

You may use dos#finset.filter to filter out the zero entries from finset.univ : finset (fin n × fin n), then you can just use docs#finset.min', and then finset.min'_le and finset.min'_mem give you its desired properties. You do need that the filtered finset is nonempty and that the order is linear. For general preorders, use docs#finset.exists_minimal.


Last updated: Dec 20 2023 at 11:08 UTC