# Finding the least positive integer satisfying a quantified statement

I'm studying the convergence of the sequence of functions $f_n:[0,1]\subset\mathbb{R}\to\mathbb{R}$ defined by $$f_n(x)=n^2x(1-x^2)^n$$ for $n\in\mathbb{N}$. These functions converge pointwise to the zero function $f(x)=0$.

Define the function $N(\epsilon,x):(0,\infty)\times[0,1]\to\mathbb{N}$ to be the smallest positive integer $N$ such that $$\forall m(m\in\mathbb{N}\land m\geq N\implies m^2x(1-x^2)^m<\epsilon)$$

Convergence and well-ordering guarantee this function is well-defined. Given $\epsilon$ and $x$, this function tells us how far out in the sequence $\left\{f_n(x)\right\}_1^\infty$ we must go in order to squeeze the remaining terms to within $\epsilon$ of $f(x)=0$. For fixed $\epsilon$, I know the dependence of $N$ on $x$ blows up as $x\to0^{+}$, but I thought it would be nice to see this explicitly.

Alas, while some values of this function are trivial to calculate, most aren't because of the mixture of polynomial and exponential dependence on $m$. Ideally I'd like to have Mathematica plot this function over $x\in[0,1]$ for fixed small $\epsilon$, say $\epsilon=1$ or $0.1$.

I can use Reduce to determine the set of all $n\in\mathbb{N}$ such that $n^2x(1-x^2)^n<\epsilon$ for fixed $x$ and $\epsilon$. For example, with $\epsilon=1$ and $x=0.2$, I use

Reduce[Element[n, Integers] && n^2 0.2 (1 - 0.2^2)^n < 1 && n > 0, {n}]


The output is

$n=1\lor n=2\lor(n\in\mathbb{Z}\land n\geq227)$

Using this, I deduce that $N(1,0.2)=227$, but I have two questions:

(1) I'm not sure how to code things to generate 227 directly (i.e. the value of my function $N(\epsilon,x)$ for fixed $\epsilon$ and $x$) without getting the entire solution set; all I want is the least integer that guarantees all larger integers are in the solution set, too.

(2) Nor do I know how to code things to handle variable (rather than fixed) $x$ and $\epsilon$. I'd be happy enough to fix $\epsilon$ and be able to plot $N(\epsilon,x)$ versus $x$.

• For the first question: ArgMin[{n, Reduce[ForAll[m, n < m && Element[n, Integers], m^2 0.2 (1 - 0.2^2)^m < 1 && m > 0], n]}, n] (* 227 *). – kirma Jun 22 '15 at 20:54
• @kirma: thanks. If you include this in an answer I can upvote it. Any thoughts on the second question? – symplectomorphic Jun 22 '15 at 20:55
• No ideas on the second question - my answer definitely doesn't help on that. – kirma Jun 22 '15 at 21:03

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.

• I like that this demonstrates how you can often directly translate a mathematical problem to Mathematica syntax. – J. M. will be back soon Jun 22 '15 at 23:32
• is there a reason you switched from using Reduce (in your comment on my OP) to Resolve (in your answer here)? – symplectomorphic Jun 23 '15 at 4:27
• @symplectomorphic It's mostly a matter of style. Documentation states: "Resolve[expr] attempts to resolve expr into a form that eliminates ForAll and Exists quantifiers." Also, "Resolve is in effect automatically applied by Reduce." We don't really need applying Reduce in this case to make constrained ArgMin happy, and with Resolve, we don't need to specify any variables. – kirma Jun 23 '15 at 4:34
• @kirma: for posterity, I figured out an answer to the second question, which was the obvious solution (but I'm a novice with Mathematica): g[x_] := ArgMin[{n, Reduce[ForAll[m, m >= n && Element[n, Integers], m^2 x (1 - x^2)^m < 1 && m > 0], n]}, n] – symplectomorphic Jun 23 '15 at 17:51
• @symplectomorphic Ah, you were asking that! I was thinking you would want to find less convoluted (like "closed-form") answers for the question. – kirma Jun 23 '15 at 18:02

One can use Mathematica to arrive at a symbolic expression for your function N. First, let's use Reduce on the boundary of your inequality:

soln = Reduce[m^2 x (1 - x^2)^m == ϵ , m]


(x == 1 && ϵ == 0 && Re[m] > 0) || (x == -1 && ϵ == 0 && Re[m] > 0) || (x == 0 && ϵ == 0) || (-1 + x^2 != 0 && ((ϵ == 0 && m == 0) || (Log[-(-1 + x) (1 + x)] != 0 && ϵ == 0 && m == 0))) || (C ∈ Integers && x != 0 && Log[-(-1 + x) (1 + x)] != 0 && (-1 + x^2) Sqrt[ϵ] Log[-(-1 + x) (1 + x)] != 0 && (m == ( 2 ProductLog[ C, -((Sqrt[ϵ] Log[-(-1 + x) (1 + x)])/(2 Sqrt[x]))])/ Log[-(-1 + x) (1 + x)] || m == (2 ProductLog[C, (Sqrt[ϵ] Log[-(-1 + x) (1 + x)])/( 2 Sqrt[x])])/Log[-(-1 + x) (1 + x)]))

Next, let's simplify while imposing constraints:

s = Simplify[soln, ϵ > 0 && 0 < x < 1 && C ∈ Integers]


m Log[1 - x^2] == 2 ProductLog[C, -(1/2) Sqrt[ϵ/x] Log[1 - x^2]] || m Log[1 - x^2] == 2 ProductLog[C, 1/2 Sqrt[ϵ/x] Log[1 - x^2]]

Finally, let's solve for m:

msol = m /. Solve[s, m]


{(2 ProductLog[C, -(1/2) Sqrt[ϵ/x] Log[1 - x^2]])/Log[1 - x^2], ( 2 ProductLog[C, 1/2 Sqrt[ϵ/x] Log[1 - x^2]])/Log[1 - x^2]}

Obviously we want m to be real, so let's find out when ProductLog returns a real value:

FunctionDomain[ProductLog[n, a], a]


(n == -1 && -(1/E) <= a < 0) || (n == 0 && a >= -(1/E))

This suggests that we are interested in the following:

n[ϵ_, x_] = Ceiling[msol[] /. C -> -1];


Let's see if this agrees with your example:

n[1, .2]


227

Visualization holding $\epsilon$ constant:

LogPlot[{n[.001, x], n[1, x]}, {x, 0, 1}] • Very cool; thanks for the extra insight on this old question. – symplectomorphic Mar 14 '18 at 2:07