note-math

real-exponential_(tag)

如果指数是自然数, 则 $𝑎^{𝑛 + 𝑚} = 𝑎^{𝑛} 𝑎^{𝑚}$ . 可以简单地推广到有理数

对于指数是实数, 将指数函数 $𝑥 ⇝ 𝑎^{𝑥}$ 定义为满足 $𝑎^{𝑥 + 𝑦} = 𝑎^{𝑥} 𝑎^{𝑦}$ and $𝑎^{1} = 𝑎$

假设 $𝑓 (𝑥) = 𝑎^{𝑥}$ 解析. 对 $𝑓 (𝑥 + 𝑦) = 𝑓 (𝑥) 𝑓 (𝑦)$ 幂级数展开 (需要 $ℝ, ℂ, ℂ_{split}$ 的交换性?)

两边展开

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

令系数相同 $\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>)[]

从级数可以看出, 微分满足 $\frac{𝑑}{𝑑 𝑥} (𝑒^{𝑥}) = 𝑒^{𝑥} > 0$ ==> $𝑒^{𝑥}$ 存在 #link(<inverse-analytic>)[解析逆]

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

for $𝑎 > 0$ , 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) 定义了指数函数意味着对每个 $𝑎 \in ℝ$ 定义了每个实数指数 $𝑥$ , 因此也定义了幂函数 $𝑎 ⇝ 𝑎^{𝑥}$ 或者改写为 $𝑥 ⇝ 𝑥^{𝑎}$

也可以用 $𝑥^{𝑎} = 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}