Tartışma:L'Hopital kuralı

Addition to the article "L'Hopital Kurali"

Part 1

$~t\vdash \quad \mathrm {f} :\mathbb {X} _{\mathrm {f} }\mapsto \mathbb {Y} _{\mathrm {f} }\ \ \land \ \ \mathbb {X} _{\mathrm {f} }\times \mathbb {Y} _{\mathrm {f} }\subseteq \mathbb {R} ^{2}\quad \land \quad \mathrm {g} :\mathbb {X} _{\mathrm {g} }\mapsto \mathbb {Y} _{\mathrm {g} }\ \ \land \ \ \mathbb {X} _{\mathrm {g} }\times \mathbb {Y} _{\mathrm {g} }\subseteq \mathbb {R} ^{2}\quad \land \quad a\in \mathbb {X} _{\mathrm {f} }\ \cap \ \mathbb {X} _{\mathrm {g} }\quad \land$

$~\lim _{x\to a}f(x)=\lim _{x\to a}g(x)\quad \land \quad \{\lim _{x\to a}f(x),\ \ \lim _{x\to a}g(x)\}\ \subseteq \ \{\{-\infty \},\ \{0\},\ \{\infty \}\}\quad \land$

$~\exists _{\delta \ \in \ (0,\ \infty )}\ \forall _{x\ \in \ \mathbb {X} _{\mathrm {f} }\ \cap \ \mathbb {X} _{\mathrm {g} }\ \land \ 0\ <\ |x-a|\ <\ \delta }\ (f'(x)\in \mathbb {R} \ \ \land \ \ g'(x)\in \mathbb {R} \setminus \{0\}\ )\quad \to$

$~(\ \exists _{L\ \in \ \mathbb {R} }\ (\lim _{x\to a}{\frac {f'(x)}{g'(x)}}=L)\quad \to \quad \lim _{x\to a}{\frac {f(x)}{g(x)}}=\lim _{x\to a}{\frac {f'(x)}{g'(x)}}\ )$

Notes

$~\mathrm {f} :\mathbb {X} _{\mathrm {f} }\mapsto \mathbb {Y} _{\mathrm {f} }\quad \Leftrightarrow \quad \mathrm {f} =\{\langle x,y\rangle |\quad \langle x,y\rangle \in \mathbb {X} _{\mathrm {f} }\times \mathbb {Y} _{\mathrm {f} }\quad \land \quad y=f(x)\ \}$

$~\vdash \quad \mathbb {X} _{\mathrm {f} }\times \mathbb {Y} _{\mathrm {f} }=\{\langle x,y\rangle |\quad x\in \mathbb {X} _{\mathrm {f} }\quad \land \quad y\in \mathbb {Y} _{\mathrm {f} }\ \}$

$~\mathbb {X} _{\mathrm {f} }\times \mathbb {Y} _{\mathrm {f} }\subseteq \mathbb {R} ^{2}\quad \Leftrightarrow \quad \forall x\forall y\ (\ \langle x,y\rangle \in \mathbb {X} _{\mathrm {f} }\times \mathbb {Y} _{\mathrm {f} }\ \to \ \langle x,y\rangle \in \mathbb {R} ^{2}\ )$

$~\mathrm {g} :\mathbb {X} _{\mathrm {g} }\mapsto \mathbb {Y} _{\mathrm {g} }\quad \Leftrightarrow \quad \mathrm {g} =\{\langle x,y\rangle |\quad \langle x,y\rangle \in \mathbb {X} _{\mathrm {g} }\times \mathbb {Y} _{\mathrm {g} }\quad \land \quad y=g(x)\ \}$

$~\vdash \quad \mathbb {X} _{\mathrm {g} }\times \mathbb {Y} _{\mathrm {g} }=\{\langle x,y\rangle |\quad x\in \mathbb {X} _{\mathrm {g} }\quad \land \quad y\in \mathbb {Y} _{\mathrm {g} }\ \}$

