微分可能
$ a\quad(\in A)にて函数$ f:A\to Bの微分係数$ f'(a)が存在すること 定義
$ \forall A,B\forall f:A\to B\forall a\in A.
$ fは$ aにて微分できる$ :\iff\exist \alpha\in C.\frac{f(a+\delta)-f(a)}{\delta}\to \alpha\quad(\delta\to0)
$ Cを何にするかがわからないtakker.icon
$ \frac{f(a+\delta)-f(a)}{\delta}の極限が$ Bに含まれるなら、$ C=Bでいいだろうけど
前進差分$ \varDelta_\bullet f(\bullet):(\delta,x)\mapsto f(x+\delta)-f(x)を使えば、↓ともかける $ \exist\alpha\in C.\left.\frac{\varDelta_\delta f}{\varDelta_\delta x}\right|_{x=a}\to\alpha\quad(\delta\to 0)
この定義は次と同値
$ \forall A,B\forall f:A\to B\forall a\in A.
$ fは$ aにて微分できる$ :\iff\exist\alpha\in C\exist\varepsilon:A\setminus\{0\}\to B.\begin{dcases}\forall\delta\in A\setminus\{0\}.f(a+\delta)-f(a)=\alpha\delta+\varepsilon(\delta)\delta\\\varepsilon(\delta)\to 0\quad(\delta\to0)\end{dcases}
証明
$ \forall A,B\forall f:A\to B\forall a\in A.
$ \exist \alpha\in C.\frac{f(a+\delta)-f(a)}{\delta}\to \alpha\quad(\delta\to0)
$ \iff\exist\alpha\in C\forall\varepsilon\in B_{>0}\exist\delta\in A_{>0}\forall h\in A_{\neq0}.\left(|h|<\delta\implies\left|\frac{f(a+h)-f(a)}{h}-\alpha\right|<\varepsilon\right)
$ \iff\exist\alpha\in C\exist\varepsilon_f:A\setminus\{0\}\to B.\begin{dcases}\varepsilon_f:\delta\mapsto\frac{f(a+\delta)-f(a)}{\delta}-\alpha\\\forall\varepsilon\in B_{>0}\exist\delta\in A_{>0}\forall h\in A_{\neq0}.\left(|h|<\delta\implies\left|\varepsilon_f(h)\right|<\varepsilon\right)\end{dcases}
$ \iff\exist\alpha\in C\exist\varepsilon_f:A\setminus\{0\}\to B.\begin{dcases}\varepsilon_f:\delta\mapsto\frac{f(a+\delta)-f(a)}{\delta}-\alpha\\\varepsilon_f(\delta)\to0\quad(\delta\to0)\end{dcases}
$ \iff\exist\alpha\in C\exist\varepsilon:A\setminus\{0\}\to B.\begin{dcases}\forall\delta\in A\setminus\{0\}.f(a+\delta)-f(a)=\alpha\delta+\varepsilon(\delta)\delta\\\varepsilon(\delta)\to 0\quad(\delta\to0)\end{dcases}
証明は後日
References