Finding the least positive integer satisfying a quantified statement
For the first question: you can use ForAll
(as you used $\forall$!) also in Mathematica. Once you have acquired a region, you can minimize argument constrained on it:
ArgMin[{n,
Resolve[ForAll[m, m >= n && Element[n, Integers],
m^2 0.2 (1 - 0.2^2)^m < 1 && m > 0]]}, n]
227
If you take a hard look at the statement above, you may notice it's not exactly the same as the original question: it requires all real values of m
larger or equal to integer n
to satisfy the inequality, not just all integer values of m
... well, it seems Resolve
handles this well, but can't make the same reasoning when m
is constrained to integers.
I don't know an answer to the second question.