$~\mathbb {X} _{\mathrm {g} }\times \mathbb {Y} _{\mathrm {g} }\subseteq \mathbb {R} ^{2}\quad \Leftrightarrow \quad \forall x\forall y\ (\ \langle x,y\rangle \in \mathbb {X} _{\mathrm {g} }\times \mathbb {Y} _{\mathrm {g} }\ \to \ \langle x,y\rangle \in \mathbb {R} ^{2}\ )$

$~a\in \mathbb {X} _{\mathrm {f} }\cap \mathbb {X} _{\mathrm {g} }\quad \Leftrightarrow \quad a\in \mathbb {X} _{\mathrm {f} }\ \ \land \ \ a\in \mathbb {X} _{\mathrm {g} }$

$~\vdash \quad \mathbb {X} _{\mathrm {f} }\cap \mathbb {X} _{\mathrm {g} }=\{x|\quad x\in \mathbb {X} _{\mathrm {f} }\quad \land \quad x\in \mathbb {X} _{\mathrm {g} }\ \}$

$~\lim _{x\to a}f(x)=-\infty \quad \Leftrightarrow \quad \forall _{m\ \in \ (-\infty ,\ 0)}\exists _{\delta \ \in \ (0,\ \infty )}\ \forall _{x\ \in \ \mathbb {X} _{\mathrm {f} }}\ (0<|x-a|<\delta \ \to \ f(x)<m)$

$~\lim _{x\to a}g(x)=-\infty \quad \Leftrightarrow \quad \forall _{m\ \in \ (-\infty ,\ 0)}\ \exists _{\delta \ \in \ (0,\ \infty )}\ \forall _{x\ \in \ \mathbb {X} _{\mathrm {g} }}\ (0<|x-a|<\delta \ \to \ g(x)<m)$

$~\lim _{x\to a}f(x)=0\quad \Leftrightarrow \quad \forall _{\varepsilon \ \in \ (0,\ \infty )}\ \exists _{\delta \ \in \ (0,\ \infty )}\ \forall _{x\ \in \ \mathbb {X} _{\mathrm {f} }}\ (0<|x-a|<\delta \ \to \ |f(x)|<\varepsilon )$

$~\lim _{x\to a}g(x)=0\quad \Leftrightarrow \quad \forall _{\varepsilon \ \in \ (0,\ \infty )}\ \exists _{\delta \ \in \ (0,\ \infty )}\ \forall _{x\ \in \ \mathbb {X} _{\mathrm {g} }}\ (0<|x-a|<\delta \ \to \ |g(x)|<\varepsilon )$

$~\lim _{x\to a}f(x)=\infty \quad \Leftrightarrow \quad \forall _{M\ \in \ (0,\ \infty )}\ \exists _{\delta \ \in \ (0,\ \infty )}\ \forall _{x\ \in \ \mathbb {X} _{\mathrm {f} }}\ (0<|x-a|<\delta \ \to \ f(x)>M)$

$~\lim _{x\to a}g(x)=\infty \quad \Leftrightarrow \quad \forall _{M\ \in \ (0,\ \infty )}\ \exists _{\delta \ \in \ (0,\ \infty )}\ \forall _{x\ \in \ \mathbb {X} _{\mathrm {g} }}\ (0<|x-a|<\delta \ \to \ g(x)>M)$

$~\vdash \quad f'(x)=\lim _{h\to 0}{\frac {f(x+h)-f(x)}{h}}$

