Skip to main content
correction
Source Link
Emil Jeřábek
  • 47.1k
  • 4
  • 147
  • 208

We can define Greg Martin's absolutely abnormal number in this language, based on Martin's paper as in the arxiv or the American Mathematical Monthly.

Our number which is abnormal in all bases is $\alpha=M(1)$, where we will define the function $$M(z) = \prod_{j=2}^\infty \left( 1-\frac{z^{2^j}}{d_j}\right)$$ using a sequence of $d$'s defined by $d_2=4$ and $$d_{j+1} = (j+1)^{d_j/j}$$ for $j\ge 2$. The $d$'s increase so super-exponentially that $M$ is an analytic function.

Before we can define $M$ we need some preliminaries. They are slightly tricky because we can not define a global function $x^k$, but can define it when $k$ is a natural number. Similarly, we can not define $j<k$ globally, but can define it when $j$ and $k$ are both natural numbers. \begin{align} z=e^y &:= \exists f [\partial f = f \wedge f \circ 0 = 1 \wedge f \circ y = z]\\ n\in Z &:= \forall y [e^y=1 \implies e^{ny}=1]\\ n\in N &:= \exists w,x,y,z [n=w^2+x^2+y^2+z^2 \wedge w,x,y,z\in Z]\\ j < k &:= \exists i[i,j,k\in N \wedge i+j+1=k]\\ Power(p,k) &:= \forall u[\partial u = 1 \implies u\partial p = kp \wedge p \circ 1 = 1]\\ y=x^k &:= \exists p[Power(p,k) \wedge y=p\circ x]\\ Legendre(q,n) &:= \forall u[\partial u = 1 \implies \partial((1-u^2)\partial q)+n(n+1)q=0]\\ Poly(p,k) &:= \forall n,q,v[k < n \wedge Legendre(q,n) \wedge \partial v = pq \implies v \circ (-1) = v \circ 1]\\ Coef(f,k,c) &:= \exists p,q,r [f=pq+r \wedge Power(p,k) \wedge q \circ 0 = c \wedge Poly(r,k-1)]\\ \end{align}\begin{align} z=e^y &:= \exists f [\partial f = f \wedge f \circ 0 = 1 \wedge f \circ y = z]\\ n\in Z &:= \forall y [e^y=1 \implies e^{ny}=1]\\ n\in N &:= \exists w,x,y,z [n=w^2+x^2+y^2+z^2 \wedge w,x,y,z\in Z]\\ j < k &:= \exists i[i,j,k\in N \wedge i+j+1=k]\\ Power(p,k) &:= \forall u[\partial u = 1 \land u\circ0=0 \implies u\partial p = kp \wedge p \circ 1 = 1]\\ y=x^k &:= \exists p[Power(p,k) \wedge y=p\circ x]\\ Legendre(q,n) &:= \forall u[\partial u = 1 \land u\circ0=0 \implies \partial((1-u^2)\partial q)+n(n+1)q=0]\\ Poly(p,k) &:= \forall n,q,v[k < n \wedge Legendre(q,n) \wedge \partial v = pq \implies v \circ (-1) = v \circ 1]\\ Coef(f,k,c) &:= \exists p,q,r [f=pq+r \wedge Power(p,k) \wedge q \circ 0 = c \wedge Poly(r,k-1)]\\ \end{align}

Now we will abbreviate $M_k$ for the $k$th coefficient in the power series expansion of $M$ at 0, i.e. the number such that $Coef(M,k,M_k)$. We will abbreviate $d_k$ for $-1/M_{2^k}$.

Then, finally, $\alpha$ is defined by \begin{align} \exists M[& M \circ 1=\alpha\\ &\wedge M_0=1 \wedge M_1=0 \wedge M_2=0 \wedge M_3=0 \wedge d_2=4\\ &\wedge \forall j[1<j\implies d_{j+1}^j=(j+1)^{d_j}]\\ &\wedge \forall j,k[j<2^k \implies M_{j+2^k} = M_j M_{2^k}]] \end{align}

The validity of these definitions uses several facts:

  • for $Power(p,k)$ and $Legendre(q,n)$, the fact that they solve standard differential equations;
  • for $Poly(p,k)$, the completeness of the Legendre polynomials;
  • for $M$, the fact that analytic functions are uniquely determined by their power series coefficients.

