Saturday 25 July 2015

Formalizing problems

This is a TIL post. The problem was disguised as a simple inequality exercise in Norman L Biggs' Discrete Mathematics book.

So here's the deal:

Problem: Prove that in a square matrix, the least of the greatest valued members of each row is greater or equal to greatest of the least value members of a each column. (For convenience, I have assumed the matrix consists of only natural numbers)

Formalizing: 

With some help from math.stackexchange.com, I was able to formalize this as:

Prove that Miny(Maxxf(x,y)) >= Maxx(Minyf(x,y)) where f(x,y) is basically any value in the matrix and x and y refers to the row and column respectively.

Proof:

Let's break it down. From general definitions of Min and Max, we know that:
f(x,y) >= Min(f(x,y))
and
Max(x,y) >= f(x,y) - (I)

So, it simply boils down to proving the statement:
Maxxf(x, y) >= Minyf(x, y)

Let xo be a row at which the value Maxxf(x, y) is found. As a result, f(xo, y) would be the greatest possible value for any y  in the xo row - (II)

Let yo be a column at which the value Minyf(x, y) is found. As a result, f(x, yo) would be the lowest possible value for any x in the yo column. - (III)

From (II),
 f(xo, y) >= f(xo, yo)
And from (III),
f(xo, yo)>= f(x, yo)

What we just proved is that there exists a f(xo, yo) that belongs to N, such that
f(xo, y) >= f(xo, yo) and f(xo, yo)>= f(x, yo)

Hence, we can claim using axioms of inequality and natural numbers that:
 f(xo, y) >= f(x, yo)

or in other words,

Maxxf(x, y) >= Min y f(x, y)

which can further be extended to

Miny(Maxxf(x,y)) >= Maxx(Minyf(x,y))

using the reasoning in (I)

Summary

Although it took me a while to understand this problem, it took me much lesser time to identify the mental route to understanding this problem (commonly conveyed as "connecting the dots") once it was formalized and expressed as a statement. So the formalization process was worth it because, it helped me clearly understand the problem I was trying to solve. I have not quite been the fan of formal mathematical representation in the past, but I guess that just might change in the future :)

Another take-away realization from today: there is a lot of meaning in "break down problems before you try to solve them". This is just a simple example.