$~f'(x)\in \mathbb {R} \quad \Leftrightarrow \quad \exists y\ (y\in \mathbb {R} \ \ \land \ \ y=f'(x)\ )\quad \Leftrightarrow \quad \exists _{y\ \in \ \mathbb {R} }\ (y=f'(x))$

$~\vdash \quad g'(x)=\lim _{h\to 0}{\frac {g(x+h)-g(x)}{h}}$

$~g'(x)\in \mathbb {R} \setminus \{0\}\quad \Leftrightarrow \quad g'(x)\in \mathbb {R} \ \ \land \ \ g'(x)\notin \{0\}\quad \Leftrightarrow \quad g'(x)\in \mathbb {R} \ \ \land \ \ g'(x)\neq 0$

$~\exists _{L\ \in \ \mathbb {R} }\ (\lim _{x\to a}{\frac {f'(x)}{g'(x)}}=L)\quad \Leftrightarrow \quad \exists L\ (\ L\in \mathbb {R} \ \ \land \ \ \lim _{x\to a}{\frac {f'(x)}{g'(x)}}=L\ )\quad \Leftrightarrow \quad \lim _{x\to a}{\frac {f'(x)}{g'(x)}}\in \mathbb {R}$

Part 2

$~t\vdash \quad \mathrm {f} :\mathbb {X} _{\mathrm {f} }\mapsto \mathbb {Y} _{\mathrm {f} }\quad \land \quad \mathbb {X} _{\mathrm {f} }\ \times \ \mathbb {Y} _{\mathrm {f} }\subseteq \mathbb {R} ^{2}\quad \land \quad \mathrm {g} :\mathbb {X} _{\mathrm {g} }\mapsto \mathbb {Y} _{\mathrm {g} }\quad \land \quad \mathbb {X} _{\mathrm {g} }\ \times \ \mathbb {Y} _{\mathrm {g} }\subseteq \mathbb {R} \quad \land$

$~\exists a_{\mathrm {f} }\exists a_{\mathrm {g} }\ (\ \{a_{\mathrm {f} },\ a_{\mathrm {g} }\}\subseteq \mathbb {R} \quad \land \quad (a_{\mathrm {f} },\ \infty )\subseteq \mathbb {X} _{\mathrm {f} }\quad \land \quad (a_{\mathrm {g} },\ \infty )\subseteq \mathbb {X} _{\mathrm {g} }\quad \land$

$~\lim _{x\to \infty }f(x)=\lim _{x\to \infty }g(x)\quad \land \quad \{\lim _{x\to \infty }f(x),\ \ \lim _{x\to \infty }g(x)\}\ \subseteq \ \{\{-\infty \},\ \{0\},\ \{\infty \}\}\quad \land$

$~\exists _{a\ \in \ \mathbb {R} \ \land \ a\ \geq \ max(a_{\mathrm {f} },a_{\mathrm {g} })}\ \forall _{x\ \in \ (a,\infty )}\ (f'(x)\in \mathbb {R} \ \land \ g'(x)\in \mathbb {R} \setminus \{0\})\quad \land \quad \lim _{x\to \infty }{\frac {f'(x)}{g'(x)}}\in \mathbb {R} )\quad \to$

$~\to \quad \lim _{x\to \infty }{\frac {f(x)}{g(x)}}=\lim _{x\to \infty }{\frac {f'(x)}{g'(x)}}$

Notes

$~\{a_{\mathrm {f} },\ a_{\mathrm {g} }\}\subseteq \mathbb {R} \quad \Leftrightarrow \quad a_{\mathrm {f} }\in \mathbb {R} \ \ \land \ \ a_{\mathrm {g} }\in \mathbb {R}$

$~\vdash \quad (a_{\mathrm {f} },\ \infty )\ =\ \{x|\quad x\in \mathbb {R} \quad \land \quad x>a_{\mathrm {f} }\ \}$

$~(a_{\mathrm {f} },\ \infty )\subseteq \mathbb {X} _{\mathrm {f} }\quad \Leftrightarrow \quad \forall x\ (x\in (a_{\mathrm {f} },\ \infty )\ \to \ x\in \mathbb {X} _{\mathrm {f} })$

$~\vdash \quad (a_{\mathrm {g} },\ \infty )\ =\ \{x|\quad x\in \mathbb {R} \quad \land \quad x>a_{\mathrm {g} }\ \}$

$~(a_{\mathrm {g} },\ \infty )\subseteq \mathbb {X} _{\mathrm {g} }\quad \Leftrightarrow \quad \forall x\ (x\in (a_{\mathrm {g} },\ \infty )\ \to \ x\in \mathbb {X} _{\mathrm {g} })$

$~a\ \geq \ max(a_{\mathrm {f} },a_{\mathrm {g} })\quad \Leftrightarrow \quad a\ \geq \ {\frac {1}{2}}\cdot (a_{\mathrm {f} }+a_{\mathrm {g} }+|a_{\mathrm {f} }-a_{\mathrm {g} }|)$

Part 3

$~t\vdash \quad \mathrm {f} :\mathbb {X} _{\mathrm {f} }\mapsto \mathbb {Y} _{\mathrm {f} }\quad \land \quad \mathbb {X} _{\mathrm {f} }\times \mathbb {Y} _{\mathrm {f} }\subseteq \mathbb {R} ^{2}\quad \land \quad \mathrm {g} :\mathbb {X} _{\mathrm {g} }\mapsto \mathbb {Y} _{\mathrm {g} }\quad \land \quad \mathbb {X} _{\mathrm {g} }\times \mathbb {Y} _{\mathrm {g} }\subseteq \mathbb {R} ^{2}\quad \land$

$~\exists a_{\mathrm {f} }\exists a_{\mathrm {g} }\ (\ \{a_{\mathrm {f} },\ a_{\mathrm {g} }\}\subseteq \mathbb {R} \quad \land \quad (-\infty ,\ a_{\mathrm {f} })\subseteq \mathbb {X} _{\mathrm {f} }\quad \land \quad (-\infty ,\ a_{\mathrm {g} })\subseteq \mathbb {X} _{\mathrm {g} }\quad \land$

$~\lim _{x\to -\infty }f(x)=\lim _{x\to -\infty }g(x)\ \ \land \ \ \{\lim _{x\to -\infty }f(x),\ \ \lim _{x\to -\infty }g(x)\}\ \subseteq \ \{\{-\infty \},\ \{0\},\ \{\infty \}\}\ \ \land$

$~\exists _{a\ \in \ \mathbb {R} \ \land \ a\ \leq \ min(a_{\mathrm {f} },a_{\mathrm {g} })}\ \forall _{x\ \in \ (-\infty ,a)}\ (f'(x)\in \mathbb {R} \ \land \ g'(x)\in \mathbb {R} \setminus \{0\})\ \ \land \ \ \lim _{x\to -\infty }{\frac {f'(x)}{g'(x)}}\in \mathbb {R} )$

$~\to \quad \lim _{x\to -\infty }{\frac {f(x)}{g(x)}}=\lim _{x\to -\infty }{\frac {f'(x)}{g'(x)}}$

Notes

$~\vdash \quad (-\infty ,\ a_{\mathrm {f} })\ =\ \{x|\quad x\in \mathbb {R} \quad \land \quad x<a_{\mathrm {f} }\ \}$

$~(-\infty ,\ a_{\mathrm {f} })\subseteq \mathbb {X} _{\mathrm {f} }\quad \Leftrightarrow \quad \forall x\ (x\in (-\infty ,\ a_{\mathrm {f} })\ \to \ x\in \mathbb {X} _{\mathrm {f} })\quad \Leftrightarrow \quad \forall _{x\ \in \ (-\infty ,\ a_{\mathrm {f} })}\ (x\in \mathbb {X} _{\mathrm {f} })$

$~\vdash \quad (-\infty ,\ a_{\mathrm {g} })\ =\ \{x|\quad x\in \mathbb {R} \quad \land \quad x<a_{\mathrm {g} }\ \}$

$~(-\infty ,\ a_{\mathrm {g} })\subseteq \mathbb {X} _{\mathrm {g} }\quad \Leftrightarrow \quad \forall x\ (x\in (-\infty ,\ a_{\mathrm {g} })\ \to \ x\in \mathbb {X} _{\mathrm {g} })\quad \Leftrightarrow \quad \forall _{x\ \in \ (-\infty ,\ a_{g})}\ (x\in \mathbb {X} _{\mathrm {g} })$

$~a\ \leq \ min(a_{\mathrm {f} },a_{\mathrm {g} })\quad \Leftrightarrow \quad a\ \leq \ {\frac {1}{2}}\cdot (a_{\mathrm {f} }+a_{\mathrm {g} }-|a_{\mathrm {f} }-a_{\mathrm {g} }|)$