We can define Greg Martin's absolutely abnormal number in this language, based on Martin's paper as in the arxiv or the American Mathematical Monthly.

Our number which is abnormal in all bases is $\alpha=M(1)$, where we will define the function $$M(z) = \prod_{j=2}^\infty \left( 1-\frac{z^{2^j}}{d_j}\right)$$ using a sequence of $d$'s defined by $d_2=4$ and $$d_{j+1} = (j+1)^{d_j/j}$$ for $j\ge 2$. The $d$'s increase so super-exponentially that $M$ is an analytic function.

Before we can define $M$ we need some preliminaries. They are slightly tricky because we can not define a global function $x^k$, but can define it when $k$ is a natural number. Similarly, we can not define $j<k$ globally, but can define it when $j$ and $k$ are both natural numbers. \begin{align} z=e^y &:= \exists f [\partial f = f \wedge f \circ 0 = 1 \wedge f \circ y = z]\\ n\in Z &:= \forall y [e^y=1 \implies e^{ny}=1]\\ n\in N &:= \exists w,x,y,z [n=w^2+x^2+y^2+z^2 \wedge w,x,y,z\in Z]\\ j < k &:= \exists i[i,j,k\in N \wedge i+j+1=k]\\ Power(p,k) &:= \forall u[\partial u = 1 \implies u\partial p = kp \wedge p \circ 1 = 1]\\ y=x^k &:= \exists p[Power(p,k) \wedge y=p\circ x]\\ Legendre(q,n) &:= \forall u[\partial u = 1 \implies \partial((1-u^2)\partial q)+n(n+1)q=0]\\ Poly(p,k) &:= \forall n,q,v[k < n \wedge Legendre(q,n) \wedge \partial v = pq \implies v \circ (-1) = v \circ 1]\\ Coef(f,k,c) &:= \exists p,q,r [f=pq+r \wedge Power(p,k) \wedge q \circ 0 = c \wedge Poly(r,k-1)]\\ \end{align}

Now we will abbreviate $M_k$ for the $k$th coefficient in the power series expansion of $M$ at 0, i.e. the number such that $Coef(M,k,M_k)$. We will abbreviate $d_k$ for $-1/M_{2^k}$.

Then, finally, $\alpha$ is defined by \begin{align} \exists M[& M \circ 1=\alpha\\ &\wedge M_0=1 \wedge M_1=0 \wedge M_2=0 \wedge M_3=0 \wedge d_2=4\\ &\wedge \forall j[1<j\implies d_{j+1}^j=(j+1)^{d_j}]\\ &\wedge \forall j,k[j<2^k \implies M_{j+2^k} = M_j M_{2^k}]] \end{align}

The validity of these definitions uses several facts:

  • for $Power(p,k)$ and $Legendre(q,n)$, the fact that they solve standard differential equations;
  • for $Poly(p,k)$, the completeness of the Legendre polynomials;
  • for $M$, the fact that analytic functions are uniquely determined by their power series coefficients.

We can define Greg Martin's absolutely abnormal number in this language, based on Martin's paper as in the arxiv or the American Mathematical Monthly.

Our number which is abnormal in all bases is $\alpha=M(1)$, where we will define the function $$M(z) = \prod_{j=2}^\infty \left( 1-\frac{z^{2^j}}{d_j}\right)$$ using a sequence of $d$'s defined by $d_2=4$ and $$d_{j+1} = (j+1)^{d_j/j}$$ for $j\ge 2$. The $d$'s increase so super-exponentially that $M$ is an analytic function.

Before we can define $M$ we need some preliminaries. They are slightly tricky because we can not define a global function $x^k$, but can define it when $k$ is a natural number. Similarly, we can not define $j<k$ globally, but can define it when $j$ and $k$ are both natural numbers. \begin{align} z=e^y &:= \exists f [\partial f = f \wedge f \circ 0 = 1 \wedge f \circ y = z]\\ n\in Z &:= \forall y [e^y=1 \implies e^{ny}=1]\\ n\in N &:= \exists w,x,y,z [n=w^2+x^2+y^2+z^2 \wedge w,x,y,z\in Z]\\ j < k &:= \exists i[i,j,k\in N \wedge i+j+1=k]\\ Power(p,k) &:= \forall u[\partial u = 1 \land u\circ0=0 \implies u\partial p = kp \wedge p \circ 1 = 1]\\ y=x^k &:= \exists p[Power(p,k) \wedge y=p\circ x]\\ Legendre(q,n) &:= \forall u[\partial u = 1 \land u\circ0=0 \implies \partial((1-u^2)\partial q)+n(n+1)q=0]\\ Poly(p,k) &:= \forall n,q,v[k < n \wedge Legendre(q,n) \wedge \partial v = pq \implies v \circ (-1) = v \circ 1]\\ Coef(f,k,c) &:= \exists p,q,r [f=pq+r \wedge Power(p,k) \wedge q \circ 0 = c \wedge Poly(r,k-1)]\\ \end{align}

