162 reputation
7
bio website zelych.livejournal.com
location Moscow, Russia
age 32
visits member for 3 years
seen Sep 2 at 17:46

nothing special


Sep
1
comment Constructive proof of pigeonhole principle
Sorry for delay. I just completed the proof, you can see it here. It is still hairy and badly structured. I'll try to simplify it and then will post it here as a separate answer. Thanks again for the detailed explanation.
Aug
27
comment Constructive proof of pigeonhole principle
I succeeded formalizing everything except $(\forall f)(\forall k)(\forall m)[(\exists i < m)[f(i) = k] \lor \lnot (\exists i < m)[f(i) = k]]$. It is easy to prove it by classic axiom but I still trying to understand how to prove it by induction.
Aug
27
accepted Constructive proof of pigeonhole principle
Aug
27
comment Constructive proof of pigeonhole principle
I'll try to formalize this proof an then will accept your answer.
Aug
27
comment Constructive proof of pigeonhole principle
Thank you very much. The proof is really easy and straightforward, I even thought about applying inductive hypothesis to some new function but then got distracted and switched to googling for hints.
Aug
27
comment Constructive proof of pigeonhole principle
Yep, sorry. I added my definition (failed to TeXify it, but hope it is clear as it is).
Aug
27
revised Constructive proof of pigeonhole principle
added 216 characters in body
Aug
27
asked Constructive proof of pigeonhole principle
May
15
awarded  Caucus
Nov
27
comment Expected value of minimum distance
I need some time to understand this but accepting it for now. Thanks for answering.
Nov
27
accepted Expected value of minimum distance
Nov
27
comment Expected value of minimum distance
@Yury, Wow. Can you please post this as an answer with little more explanations?
Nov
27
comment Expected value of minimum distance
@Yury, I think we can assume only $n > m$ not $n >> m$. But if this somehow simplifies solution, you are welcome: solution to some similar problem is better than no solution at all.
Nov
27
comment Expected value of minimum distance
@mike, thanks. reading about order stats now, seems relevant.
Nov
27
comment Expected value of minimum distance
@Henry, yes integers are not necessarily distinct
Nov
27
comment Expected value of minimum distance
@Yury, closed form is preferable
Nov
26
awarded  Commentator
Nov
26
awarded  Editor
Nov
26
comment Expected value of minimum distance
@user1551, fixed, thanks for pointing.
Nov
26
revised Expected value of minimum distance
added 1 characters in body