note-math

real-exponential_(tag)

If the exponent is a natural number, then $𝑎^{𝑛 + 𝑚} = 𝑎^{𝑛} 𝑎^{𝑚}$ . It can be simply generalized to rational numbers

For the exponent being a real number, define the exponential function $𝑥 ⇝ 𝑎^{𝑥}$ as satisfying $𝑎^{𝑥 + 𝑦} = 𝑎^{𝑥} 𝑎^{𝑦}$ and $𝑎^{1} = 𝑎$

Assume $𝑓 (𝑥) = 𝑎^{𝑥}$ is analytic. Power series expansion of $𝑓 (𝑥 + 𝑦) = 𝑓 (𝑥) 𝑓 (𝑦)$ (requires commutativity of $ℝ, ℂ, ℂ_{split}$ ?)

Expand both sides

\begin{matrix} \sum \frac{𝑓^{(𝑛)} (0)}{𝑛!} {(𝑥 + 𝑦)}^{𝑛} & = & \sum \frac{𝑓^{(𝑛)} (0)}{𝑛!} 𝑥^{𝑛} \sum \frac{𝑓^{(𝑛)} (0)}{𝑛!} 𝑦^{𝑛} \\ \sum_{𝑛} \sum_{𝑖 + 𝑗 = 𝑛} \frac{𝑓^{(𝑛)} (0)}{𝑛!} \frac{𝑛!}{𝑖! 𝑗!} 𝑥^{𝑖} 𝑦^{𝑗} & = & \sum_{𝑛} \sum_{𝑖 + 𝑗 = 𝑛} \frac{𝑓^{(𝑖)} (0)}{𝑖!} \frac{𝑓^{(𝑗)} (0)}{𝑗!} 𝑥^{𝑖} 𝑦^{𝑗} \end{matrix}

Let the coefficients be the same $\forall 𝑛, \forall 𝑖 + 𝑗 = 𝑛, 𝑓^{(𝑛)} (0) = 𝑓^{(𝑖)} (0) 𝑓^{(𝑗)} (0)$
==>

$\forall 𝑛, 𝑓^{(𝑛)} (0) = 𝑓^{(𝑛)} (0) 𝑓^{(0)} (0) ⟹ 𝑓^{(0)} (0) = 1$
$\forall 𝑛, 𝑓^{(𝑛)} (0) = {(𝑓^{(1)} (0))}^{𝑛}$

==>

𝑓 (𝑥) = \sum {(\frac{𝑓^{(1)} (0)}{𝑛!} 𝑥)}^{𝑛}

natural-exponential_(tag) def $𝑒^{𝑥} = exp 𝑥 = \sum \frac{1}{𝑛!} 𝑥^{𝑛} : ℝ \to (0, \infty)$ with $𝑒^{1} = exp (1) = \sum \frac{1}{𝑛!} = 𝑒$ #link(<natural-constant>)[]

from the series, we can see that, differential $\frac{𝑑}{𝑑 𝑥} (𝑒^{𝑥}) = 𝑒^{𝑥} > 0$ ==> $𝑒^{𝑥}$ exists #link(<inverse-analytic>)[]

natural-logarithm_(tag) def $log = {exp}^{- 1} : (0, \infty) \to ℝ$ . $\frac{𝑑}{𝑑 𝑥} log 𝑥 = \frac{1}{𝑥}$

for $𝑎 > 0$ , def $𝑓^{1} (0) ≔ log 𝑎 \in ℝ$

for $𝑎$ , def $𝑓^{1} (0) ≔ log 𝑎 \in 𝕂$

\begin{matrix} 𝑎^{1} & = & 𝑓 (1) \\ = & \sum \frac{1}{𝑛!} {(log 𝑎)}^{𝑛} \\ = & exp log 𝑎 \\ = & 𝑎 \\ 𝑎^{𝑥} & = & 𝑓 (𝑥) \\ = & \sum \frac{1}{𝑛!} {(log 𝑎 \cdot 𝑥)}^{𝑛} \\ = & exp (𝑥 log 𝑎) \end{matrix}

power-function_(tag) Defining the exponential function means that for each $𝑎 \in ℝ$ , each real exponent $𝑥$ is defined, and thus the power function $𝑎 ⇝ 𝑎^{𝑥}$ is also defined, or rewritten as $𝑥 ⇝ 𝑥^{𝑎}$

It can also be expressed as $𝑥^{𝑎} = exp (𝑎 log 𝑥)$

Euler-formula_(tag)

$ℂ$

\begin{matrix} exp 𝑧 & = & cos 𝑧 + i sin 𝑧 \\ i & ≃ & (\begin{matrix} - 1 \\ 1 \end{matrix}) \sim so (2) \end{matrix}

$ℂ_{split}$

\begin{matrix} exph 𝑧 & = & cosh 𝑧 + i_{split} sinh 𝑧 \\ i_{split} & ≃ & (\begin{matrix} 1 \\ 1 \end{matrix}) \sim so (1, 1) \end{matrix}