Now we will abbreviate $M_k$ for the $k$th coefficient in the power series expansion of $M$ at 0, i.e. the number such that $Coef(M,k,M_k)$. We will abbreviate $d_k$ for $-1/M_{2^k}$.

Then, finally, $\alpha$ is defined by \begin{align} \exists M[& M \circ 1=\alpha\\ &\wedge M_0=1 \wedge M_1=0 \wedge M_2=0 \wedge M_3=0 \wedge d_2=4\\ &\wedge \forall j[1<j\implies d_{j+1}^j=(j+1)^{d_j}]\\ &\wedge \forall j,k[j<2^k \implies M_{j+2^k} = M_j M_{2^k}]] \end{align}

The validity of these definitions uses several facts:

  • for $Power(p,k)$ and $Legendre(q,n)$, the fact that they solve standard differential equations;
  • for $Poly(p,k)$, the completeness of the Legendre polynomials;
  • for $M$, the fact that analytic functions are uniquely determined by their power series coefficients.
Added link to AMM paper
Source Link
LSpice
  • 12.9k
  • 4
  • 45
  • 69

We can define Greg Martin's absolutely abnormal number in this language, based on Martin's paper as in the arxiv or the American Mathematical MonthlyAmerican Mathematical Monthly.

Our number which is abnormal in all bases is $\alpha=M(1)$, where we will define the function $$M(z) = \prod_{j=2}^\infty \left( 1-\frac{z^{2^j}}{d_j}\right)$$ using a sequence of $d$'s defined by $d_2=4$ and $$d_{j+1} = (j+1)^{d_j/j}$$ for $j\ge 2$. The $d$'s increase so super-exponentially that $M$ is an analytic function.

Before we can define $M$ we need some preliminaries. They are slightly tricky because we can not define a global function $x^k$, but can define it when $k$ is a natural number. Similarly, we can not define $j<k$ globally, but can define it when $j$ and $k$ are both natural numbers. \begin{align} z=e^y &:= \exists f [\partial f = f \wedge f \circ 0 = 1 \wedge f \circ y = z]\\ n\in Z &:= \forall y [e^y=1 \implies e^{ny}=1]\\ n\in N &:= \exists w,x,y,z [n=w^2+x^2+y^2+z^2 \wedge w,x,y,z\in Z]\\ j < k &:= \exists i[i,j,k\in N \wedge i+j+1=k]\\ Power(p,k) &:= \forall u[\partial u = 1 \implies u\partial p = kp \wedge p \circ 1 = 1]\\ y=x^k &:= \exists p[Power(p,k) \wedge y=p\circ x]\\ Legendre(q,n) &:= \forall u[\partial u = 1 \implies \partial((1-u^2)\partial q)+n(n+1)q=0]\\ Poly(p,k) &:= \forall n,q,v[k < n \wedge Legendre(q,n) \wedge \partial v = pq \implies v \circ (-1) = v \circ 1]\\ Coef(f,k,c) &:= \exists p,q,r [f=pq+r \wedge Power(p,k) \wedge q \circ 0 = c \wedge Poly(r,k-1)]\\ \end{align}

Now we will abbreviate $M_k$ for the $k$th coefficient in the power series expansion of $M$ at 0, i.e. the number such that $Coef(M,k,M_k)$. We will abbreviate $d_k$ for $-1/M_{2^k}$.

Then, finally, $\alpha$ is defined by \begin{align} \exists M[& M \circ 1=\alpha\\ &\wedge M_0=1 \wedge M_1=0 \wedge M_2=0 \wedge M_3=0 \wedge d_2=4\\ &\wedge \forall j[1<j\implies d_{j+1}^j=(j+1)^{d_j}]\\ &\wedge \forall j,k[j<2^k \implies M_{j+2^k} = M_j M_{2^k}]] \end{align}

