6 ms·

I like to think that I'm good at these combinatorics-kind of questions, but I can't wrap my head around this one. I can follow the construction of the matrix, b

by meuk 7y ago

I like to think that I'm good at these combinatorics-kind of questions, but I can't wrap my head around this one. I can follow the construction of the matrix, but I don't understand how you came up with the formula.

ocfnash 7y ago
I presume you've been looking at my presentation here http://olivernash.org/2019/07/06/coq-imo/index.html http://olivernash.org/2019/07/06/coq-imo/index.html which I confess is quite concise; apologies if it is too terse. Reusing the notation of my post, here's how the formula arises. The argument based on counting cells that are either row/column good/bad requires the following of the parameter k: 1. k-1 < r/m 2. k-1 < c/n 3. k−1 < cr/(c(m-1) + r(n-1)) These are equivalent to: 1. k <= ceil r m 2. k <= ceil c n 3. k <= ceil cr (c(m-1) + r(n-1)) And so it is sufficient to have: k <= min (ceil r m) (ceil c n) (ceil cr (c(m-1) + r(n-1))) We can then rearrange this to the headline formula by noting: * ceil r m = ceil (cr) (cm) * ceil c n = ceil (cr) (mr) And then simplifying by repeatedly using the fact that for any x, y, z: * min (ceil x y) (ceil x z) = ceil x (max y z) All this is of course in the Coq code. E.g., the last fact mentioned above is here: https://github.com/ocfnash/imo-coq/blob/f6d2e8337fadf00583fd09f86faf9cba62a25677/q3_2001/inequalities.v#L50 https://github.com/ocfnash/imo-coq/blob/f6d2e8337fadf00583fd...
- krapht 7y ago
  Related: https://imo-grand-challenge.github.io/ https://imo-grand-challenge.github.io/
  - ocfnash 7y ago
    Cool!
- meuk 7y ago
  Thanks. I just don't understand how you arrived at k <= ceil cr (c(m-1) + r(n-1)) The rest is clear.
  - ocfnash 7y ago
    Oh I see. Here's how I got there (still using the terminology / notation of my original post). Without knowing anything about k except that k-1 < r/m, I counted how many cells are column-bad for this value of k. By the pigeon-hole-principle argument in the post this is at most c(m-1)(k-1) cells. Similarly, and still knowing nothing about k except that k-1 < c/n, I count how many cells are row-bad for this value of k and see that it is at most r(n-1)(k-1). Combining these two I know that as long as we have k-1 < r/m and k-1 < c/n the number of cells that are either column-bad or row-bad (or both) is at most: * c(m-1)(k-1) + r(n-1)(k-1) Since I want to be able to conclude that there is a cell that is neither column-bad nor row-bad, and since there are rc cells in total, I then further require that k is such that: * c(m-1)(k-1) + r(n-1)(k-1) < rc (The point is that this is a strict inequality and so there must be a cell that is neither column-bad nor row-bad.) And then solve this to get the formula for k. Of course when expositing it in the post, I _start_ with the formula which perhaps makes things seem mysterious at first, but I thought was efficient.
    - meuk 7y ago
      Ah, it makes total sense now! Thanks for taking the time to explain your thought process to a random stranger on the internet ;) I'd say that the exposition in your post is very fitting for the purpose of proving it. The most elegant proofs are usually not the most enlightening.
      - ocfnash 7y ago
        You're welcome.

by meuk 7y ago

ocfnash 7y ago

I presume you've been looking at my presentation here http://olivernash.org/2019/07/06/coq-imo/index.html http://olivernash.org/2019/07/06/coq-imo/index.html which I confess is quite concise; apologies if it is too terse. Reusing the notation of my post, here's how the formula arises. The argument based on counting cells that are either row/column good/bad requires the following of the parameter k: 1. k-1 < r/m 2. k-1 < c/n 3. k−1 < cr/(c(m-1) + r(n-1)) These are equivalent to: 1. k <= ceil r m 2. k <= ceil c n 3. k <= ceil cr (c(m-1) + r(n-1)) And so it is sufficient to have: k <= min (ceil r m) (ceil c n) (ceil cr (c(m-1) + r(n-1))) We can then rearrange this to the headline formula by noting: * ceil r m = ceil (cr) (cm) * ceil c n = ceil (cr) (mr) And then simplifying by repeatedly using the fact that for any x, y, z: * min (ceil x y) (ceil x z) = ceil x (max y z) All this is of course in the Coq code. E.g., the last fact mentioned above is here: https://github.com/ocfnash/imo-coq/blob/f6d2e8337fadf00583fd09f86faf9cba62a25677/q3_2001/inequalities.v#L50 https://github.com/ocfnash/imo-coq/blob/f6d2e8337fadf00583fd...

krapht 7y ago
Related: https://imo-grand-challenge.github.io/ https://imo-grand-challenge.github.io/
- ocfnash 7y ago
  Cool!
meuk 7y ago
Thanks. I just don't understand how you arrived at k <= ceil cr (c(m-1) + r(n-1)) The rest is clear.
- ocfnash 7y ago
  Oh I see. Here's how I got there (still using the terminology / notation of my original post). Without knowing anything about k except that k-1 < r/m, I counted how many cells are column-bad for this value of k. By the pigeon-hole-principle argument in the post this is at most c(m-1)(k-1) cells. Similarly, and still knowing nothing about k except that k-1 < c/n, I count how many cells are row-bad for this value of k and see that it is at most r(n-1)(k-1). Combining these two I know that as long as we have k-1 < r/m and k-1 < c/n the number of cells that are either column-bad or row-bad (or both) is at most: * c(m-1)(k-1) + r(n-1)(k-1) Since I want to be able to conclude that there is a cell that is neither column-bad nor row-bad, and since there are rc cells in total, I then further require that k is such that: * c(m-1)(k-1) + r(n-1)(k-1) < rc (The point is that this is a strict inequality and so there must be a cell that is neither column-bad nor row-bad.) And then solve this to get the formula for k. Of course when expositing it in the post, I _start_ with the formula which perhaps makes things seem mysterious at first, but I thought was efficient.
  - meuk 7y ago
    Ah, it makes total sense now! Thanks for taking the time to explain your thought process to a random stranger on the internet ;) I'd say that the exposition in your post is very fitting for the purpose of proving it. The most elegant proofs are usually not the most enlightening.
    - ocfnash 7y ago
      You're welcome.