avewright/proofwiki-math huggingface dataset:
Theorem: Excess Kurtosis of Logistic Distribution

Let $X$ be a continuous random variable which satisfies the logistic distribution:
:$X \sim \map {\operatorname {Logistic} } {\mu, s}$
Then the excess kurtosis $\gamma_2$ of $X$ is equal to $\dfrac 6 5$.

Proof:
From Kurtosis in terms of Non-Central Moments, we have: 
:$\gamma_2 = \dfrac {\expect {X^4} - 4 \mu \expect {X^3} + 6 \mu^2 \expect {X^2} - 3 \mu^4} {\sigma^4} - 3$
where: 
:$\mu$ is the expectation of $X$. 
:$\sigma$ is the standard deviation of $X$.
By Expectation of Logistic Distribution we have: 
:$\mu = \mu$ 
By Variance of Logistic Distribution we have: 
:$\sigma = \dfrac {s \pi} {\sqrt 3}$ 
From Moment in terms of Moment Generating Function:
:$\expect {X^n} = \map { {M_X}^{\paren n} } 0$
where $M_X$ is the moment generating function of $X$.
From Derivatives of Moment Generating Function of Logistic Distribution: 
:$\ds \map { {M_X}^{\paren 4} } 0 = \mu^4 \int_{\to 0}^{\to 1} \rd u - 4 \mu^3 s \int_{\to 0}^{\to 1} \map \ln {\dfrac {1 - u} u} \rd u + 6 \mu^2 s^2 \int_{\to 0}^{\to 1} \map {\ln^2} {\dfrac {1 - u} u} \rd u - 4 \mu s^3 \int_{\to 0}^{\to 1} \map {\ln^3} {\dfrac {1 - u} u} \rd u + s^4 \int_{\to 0}^{\to 1} \map {\ln^4} {\dfrac {1 - u} u} \rd u $
Therefore:
{{begin-eqn}}
{{eqn | l = \expect {X^4}
      | r = \mu^4 - 4 \mu^3 s \paren {0} + 6 \mu^2 s^2 \paren {\dfrac {\pi^2} 3} - 4 \mu s^3 \paren {0} + s^4 \paren {\dfrac {7 \pi^4} {15} }
      | c = Variance of Logistic Distribution/Lemma 4, Expectation of Logistic Distribution/Lemma 3 and Definite Integral from 0 to 1 of Even Powers of Logarithm of 1 - x over x
}}
{{eqn | r = \mu^4 + 2 \mu^2 s^2 \pi^2 + \dfrac {7 s^4 \pi^4} {15}
      | c = 
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = \gamma_2
      | r = \frac {\paren {\mu^4 + 2 \mu^2 s^2 \pi^2 + \dfrac {7 s^4 \pi^4} {15} } - 4 \mu \paren {\mu^3 + \mu s^2 \pi^2}  + 6 \mu^2 \paren {\mu^2 + \dfrac {s^2 \pi^2} 3} - 3 \mu^4} {\paren { {\dfrac {s \pi} {\sqrt 3} } }^4} - 3
      | c = 
}}
{{eqn | r = \frac {\paren {1 - 4 + 6 - 3} \mu^4 + \paren {2 - 4 + 2} \mu^2 s^2 \pi^2 + \dfrac {7 s^4 \pi^4} {15} } {\dfrac {s^4 \pi^4} 9} - 3
      | c = 
}}
{{eqn | r = \dfrac {\dfrac {21 s^4 \pi^4} 5} {s^4 \pi^4} - 3
      | c = 
}}
{{eqn | r = \dfrac 6 5
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Category:Kurtosis
Category:Logistic Distribution
em5u2fg9byb7y86kmqlc0mhqm0ofgh5
Theorem: Characterization of P-adic Valuation on Integers

Let $p \in \N$ be a prime number.
Let $\nu_p^\Z: \Z \to \N \cup \set {+\infty}$ be the $p$-adic valuation on $\Z$.
Let $n \in \Z_{\ne 0}$.
Then $\map {\nu_p^\Z} n$ is the unique $r \in \N$ such that:
:$\exists k \in \Z: n = p^r k : p \nmid k$

Proof:
=== Uniqueness of $r$ ===
Let $r, r'$ be such that:
:$\exists k \in \Z: n = p^r k : p \nmid k$
and:
:$\exists k' \in \Z: n = p^{r'} k' : p \nmid k'$
{{WLOG}}, suppose $r \ge r'$.
By subtracting the above equations:
:$0 = p^r k - p^{r'} k' = p^{r'} \paren {p^{r - r'} k - k'} = 0$
Therefore:
:$p ^{r - r'} k = k'$
Thus because $p \nmid k'$:
:$r - r' = 0$
{{qed|lemma}}
Let $n \in \Z_{\ne 0}$.
In the following, we shall find a $k\in\Z$ such that:
:$n = p^{\map {\nu_p^\Z} n} k$
:$p \nmid k$
By definition of $p$-adic valuation:
:$\map {\nu_p^\Z} n = \sup S$
where
:$S := \set {v \in \N: p^v \divides n}$
$S$ is a non-empty finite set, since:
:$0 \in S \subseteq \closedint 0 {\floor {\log _p n} }$
Hence, the supremum of $S$ is adopted, that is:
:$\map {\nu_p^\Z} n \in S$
:$\forall v > \map {\nu_p^\Z} n : v \notin S$
In particular:
:$p^{\map {\nu_p^\Z} n} \divides n$
:$p^{\map {\nu_p^\Z} n + 1} \nmid n$
Therefore, let:
:$k := \dfrac n {p^{\map {\nu_p^\Z} n} }$
so that:
:$n = p^{\map {\nu_p^\Z} n} k$
Finally, $p \nmid k$, as $p^{\map {\nu_p^\Z} n + 1} \nmid n$.
{{qed}}
Category:P-adic Valuations
irhe9zlw6my9nw3e6zfote2b7egpeq3
Theorem: Commutator of x and Distributional Derivative acting on Distribution

Let $T \in \map {\DD'} \R$ be a Schwartz distribution.
Let:
:$\sqbrk {x, \dfrac \d {\d x} } T := x \dfrac {\d T} {\d x} - \dfrac {\d \paren {x T} } {\d x}$
where derivatives are to be understood in the distributional sense.
Then:
:$\sqbrk {x, \dfrac \d {\d x} } T = - T$

Proof:
Let $\phi \in \map \DD \R$ be a test function.
{{begin-eqn}}
{{eqn | l = \map {\paren{x \dfrac {\d T} {\d x} - \dfrac {\d \paren {x T} } {\d x} } } \phi
      | r = \map {\paren {x \dfrac {\d T} {\d x} } } \phi - \map {\paren {\dfrac {\d \paren {x T} } {\d x} } } \phi
      | c = Linearity of Schwartz distribution
}}
{{eqn | r = \map {\paren {\dfrac {\d T} {\d x} } } {x \phi} - \map {\paren {\dfrac {\d \paren {x T} } {\d x} } } \phi
      | c = {{Defof|Multiplication of Schwartz Distribution by Smooth Function}}
}}
{{eqn | r =-\map T {\paren {x \phi}'} + \map {\paren {x T} } {\phi'}
      | c = {{Defof|Distributional Derivative}}
}}
{{eqn | r = -\map T {\paren {x \phi}'} + \map T {x \phi'}
      | c = {{Defof|Multiplication of Schwartz Distribution by Smooth Function}}
}}
{{eqn | r = \map T {-\phi - x \phi' + x \phi'}
      | c = Linearity of Schwartz distribution
}}
{{eqn | r = \map T {-\phi}
}}
{{eqn | r = -\map T \phi
      | c = Linearity of Schwartz distribution
}}
{{end-eqn}}
{{qed}}
Theorem: Commutative and Associative Product on Space of Distributions does not Exist

Let $\map {\DD'} \R$ be the distribution space.
Let $\alpha \in \map {C^\infty} \R$ be a smooth function.
Let $\circ$ be a product operation on $\map {\DD'} \R$.
Suppose:
:$\forall T \in \map {\DD'} \R : \forall \alpha \in \map {C^\infty} \R : \alpha \circ T := \alpha \cdot T$
where $\cdot$ stands for multiplication of Schwartz distribution by a smooth function.
Suppose $\circ$ is commutative and associative.
Then $\circ$ does not exist.

Proof:
{{AimForCont}} there is such a product.
Let $\delta \in \map {\DD'} \R$ be the Dirac delta distribution.
We also have from Principal Value of One over x is Distribution that $\ds \PV \frac 1 x$ is a Schwartz distribution.
Let $\phi, \psi \in \map \DD \R$ be test functions.
Then:
{{begin-eqn}}
{{eqn | l = x \cdot \map {\paren { \PV \frac 1 x} } \phi
      | r = \map {\paren {\PV \frac 1 x} } {x \phi}
}}
{{eqn | r = \lim_{\epsilon \mathop \to 0} \int_{\size x \mathop > \epsilon} \frac {x \map \phi x} x \rd x
}}
{{eqn | r = \lim_{\epsilon \mathop \to 0} \int_{\size x \mathop > \epsilon} \map \phi x \rd x
}}
{{eqn | r = \int_{- \infty}^\infty \map \phi x \rd x
      | c = {{Defof|Test Function}}
}}
{{eqn | r = \map {\bf 1} \phi
}}
{{eqn | r = c
      | c = $c \in \R$
}}
{{end-eqn}}
Here $\mathbf 1$ is the distribution associated to the real function defined by:
:$\mathbf 1 : \R \to 1$
Consider the product $\ds \delta \cdot x \cdot \PV \frac 1 x$ in the distributional sense, where:
:$\delta$ and $\PV \frac 1 x$ are distributions
:$x$ is a smooth function.
{{begin-eqn}}
{{eqn | l = \paren{\map \delta \psi \circ x} \circ \map {\paren{\PV \frac 1 x} } \phi
      | r = \paren{x \circ \map \delta \psi} \circ \map {\paren{\PV \frac 1 x} } \phi
      | c = Commutativity in the first pair
}}
{{eqn | r = \paren{x \cdot \map \delta \psi} \circ \map {\paren{\PV \frac 1 x} } \phi
}}
{{eqn | r = \map \delta {x \psi} \circ \map {\paren{\PV \frac 1 x} } \phi
      | c = {{Defof|Multiplication of Schwartz Distribution by Smooth Function}}
}}
{{eqn | r = 0 \circ \map {\paren{\PV \frac 1 x} } \phi
      | c = {{Defof|Dirac Delta Distribution}}
}}
{{eqn | r = 0 \cdot \map {\paren{\PV \frac 1 x} } \phi
}}
{{eqn | r = 0
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = \map \delta \psi \circ \paren {x \circ \map {\paren{\PV \frac 1 x} } \phi}
      | r = \map \delta \psi \circ \paren {x \cdot \map {\paren{\PV \frac 1 x} } \phi}
}}
{{eqn | r = \map \delta \psi \circ \map {\mathbf 1} \phi
}}
{{eqn | r = \map {\mathbf 1} \phi \circ \map \delta \psi
      | c = Commutativity
}}
{{eqn | r = c \circ \map \delta \psi
}}
{{eqn | r = c \cdot \map \delta \psi
}}
{{eqn | r = \map \delta {c \psi}
      | c = {{Defof|Multiplication of Schwartz Distribution by Smooth Function}}
}}
{{eqn | o = \ne
      | r = 0
}}
{{end-eqn}}
Altogether, we have that:
:$\ds \paren {\delta \circ x} \circ \PV \frac 1 x \ne \delta \circ \paren {x \circ \PV \frac 1 x}$
Hence, the associativity is violated, and we have reached a contradiction.
{{qed}}
Theorem: Exp (-x^2) is Schwartz Test Function

{{explain|What is the domain and codomain for the exponential function defined? Is it over the Real Numbers?}}
$\map \exp {-x^2}$ is a Schwartz test function.

Proof:
Let:
{{explain|What is p_n and what is p_n'? Please clarify}}
:$\dfrac {\d^n}{\d x^n} \map \exp {-x^2} = \map {p_n} x \map \exp {-x^2}$
We have that $\map {p_0} x = 1$ and $\map {p_1} x = -2 x$.
Then:
{{begin-eqn}}
{{eqn | l = \dfrac {\d^{n + 1} } {\d x^{n + 1} } \map \exp {-x^2}
      | r = \dfrac \d {\d x} \dfrac {\d^n}{\d x^n} \map \exp {-x^2}
}}
{{eqn | r = \dfrac \d {\d x} \paren {\map {p_n} x \map \exp {-x^2} }
}}
{{eqn | r = \map {p_n'} x \map \exp {-x^2} - 2 x \map {p_n} x \map \exp {-x^2}
}}
{{eqn | r = \paren{\map {p_n'} x - 2 x \map {p_n} x} \map \exp {-x^2}
}}
{{end-eqn}}
where 
:$\map {p_{n + 1}} x := \map {p_n'} x - 2 x \map {p_n} x$
Note that each subsequent $\map {p_n} x$ is constructed from derivatives, products and differences of polynomials.
Hence, $\map {p_n} x$ is a polynomial.
Consider the Maclaurin series of $\map \exp {x^2}$ .
{{begin-eqn}}
{{eqn | l = \map \exp {x^2}
      | r = \sum_{k \mathop = 0}^\infty \frac {\paren {x^2}^k} {k!}
}}
{{eqn | o = \ge
      | r = \frac {\paren {x^2}^k} {k!}
      | c = $k \in \N$
}}
{{eqn | r = \frac {\size x^k} {k!} \size x^k
      | c = Absolute Value Function is Completely Multiplicative
}}
{{eqn | ll = \leadsto 
      | l = \size x^{-k} k!
      | o = \ge
      | r = \size x^k \map \exp{-x^2}
}}
{{end-eqn}}
Suppose $\size x \ge 1$.
Then:
{{begin-eqn}}
{{eqn | l = \size {x^k \map \exp {-x^2} }
      | r = \size x^k \map \exp {-x^2}
      | c = Absolute Value Function is Completely Multiplicative
}}
{{eqn | o = \le 
      | r = \frac {k!} {\size x^k} 
}}
{{eqn | o = \le 
      | r = k!
      | c = $\size x \ge 1$
}}
{{end-eqn}}
Suppose $\size x \le 1$.
We have that $x^k \map \exp {-x^2}$ is a continuous function.
{{explain|There needs to be a link to show why this is a continuous real function, or a proof using epsilon delta to show it is continuous}}
Hence, it is bounded:
:$\forall x \in \closedint {-1} 1 \exists M \in \R : \size {x^k \map \exp {-x^2}} \le M$
Altogether:
:$\sup \size {x^k \map \exp {-x^2}} \le \map \max {M, k!} < \infty$
Thus:
:$\map \exp {-x^2} \in \map \SS \R$.
{{qed}}
Theorem: Discrete Space iff Diagonal Set on Product is Open

Let $\struct {X, \tau}$ be a topological space.
Endow $X \times X$ with the product topology.
Let: 
:$\Delta = \set {\tuple {x, x} : x \in X}$
Then: 
:$\tau = \powerset X$
{{iff}}:
:$\Delta$ is open in $X$.
That is:
:the topology on $X$ is discrete {{iff}} $\Delta$ is open in $X$.

Proof:
=== Sufficient Condition ===
Suppose that $\tau = \powerset X$. 
Then for each $x \in X$, the set:
:$\set {\tuple {x, x} }$
is open.
Note that we can write: 
:$\ds \Delta = \bigcup_{x \in X} \set {\tuple {x, x} }$
This is the union of open sets, so from the definition of a topology we have that: 
:$\Delta$ is open.
{{qed|lemma}}
Theorem: Order of Second Chebyshev Function

:$\ds \map \psi x = \sum_{p \mathop \le x} \ln p + \map \OO {\sqrt x \paren {\ln x}^2}$

Proof:
From the definition of the Second Chebyshev Function, we have: 
:$\ds \map \psi x = \sum_{k \mathop = 1}^\infty \paren {\sum_{p^k \mathop \le x} \ln p}$
where the inner sum runs over the primes $p$ with $p^k \le x$.
That is, the primes $p$ with $p \le x^{1/k}$, so we can write: 
:$\ds \sum_{p^k \mathop \le x} \ln p = \sum_{p \mathop \le x^{1/k} } \ln p$
Note that there are no primes with $p < 2$, so if: 
:$x^{1/k} < 2$
we have: 
:$\ds \sum_{p^k \mathop \le x} \ln p = 0$
That is, if: 
:$\ds k > \frac {\ln x} {\ln 2}$
So, we have: 
{{begin-eqn}}
{{eqn	| l = \map \psi x 
	| r = \sum_{1 \mathop \le k \mathop \le \frac {\ln x} {\ln 2} } \paren {\sum_{p \mathop \le x^{1/k} } \ln p}
}}
{{eqn	| r = \sum_{p \mathop \le x} \ln p + \sum_{2 \mathop \le k \mathop \le \frac {\ln x} {\ln 2} } \paren {\sum_{p \mathop \le x^{1/k} } \ln p}
}}
{{end-eqn}}
From Logarithm is Strictly Increasing, for $2 \le p \le x^{1/k}$ we have: 
:$\ds 0 < \ln p \le \map \ln {x^{1/k} }$
So:
{{begin-eqn}}
{{eqn	| l = \sum_{p \mathop \le x^{1/k} } \ln p
	| o = \le
	| r = \sum_{p \mathop \le x^{1/k} } \map \ln {x^{1/k} }
}}
{{eqn	| o = \le
	| r = x^{1/k} \map \ln {x^{1/k} }
}}
{{eqn	| r = \frac 1 k x^{1/k} \ln x
	| c = Logarithm of Power
}}
{{end-eqn}}
Then, for $k \ge 2$, we have: 
:$\ds \frac 1 k x^{1/k} \ln x \le \frac 1 2 \sqrt x \ln x$
so:
{{begin-eqn}}
{{eqn	| l = \sum_{2 \mathop \le k \mathop \le \frac {\ln x} {\ln 2} } \paren {\sum_{p \mathop \le x^{1/k} } \ln p}
	| o = \le
	| r = \sum_{2 \mathop \le k \mathop \le \frac {\ln x} {\ln 2} } \paren {\frac 1 2 \sqrt x \ln x}
}}
{{eqn	| o = \le
	| r = \frac 1 {2 \ln 2} \sqrt x \paren {\ln x}^2
}}
{{end-eqn}}
From the definition of big-O notation, we have: 
:$\ds \sum_{2 \mathop \le k \mathop \le \frac {\ln x} {\ln 2} } \paren {\sum_{p \mathop \le x^{1/k} } \ln p} = \map \OO {\sqrt x \paren {\ln x}^2}$
so:
:$\ds \map \psi x = \sum_{p \mathop \le x} \ln p + \map \OO {\sqrt x \paren {\ln x}^2}$
{{qed}}
Category:Second Chebyshev Function
Category:Analytic Number Theory
27o3ynbkv11z9kg4oxjntv3a74rns7d
Theorem: Sum of Big-O Estimates/Real Analysis

Let $c$ be a real number.
Let $f, g : \hointr c \infty \to \R$ be real functions.
Let $\OO$ denote big-$\OO$ notation.
Let $R_1 : \hointr c \infty \to \R$ be a real function such that $f = \map \OO {R_1}$.
Let $R_2 : \hointr c \infty \to \R$ be a real function such that $g = \map \OO {R_2}$.
Then: 
:$f + g = \map \OO {\size {R_1} + \size {R_2} }$

Proof:
Since: 
:$f = \map \OO {R_1}$
there exists $x_1 \in \hointr c \infty$ and a real number $C_1$ such that: 
:$\size {\map f x} \le C_1 \size {\map {R_1} x}$
for $x \ge x_1$.
Similarly, since:
:$g = \map \OO {R_2}$
there exists $x_2 \in \hointr c \infty$ and a real number $C_2$ such that: 
:$\size {\map g x} \le C_2 \size {\map {R_2} x}$
Set:
:$x_0 = \max \set {x_1, x_2}$
and:
:$C = \max \set {C_1, C_2}$
Then, for $x \ge x_0$ we have:
{{begin-eqn}}
{{eqn | l = \size {\map f x + \map g x}
      | o = \le
      | r = \size {\map f x} + \size {\map g x}
      | c = Triangle Inequality
}}
{{eqn | o = \le
      | r = C_1 \size {\map {R_1} x} + C_2 \size {\map {R_2} x}
      | c = since $x \ge x_1$ and $x \ge x_2$
}}
{{eqn | o = \le
      | r = C \size {\map {R_1} x} + C \size {\map {R_2} x}
}}
{{eqn | r = C \size {\size {\map {R_1} x} + \size {\map {R_2} x} }
}}
{{end-eqn}}
That is, by the definition of big-$\OO$ notation, we have: 
:$f + g = \map \OO {\size {R_1} + \size {R_2} }$
{{qed}}
Category:Big-O Notation
r6i9qbaanrmczv9cbim1tgujv2qmpqv
Theorem: Product of Big-O Estimates/Real Analysis

Let $c$ be a real number.
Let $f, g : \hointr c \infty \to \R$ be real functions.
Let $\OO$ denote big-$\OO$ notation.
Let $R_1 : \hointr c \infty \to \R$ be a real function such that $f = \map \OO {R_1}$.
Let $R_2 : \hointr c \infty \to \R$ be a real function such that $g = \map \OO {R_2}$.
Then: 
:$f g = \map \OO {R_1 R_2}$

Proof:
Since: 
:$f = \map \OO {R_1}$
there exists $x_1 \in \hointr c \infty$ and a real number $C_1$ such that: 
:$\size {\map f x} \le C_1 \size {\map {R_1} x}$
for $x \ge x_1$.
Similarly, since:
:$g = \map \OO {R_2}$
there exists $x_2 \in \hointr c \infty$ and a real number $C_2$ such that: 
:$\size {\map g x} \le C_2 \size {\map {R_2} x}$
Set:
:$x_0 = \max \set {x_1, x_2}$
Then for $x \ge x_0$ we have: 
{{begin-eqn}}
{{eqn | l = \size {\map f x \map g x}
      | r = \size {\map f x} \size {\map g x}
}}
{{eqn | o = \le
      | r = C_1 \size {\map {R_1} x} \size {\map g x}
      | c = since $x \ge x_1$
}}
{{eqn | o = \le
      | r = C_1 C_2 \size {\map {R_1} x} \size {\map {R_2} x}
      | c = since $x \ge x_2$
}}
{{eqn | r = C_1 C_2 \size {\map {R_1} x \map {R_2} x}
}}
{{end-eqn}}
That is, by the definition of big-$\OO$ notation, we have: 
:$f g = \map \OO {R_1 R_2}$
{{qed}}
Category:Big-O Notation
bdtwlhkf4vibhcih97oinhgap9qq1zj
Theorem: Bounds for Prime-Counting Function in terms of Second Chebyshev Function

There exists a real function $R : \hointr 2 \infty \to \R$ such that:
:$\ds \frac {\map \psi x} {\ln x} + \map R x \le \map \pi x \le \frac {2 \map \psi x} {\ln x} + \sqrt x$
for all real numbers $x \ge 2$, where:
:$\pi$ is the prime counting function
:$\psi$ is the second Chebyshev function
:$R = \map \OO {\sqrt x \ln x}$ where $\OO$ is big-$\OO$ notation.

Proof:
We have, from the definition of the prime counting function: 
:$\ds \map \pi x = \sum_{p \le x} 1$
We can write: 
:$\ds \sum_{p \le x} 1 = \sum_{p \le \sqrt x} 1 + \sum_{\sqrt x < p \le x} 1$
We have that: 
{{begin-eqn}}
{{eqn	| l = \sum_{p \le \sqrt x} 1
	| o = \le
	| r = \sum_{n \le \sqrt x} 1
}}
{{eqn	| r = \floor {\sqrt x}
}}
{{eqn	| o = \le
	| r = \sqrt x
	| c = {{Defof|Floor Function}}
}}
{{end-eqn}}
For $1 < \sqrt x < p$, we have from Logarithm is Strictly Increasing:
:$0 < \map \ln {\sqrt x} < \ln p$
So:
:$\ds \frac {\ln p} {\map \ln {\sqrt x} } > 1$
Then:
{{begin-eqn}}
{{eqn	| l = \sum_{\sqrt x < p \le x} 1
	| o = <
	| r = \sum_{\sqrt x < p \le x} \frac {\ln p} {\map \ln {\sqrt x} }
}}
{{eqn	| r = \frac 2 {\ln x} \sum_{\sqrt x < p \le x} \ln p
	| c = Logarithm of Power
}}
{{eqn	| o = \le
	| r = \frac 2 {\ln x} \sum_{p \le x} \ln p
}}
{{eqn	| o = \le
	| r = \frac 2 {\ln x} \sum_{k \mathop = 1}^\infty \paren {\sum_{p^k \le x} \ln p}
	| c = since $\ln p \ge \ln 2 > 0$ from Logarithm is Strictly Increasing
}}
{{eqn	| r = \frac 2 {\ln x} \map \psi x
	| c = {{Defof|Second Chebyshev Function}}
}}
{{end-eqn}}
So:
:$\ds \map \psi x \le \sqrt x + \frac 2 {\ln x} \map \psi x$ 
Now, from Order of Second Chebyshev Function, there exists a real function $r : \hointr 2 \infty \to \R$ such that: 
:$\ds \map \psi x = \sum_{p \le x} \ln p + \map r x$
where:
:$r = \map \OO {\sqrt x \paren {\ln x}^2}$
For $p \le x$, we have from Logarithm is Strictly Increasing:
:$0 < \ln p \le \ln x$
so:
:$\ds \frac {\ln p} {\ln x} < 1$
Then:
{{begin-eqn}}
{{eqn	| l = \sum_{p \le x} 1
	| o = >
	| r = \sum_{p \le x} \frac {\ln p} {\ln x}
}}
{{eqn	| r = \frac 1 {\ln x} \sum_{p \le x} \ln p
}}
{{eqn	| r = \frac {\map \psi x} {\ln x} + \frac {\map r x} {\ln x}
}}
{{end-eqn}}
From Product of Big-O Estimates, we have: 
:$\dfrac {\map r x} {\ln x} = \map \OO {\sqrt x \ln x}$
So if we take:
:$\map R x = \dfrac {\map r x} {\ln x}$
for each $x \ge 2$, we have: 
:$\ds \map \pi x = \sum_{p \le x} 1 \ge \frac {\map \psi x} {\ln x} + \map R x$
with $R = \map \OO {\sqrt x \ln x}$. 
So we obtain: 
:$\ds \frac {\map \psi x} {\ln x} + \map R x \le \map \pi x \le \frac {2 \map \psi x} {\ln x} + \sqrt x$
with $R = \map \OO {\sqrt x \ln x}$ as required.
{{qed}}
Category:Second Chebyshev Function
Category:Prime-Counting Function
Category:Inequalities
4w93i06w304u2s8erl75tnl37lu7kre
Theorem: Order of Natural Logarithm Function

Let $\epsilon \in \R_{>0}$ be a strictly positive real number.
Then: 
:$\ln x = \map \OO {x^\epsilon}$ as $x \to \infty$
and:
:$\ln x = \map \OO {x^{-\epsilon} }$ as $x \to 0^+$
where $\OO$ is big-O notation.

Proof:
We first show that: 
:$\ln x = \map \OO {x^\epsilon}$ as $x \to \infty$
We show that for $x \ge 1$, we have: 
:$\ds 0 \le \ln x \le \frac 1 \epsilon x^\epsilon$
We first show that for $t \ge 0$, we have: 
:$\ds t \le \frac 1 \epsilon e^{\epsilon t}$
The claim then follows taking $t = \ln x$.
Define a real function $f : \openint 0 \infty \to \R$ by: 
:$\ds \map f t = \frac 1 \epsilon e^{\epsilon t} - t$
for $t \ge 0$. 
Then $f$ is differentiable with derivative:
:$\map {f'} t = e^{\epsilon t} - 1$
by Derivative of Exponential Function.
So:
:$\map {f'} t \ge 0$ for all $t \ge 0$. 
So, from Real Function with Positive Derivative is Increasing:
:$f$ is increasing for $t \ge 0$. 
That is, for $t \ge 0$:
:$\ds \map f t \ge \map f 0 = \frac 1 \epsilon > 0$ 
So:
:$\ds \frac 1 \epsilon e^{\epsilon t} - t > 0$
for $t \ge 0$. 
So:
:$\ds \frac 1 \epsilon e^{\epsilon t} \ge t \ge 0$
for $t \ge 0$ as required.
Hence, for $x \ge 1$ we have: 
:$\ds 0 \le \ln x \le \frac 1 \epsilon x^\epsilon$
From the definition big-O notation, we have: 
:$\ln x = \map \OO {x^\epsilon}$ as $x \to \infty$
We now show that: 
:$\ln x = \map \OO {x^{-\epsilon} }$ as $x \to 0^+$
In particular, we can show that: 
:$\ds \size {\ln x} \le \frac 1 \epsilon x^{-\epsilon}$
for $0 < x \le 1$. 
Note that since: 
:$\ds \ln x \le \frac 1 \epsilon x^\epsilon$
for $x \ge 1$ we have: 
:$\ds \map \ln {\frac 1 x} \le \frac 1 \epsilon x^{-\epsilon}$
for $0 < x \le 1$. 
So, by Logarithm of Power:
:$\ds -\ln x \le \frac 1 \epsilon x^{-\varepsilon}$
For $0 < x \le 1$, we have: 
:$\ln x \le 0$
so:
:$\size {\ln x} = -\ln x$
from the definition of the absolute value. 
So we obtain: 
:$\ds \size {\ln x} \le \frac 1 \epsilon x^{-\epsilon}$
for $0 < x \le 1$ as required.
From the definition big-O notation, we therefore have:
:$\ln x = \map \OO {x^{-\epsilon} }$ as $x \to 0^+$
{{qed}}
Category:Natural Logarithms
bh2uo86n1ikujcnn8azjtkledsjp3jd
Theorem: Extension Theorem for Distributive Operations/Existence and Uniqueness

:There exists a unique operation $\circ'$ on $T$ which distributes over $*$ in $T$ and induces on $R$ the operation $\circ$.

Proof:
We have {{hypothesis}} that all the elements of $\struct {R, *}$ are cancellable.
Thus Inverse Completion of Commutative Semigroup is Abelian Group can be applied.
So $\struct {T, *}$ is an abelian group.
Theorem: Extension Theorem for Distributive Operations/Associativity

:If $\circ$ is associative, then so is $\circ'$.

Proof:
We have that $\circ'$ exists and is unique by Extension Theorem for Distributive Operations: Existence and Uniqueness.
Suppose $\circ$ is associative.
As $\circ'$ distributes over $*$, for all $n, p \in R$, the mappings:
{{begin-eqn}}
{{eqn | l = x \mapsto \paren {x \circ' n} \circ' p
      | o = ,
      | r = x \in T
      | c = 
}}
{{eqn | l = x \mapsto x \circ' \paren {n \circ' p}
      | o = ,
      | r = x \in T
      | c = 
}}
{{end-eqn}}
are endomorphisms of $\struct {T, *}$ that coincide on $R$ by the associativity of $\circ$ and hence are the same mapping.
Therefore:
:$\forall x \in T, n, p \in R: \paren {x \circ' n} \circ' p = x \circ' \paren {n \circ' p}$
Similarly, for all $x \in T, p \in R$, the mappings:
{{begin-eqn}}
{{eqn | l = y \mapsto \paren {x \circ' y} \circ' p
      | o = ,
      | r = y \in T
      | c = 
}}
{{eqn | l = y \mapsto x \circ' \paren {y \circ' p}
      | o = ,
      | r = y \in T
      | c = 
}}
{{end-eqn}}
are endomorphisms of $\struct {T, *}$ that coincide on $R$ by what we have proved and hence are the same mapping.
Therefore:
:$\forall x, y \in T, p \in R: \paren {x \circ' y} \circ' p = x \circ' \paren {y \circ' p}$
Finally, for all $x, y \in T$, the mappings:
{{begin-eqn}}
{{eqn | l = z \mapsto \paren {x \circ' y} \circ' z
      | o = ,
      | r = z \in T
      | c = 
}}
{{eqn | l = z \mapsto x \circ' \paren {y \circ' z}
      | o = ,
      | r = z \in T
      | c = 
}}
{{end-eqn}}
are endomorphisms of $\struct {T, *}$ that coincide on $R$ by what we have proved and hence are the same mapping.
Therefore $\circ'$ is associative.
{{qed}}
Theorem: Extension Theorem for Distributive Operations/Commutativity

:If $\circ$ is commutative, then so is $\circ'$

Proof:
We have that $\circ'$ exists and is unique by Extension Theorem for Distributive Operations: Existence and Uniqueness.
Suppose $\circ$ is commutative.
As $\circ'$ distributes over $*$, for all $n \in R$, the mappings:
{{begin-eqn}}
{{eqn | l = x \mapsto x \circ' n
      | o = ,
      | r = x \in T
      | c = 
}}
{{eqn | l = x \mapsto n \circ' x
      | o = ,
      | r = x \in T
      | c = 
}}
{{end-eqn}}
are endomorphisms of $\struct {T, *}$ that coincide on $R$ by the commutativity of $\circ$ and hence are the same mapping.
Therefore $\forall x \in T, n \in R: x \circ' n = n \circ' x$.
Finally, for all $y \in T$, the mappings:
{{begin-eqn}}
{{eqn | l = z \mapsto z \circ' y
      | o = ,
      | r = z \in T
      | c = 
}}
{{eqn | l = z \mapsto y \circ' z
      | o = ,
      | r = z \in T
      | c = 
}}
{{end-eqn}}
are endomorphisms of $\struct {T, *}$ that coincide on $R$ by what we have proved and hence are the same mapping.
Therefore $\circ'$ is commutative.
{{qed}}