The validity of these definitions uses several facts:

  • for $Power(p,k)$ and $Legendre(q,n)$, the fact that they solve standard differential equations;
  • for $Poly(p,k)$, the completeness of the Legendre polynomials;
  • for $M$, the fact that analytic functions are uniquely determined by their power series coefficients.

We can define Greg Martin's absolutely abnormal number in this language, based on Martin's paper as in the arxiv or the American Mathematical Monthly.

Our number which is abnormal in all bases is $\alpha=M(1)$, where we will define the function $$M(z) = \prod_{j=2}^\infty \left( 1-\frac{z^{2^j}}{d_j}\right)$$ using a sequence of $d$'s defined by $d_2=4$ and $$d_{j+1} = (j+1)^{d_j/j}$$ for $j\ge 2$. The $d$'s increase so super-exponentially that $M$ is an analytic function.

Before we can define $M$ we need some preliminaries. They are slightly tricky because we can not define a global function $x^k$, but can define it when $k$ is a natural number. Similarly, we can not define $j<k$ globally, but can define it when $j$ and $k$ are both natural numbers. \begin{align} z=e^y &:= \exists f [\partial f = f \wedge f \circ 0 = 1 \wedge f \circ y = z]\\ n\in Z &:= \forall y [e^y=1 \implies e^{ny}=1]\\ n\in N &:= \exists w,x,y,z [n=w^2+x^2+y^2+z^2 \wedge w,x,y,z\in Z]\\ j < k &:= \exists i[i,j,k\in N \wedge i+j+1=k]\\ Power(p,k) &:= \forall u[\partial u = 1 \implies u\partial p = kp \wedge p \circ 1 = 1]\\ y=x^k &:= \exists p[Power(p,k) \wedge y=p\circ x]\\ Legendre(q,n) &:= \forall u[\partial u = 1 \implies \partial((1-u^2)\partial q)+n(n+1)q=0]\\ Poly(p,k) &:= \forall n,q,v[k < n \wedge Legendre(q,n) \wedge \partial v = pq \implies v \circ (-1) = v \circ 1]\\ Coef(f,k,c) &:= \exists p,q,r [f=pq+r \wedge Power(p,k) \wedge q \circ 0 = c \wedge Poly(r,k-1)]\\ \end{align}

Now we will abbreviate $M_k$ for the $k$th coefficient in the power series expansion of $M$ at 0, i.e. the number such that $Coef(M,k,M_k)$. We will abbreviate $d_k$ for $-1/M_{2^k}$.

Then, finally, $\alpha$ is defined by \begin{align} \exists M[& M \circ 1=\alpha\\ &\wedge M_0=1 \wedge M_1=0 \wedge M_2=0 \wedge M_3=0 \wedge d_2=4\\ &\wedge \forall j[1<j\implies d_{j+1}^j=(j+1)^{d_j}]\\ &\wedge \forall j,k[j<2^k \implies M_{j+2^k} = M_j M_{2^k}]] \end{align}

The validity of these definitions uses several facts:

  • for $Power(p,k)$ and $Legendre(q,n)$, the fact that they solve standard differential equations;
  • for $Poly(p,k)$, the completeness of the Legendre polynomials;
  • for $M$, the fact that analytic functions are uniquely determined by their power series coefficients.

We can define Greg Martin's absolutely abnormal number in this language, based on Martin's paper as in the arxiv or the American Mathematical Monthly.

Our number which is abnormal in all bases is $\alpha=M(1)$, where we will define the function $$M(z) = \prod_{j=2}^\infty \left( 1-\frac{z^{2^j}}{d_j}\right)$$ using a sequence of $d$'s defined by $d_2=4$ and $$d_{j+1} = (j+1)^{d_j/j}$$ for $j\ge 2$. The $d$'s increase so super-exponentially that $M$ is an analytic function.

Before we can define $M$ we need some preliminaries. They are slightly tricky because we can not define a global function $x^k$, but can define it when $k$ is a natural number. Similarly, we can not define $j<k$ globally, but can define it when $j$ and $k$ are both natural numbers. \begin{align} z=e^y &:= \exists f [\partial f = f \wedge f \circ 0 = 1 \wedge f \circ y = z]\\ n\in Z &:= \forall y [e^y=1 \implies e^{ny}=1]\\ n\in N &:= \exists w,x,y,z [n=w^2+x^2+y^2+z^2 \wedge w,x,y,z\in Z]\\ j < k &:= \exists i[i,j,k\in N \wedge i+j+1=k]\\ Power(p,k) &:= \forall u[\partial u = 1 \implies u\partial p = kp \wedge p \circ 1 = 1]\\ y=x^k &:= \exists p[Power(p,k) \wedge y=p\circ x]\\ Legendre(q,n) &:= \forall u[\partial u = 1 \implies \partial((1-u^2)\partial q)+n(n+1)q=0]\\ Poly(p,k) &:= \forall n,q,v[k < n \wedge Legendre(q,n) \wedge \partial v = pq \implies v \circ (-1) = v \circ 1]\\ Coef(f,k,c) &:= \exists p,q,r [f=pq+r \wedge Power(p,k) \wedge q \circ 0 = c \wedge Poly(r,k-1)]\\ \end{align}

Now we will abbreviate $M_k$ for the $k$th coefficient in the power series expansion of $M$ at 0, i.e. the number such that $Coef(M,k,M_k)$. We will abbreviate $d_k$ for $-1/M_{2^k}$.

Then, finally, $\alpha$ is defined by \begin{align} \exists M[& M \circ 1=\alpha\\ &\wedge M_0=1 \wedge M_1=0 \wedge M_2=0 \wedge M_3=0 \wedge d_2=4\\ &\wedge \forall j[1<j\implies d_{j+1}^j=(j+1)^{d_j}]\\ &\wedge \forall j,k[j<2^k \implies M_{j+2^k} = M_j M_{2^k}]] \end{align}

The validity of these definitions uses several facts:

  • for $Power(p,k)$ and $Legendre(q,n)$, the fact that they solve standard differential equations;
  • for $Poly(p,k)$, the completeness of the Legendre polynomials;
  • for $M$, the fact that analytic functions are uniquely determined by their power series coefficients.
cleaned by removing duplicative definition of 2^k, simplifying definition of Power, replacing <= and > with <
Source Link
user44143
user44143

We can define Greg Martin's absolutely abnormal number in this language, based on Martin's paper as in the arxiv or the American Mathematical Monthly.

Our number which is abnormal in all bases is $\alpha=M(1)$, where we will define the function $$M(z) = \prod_{j=2}^\infty \left( 1-\frac{z^{2^j}}{d_j}\right)$$ using a sequence of $d$'s defined by $d_2=4$ and $$d_{j+1} = (j+1)^{d_j/j}$$ for $j\ge 2$. The $d$'s increase so super-exponentially that $M$ is an analytic function.

Before we can define $M$ we need some preliminaries. They are slightly tricky because we can not define a global function $x^y$$x^k$, but can define it when $x$ or $y$$k$ is a natural number. Similarly, we can not define $x<y$$j<k$ globally, but can define it when $x$$j$ and $y$$k$ are both natural numbers. \begin{align} z=e^y &:= \exists f [\partial f = f \wedge f \circ 0 = 1 \wedge f \circ y = z]\\ z=2^y &:= \exists x [2=e^x \wedge z=e^{xy}]\\ n\in Z &:= \forall y [e^y=1 \implies e^{ny}=1]\\ n\in N &:= \exists w,x,y,z [n=w^2+x^2+y^2+z^2 \wedge w,x,y,z\in Z]\\ j < k &:= \exists i[i,j,k\in N \wedge i+j+1=k]\\ Power(p,k) &:= \forall n[n \in Z \implies p \circ e^n=e^{kn}]\\ y=x^k &:= \exists p[Power(p,k) \wedge y=p\circ x]\\ Legendre(q,n) &:= \forall u[\partial u = 1 \implies \partial((1-u^2)\partial q)+n(n+1)q=0]\\ Poly(p,k) &:= \forall n,q,v[n \ge k \wedge Legendre(q,n) \wedge \partial v = pq \implies v \circ (-1) = v \circ 1]\\ Coef(f,k,c) &:= \exists p,q,r [f=pq+r \wedge Power(p,k) \wedge q \circ 0 = c \wedge Poly(r,k)]\\ \end{align}\begin{align} z=e^y &:= \exists f [\partial f = f \wedge f \circ 0 = 1 \wedge f \circ y = z]\\ n\in Z &:= \forall y [e^y=1 \implies e^{ny}=1]\\ n\in N &:= \exists w,x,y,z [n=w^2+x^2+y^2+z^2 \wedge w,x,y,z\in Z]\\ j < k &:= \exists i[i,j,k\in N \wedge i+j+1=k]\\ Power(p,k) &:= \forall u[\partial u = 1 \implies u\partial p = kp \wedge p \circ 1 = 1]\\ y=x^k &:= \exists p[Power(p,k) \wedge y=p\circ x]\\ Legendre(q,n) &:= \forall u[\partial u = 1 \implies \partial((1-u^2)\partial q)+n(n+1)q=0]\\ Poly(p,k) &:= \forall n,q,v[k < n \wedge Legendre(q,n) \wedge \partial v = pq \implies v \circ (-1) = v \circ 1]\\ Coef(f,k,c) &:= \exists p,q,r [f=pq+r \wedge Power(p,k) \wedge q \circ 0 = c \wedge Poly(r,k-1)]\\ \end{align}

Now we will abbreviate $M_k$ for the $k$th coefficient in the power series expansion of $M$ at 0, i.e. the number such that $Coef(M,k,M_k)$. We will abbreviate $d_k$ for $-1/M_{2^k}$.

Then, finally, $\alpha$ is defined by \begin{align} \exists M[& M \circ 1=\alpha\\ &\wedge M_0=1 \wedge M_1=0 \wedge M_2=0 \wedge M_3=0 \wedge d_2=4\\ &\wedge \forall j[(j-2\in N)\implies d_{j+1}^j=(j+1)^{d_j}]\\ &\wedge \forall j,k[j<2^k \implies M_{j+2^k} = M_j M_{2^k}]] \end{align}\begin{align} \exists M[& M \circ 1=\alpha\\ &\wedge M_0=1 \wedge M_1=0 \wedge M_2=0 \wedge M_3=0 \wedge d_2=4\\ &\wedge \forall j[1<j\implies d_{j+1}^j=(j+1)^{d_j}]\\ &\wedge \forall j,k[j<2^k \implies M_{j+2^k} = M_j M_{2^k}]] \end{align}

The validity of these definitions uses several facts:

  • for $Power(p,k)$ and $Legendre(q,n)$, the fact that analytic functions are uniquely determined by their values on sequences which have 0 as an accumulation point;they solve standard differential equations;
  • for $Poly(p,k)$, the completeness of the Legendre polynomials;
  • for $M$, the fact that analytic functions are uniquely determined by their power series coefficients.

We can define Greg Martin's absolutely abnormal number in this language, based on Martin's paper as in the arxiv or the American Mathematical Monthly.

Our number which is abnormal in all bases is $\alpha=M(1)$, where we will define the function $$M(z) = \prod_{j=2}^\infty \left( 1-\frac{z^{2^j}}{d_j}\right)$$ using a sequence of $d$'s defined by $d_2=4$ and $$d_{j+1} = (j+1)^{d_j/j}$$ for $j\ge 2$. The $d$'s increase so super-exponentially that $M$ is an analytic function.

Before we can define $M$ we need some preliminaries. They are slightly tricky because we can not define a global function $x^y$, but can define it when $x$ or $y$ is a natural number. Similarly, we can not define $x<y$ globally, but can define it when $x$ and $y$ are both natural numbers. \begin{align} z=e^y &:= \exists f [\partial f = f \wedge f \circ 0 = 1 \wedge f \circ y = z]\\ z=2^y &:= \exists x [2=e^x \wedge z=e^{xy}]\\ n\in Z &:= \forall y [e^y=1 \implies e^{ny}=1]\\ n\in N &:= \exists w,x,y,z [n=w^2+x^2+y^2+z^2 \wedge w,x,y,z\in Z]\\ j < k &:= \exists i[i,j,k\in N \wedge i+j+1=k]\\ Power(p,k) &:= \forall n[n \in Z \implies p \circ e^n=e^{kn}]\\ y=x^k &:= \exists p[Power(p,k) \wedge y=p\circ x]\\ Legendre(q,n) &:= \forall u[\partial u = 1 \implies \partial((1-u^2)\partial q)+n(n+1)q=0]\\ Poly(p,k) &:= \forall n,q,v[n \ge k \wedge Legendre(q,n) \wedge \partial v = pq \implies v \circ (-1) = v \circ 1]\\ Coef(f,k,c) &:= \exists p,q,r [f=pq+r \wedge Power(p,k) \wedge q \circ 0 = c \wedge Poly(r,k)]\\ \end{align}

Now we will abbreviate $M_k$ for the $k$th coefficient in the power series expansion of $M$ at 0, i.e. the number such that $Coef(M,k,M_k)$. We will abbreviate $d_k$ for $-1/M_{2^k}$.

Then, finally, $\alpha$ is defined by \begin{align} \exists M[& M \circ 1=\alpha\\ &\wedge M_0=1 \wedge M_1=0 \wedge M_2=0 \wedge M_3=0 \wedge d_2=4\\ &\wedge \forall j[(j-2\in N)\implies d_{j+1}^j=(j+1)^{d_j}]\\ &\wedge \forall j,k[j<2^k \implies M_{j+2^k} = M_j M_{2^k}]] \end{align}

The validity of these definitions uses several facts:

  • for $Power(p,k)$, the fact that analytic functions are uniquely determined by their values on sequences which have 0 as an accumulation point;
  • for $Poly(p,k)$, the completeness of the Legendre polynomials;
  • for $M$, the fact that analytic functions are uniquely determined by their power series coefficients.

We can define Greg Martin's absolutely abnormal number in this language, based on Martin's paper as in the arxiv or the American Mathematical Monthly.

Our number which is abnormal in all bases is $\alpha=M(1)$, where we will define the function $$M(z) = \prod_{j=2}^\infty \left( 1-\frac{z^{2^j}}{d_j}\right)$$ using a sequence of $d$'s defined by $d_2=4$ and $$d_{j+1} = (j+1)^{d_j/j}$$ for $j\ge 2$. The $d$'s increase so super-exponentially that $M$ is an analytic function.

Before we can define $M$ we need some preliminaries. They are slightly tricky because we can not define a global function $x^k$, but can define it when $k$ is a natural number. Similarly, we can not define $j<k$ globally, but can define it when $j$ and $k$ are both natural numbers. \begin{align} z=e^y &:= \exists f [\partial f = f \wedge f \circ 0 = 1 \wedge f \circ y = z]\\ n\in Z &:= \forall y [e^y=1 \implies e^{ny}=1]\\ n\in N &:= \exists w,x,y,z [n=w^2+x^2+y^2+z^2 \wedge w,x,y,z\in Z]\\ j < k &:= \exists i[i,j,k\in N \wedge i+j+1=k]\\ Power(p,k) &:= \forall u[\partial u = 1 \implies u\partial p = kp \wedge p \circ 1 = 1]\\ y=x^k &:= \exists p[Power(p,k) \wedge y=p\circ x]\\ Legendre(q,n) &:= \forall u[\partial u = 1 \implies \partial((1-u^2)\partial q)+n(n+1)q=0]\\ Poly(p,k) &:= \forall n,q,v[k < n \wedge Legendre(q,n) \wedge \partial v = pq \implies v \circ (-1) = v \circ 1]\\ Coef(f,k,c) &:= \exists p,q,r [f=pq+r \wedge Power(p,k) \wedge q \circ 0 = c \wedge Poly(r,k-1)]\\ \end{align}

Now we will abbreviate $M_k$ for the $k$th coefficient in the power series expansion of $M$ at 0, i.e. the number such that $Coef(M,k,M_k)$. We will abbreviate $d_k$ for $-1/M_{2^k}$.

Then, finally, $\alpha$ is defined by \begin{align} \exists M[& M \circ 1=\alpha\\ &\wedge M_0=1 \wedge M_1=0 \wedge M_2=0 \wedge M_3=0 \wedge d_2=4\\ &\wedge \forall j[1<j\implies d_{j+1}^j=(j+1)^{d_j}]\\ &\wedge \forall j,k[j<2^k \implies M_{j+2^k} = M_j M_{2^k}]] \end{align}

The validity of these definitions uses several facts:

  • for $Power(p,k)$ and $Legendre(q,n)$, the fact that they solve standard differential equations;
  • for $Poly(p,k)$, the completeness of the Legendre polynomials;
  • for $M$, the fact that analytic functions are uniquely determined by their power series coefficients.
defined polynomials in terms of integrations against Legendre polynomials
Source Link
user44143
user44143
Loading
commented on properties of analytic functions
Source Link
user44143
user44143
Loading
commented on properties of analytic functions
Source Link
user44143
user44143
Loading
Source Link
user44143
user44143
Loading