Han–Banax teoremi
$\newcommand{\bbC}{\mathbb{C}}$
$\newcommand{\bbN}{\mathbb{N}}$
$\newcommand{\bbR}{\mathbb{R}}$
$\DeclareMathOperator{\re}{Re}$
$\DeclareMathOperator{\linspan}{span}$
Teorem. Tutaq ki, separabel $L$ həqiqi normalı fəzasının $L_0$ xətti altfəzasında $f_0$ məhdud xətti funksionalı təyin olunmuşdur. Onda bütöv $L$ fəzasında təyin olunmuş elə $f$ məhdud xətti funksionalı var ki, $\|f\| = \|f_0\|$ və hər bir $x \in L_0$ üçün $f(x) = f_0(x)$.
İsbatı. Əvvəlcə göstərək ki, $x_1 \notin L_0$ hər hansı elementdirsə, onda $f_0$ funksionalını tələb olunan qaydada
$$L_1 = \linspan (L_0 \cup \{x_1\}) = \{tx_1 + y \mid t \in \bbR,\ y \in L_0\}$$
xətti altfəzasında təyin olunmuş $f_1$ funksionalına davam etdirmək olar. Funksionalı davam etdirmək üçün yalnız $c := f_1(x_1)$ qiymətini təyin etmək kifayətdir, çünki
$$f_1(t x_1 + y) = t f_1(x_1) + f_1(y) = tc + f_0(y), \qquad t \in \bbR,\ y \in L_0.$$
Bu qiyməti elə seçməliyik ki, funksionalın norması artmasın. İxtiyari $t' < 0 < t$ ədədləri və $y$, $y' \in L_0$ elementləri üçün doğru olan
\begin{multline*}
f_0 \left( \frac{y}{t} \right) - f_0 \left( \frac{y'}{t'} \right) = f_0 \left( \frac{y}{t} - \frac{y'}{t'} \right) \le \left| f_0 \left( \frac{y}{t} - \frac{y'}{t'} \right) \right| \le \|f_0\| \left\| \frac{y}{t} - \frac{y'}{t'} \right\| = \\
= \|f_0\| \left\| x_1 + \frac{y}{t} - \left( x_1 + \frac{y'}{t'} \right) \right\| \le \|f_0\| \left( \left\| x_1 + \frac{y}{t} \right\| + \left\| x_1 + \frac{y'}{t'} \right\| \right)
\end{multline*}
bərabərsizliyindən çıxır ki,
$$\frac{\|f_0\| \|t' x_1 + y'\| - f_0(y')}{t'} \le \frac{\|f_0\| \|t x_1 + y\| - f_0(y)}{t}.$$
Beləliklə,
$$\sup_{\substack{t' < 0 \\ y' \in L_0}} \frac{\|f_0\| \|t' x_1 + y'\| - f_0(y')}{t'} \le \inf_{\substack{t > 0 \\ y \in L_0}} \frac{\|f_0\| \|t x_1 + y\| - f_0(y)}{t}.$$
Ona görə də elə $c \in \bbR$ ədədi tapmaq olar ki,
$$\sup_{\substack{t' < 0 \\ y' \in L_0}} \frac{\|f_0\| \|t' x_1 + y'\| - f_0(y')}{t'} \le c \le \inf_{\substack{t > 0 \\ y \in L_0}} \frac{\|f_0\| \|t x_1 + y\| - f_0(y)}{t}$$
olsun. Bu cür seçilmiş $c$ ədədi üçün
$$tc \le \|f_0\| \|t x_1 + y\| - f_0(y), \qquad t \in \bbR,\ y \in L_0$$
yəni
$$f_1(t x_1 + y) = tc + f_0(y) \le \|f_0\| \|t x_1 + y\|, \qquad t \in \bbR,\ y \in L_0$$
olar. Sonuncu bərabərsizliyi
$$f_1(z) \le \|f_0\| \|z\|, \qquad z \in L_1$$
şəklində yazıb, ondan alınan
$$-f_1(z) = f_1(-z) \le \|f_0\| \|z\|, \qquad z \in L_1$$
bərabərsizliyi ilə birləşdirsək,
$$|f_1(z)| \le \|f_0\| \|z\|, \qquad z \in L_1$$
olduğunu alarıq. Bu isə o deməkdir ki, $\|f_1\| \le \|f_0\|$. Digər tərəfdən
$$\|f_1\| = \sup_{z \in L_1} |f_1(z)| \ge \sup_{z \in L_0} |f_1(z)| = \sup_{z \in L_0} |f_0(z)| = \|f_0\|$$
olduğu üçün $\|f_1\| = \|f_0\|$.
Normalı fəzamız separabel olduğu üçün bu fəzada hər yerdə sıx olan $x_1$, $x_2$, $x_3$, $\ldots$ hesabi çoxluğu var. Bu çoxluğun elementləri vasitəsilə
$$L_k := \linspan (L_{k-1} \cup \{x_k\}), \quad k = 1, 2, 3, \ldots$$
xətti altfəzalar ardıcıllığını quraq. Onda hər bir $k \in \bbN$ ədədi üçün $x_k \in L_{k-1}$ olduqda $L_k = L_{k-1}$ olduğu üçün $L_{k-1}$ altfəzasında təyin olunmuş funksional həm də $L_k$ altfəzasında təyin olunmuş olur, $x_k \notin L_{k-1}$ olduqda isə $L_{k-1}$ altfəzasında təyin olunmuş funksionalı normasını saxlamaqla yuxarıdakı qayda ilə $L_k$ altfəzasına davam etdirmək olar. Ona görə də $L_0$ xətti altfəzasında təyin olunmuş $f_0$ funksionalını ardıcıl olaraq əvvəlcə $L_1$ xətti altfəzasına, sonra $L_2$ xətti altfəzasına və s. davam etdirsək, nəticədə $f_0$ funksionalı $L$ fəzasında hər yerdə sıx olan
$$\linspan (L_0 \cup \bigcup_{k=1}^{\infty} \{x_k\})$$
xətti altfəzasına davam olunmuş olacaq. Alınmış funksionalı isə kəsilməzliyə görə bütöv $L$ fəzasına davam etdirməklə axtardığımız $f$ funksionalını almış olarıq.
$\square$
Teorem. Tutaq ki, separabel $L$ kompleks normalı fəzasının $L_0$ xətti altfəzasında $f_0$ məhdud xətti funksionalı təyin olunmuşdur. Onda bütöv $L$ fəzasında təyin olunmuş elə $f$ məhdud xətti funksionalı var ki, $\|f\| = \|f_0\|$ və hər bir $x \in L_0$ üçün $f(x) = f_0(x)$.
İsbatı. Verilmiş $L$ və $L_0$ kompleks xətti fəzalarına həm də həqiqi xətti fəzalar kimi baxmaq olar. Bu zaman onları uyğun olaraq $\Lambda$ və $\Lambda_0$ ilə işarə edək. Onda
$$\varphi_0(x) := \re f_0(x)$$
ifadəsi $\Lambda_0$ həqiqi xətti fəzasında məhdud xətti funksional təyin edir və $\|\varphi_0\| = \|f_0\|$. Yuxarıdakı teoremə əsasən $\Lambda$ fəzasında təyin olunmuş elə $\varphi$ həqiqi xətti funksionalı var ki, $\|\varphi\| = \|\varphi_0\|$ və $\varphi(x) = \varphi_0(x)$, $x \in \Lambda_0$. Bu funksional vasitəsilə qurulmuş
$$f(x) := \varphi(x) - i \varphi(ix)$$
ifadəsi $L$ fəzasında kompleks xətti funksional təyin edir, çünki
\begin{multline*}
f((\alpha + i \beta)x) = \varphi(\alpha x + i \beta x) - i \varphi(-\beta x + i \alpha x) = \\
= \alpha \varphi(x) + \beta \varphi(ix) + i \beta \varphi(x) - i \alpha \varphi(ix) = \\
= (\alpha + i \beta)(\varphi(x) - i \varphi(ix)) = (\alpha + i \beta)f(x), \qquad \forall \alpha, \beta \in \bbR.
\end{multline*}
Aydındır ki,
$$f(x) = f_0(x), \qquad x \in L_0.$$
Nəhayət, ixtiyari $x \in L$ üçün funksionalın bu nöqtədəki qiymətini $f(x) = re^{i\theta}$ şəklində yazıb $\varphi(x) = \re f(x)$ bərabərliyini nəzərə alsaq
$$|f(x)| = e^{-i\theta} f(x) = f(e^{-i\theta} x) = \varphi(e^{-i\theta} x) \le \|\varphi_0\| \|x\| = \|f_0\| \|x\|$$
olduğu üçün $\|f\| = \|f_0\|$.
$\square$
Nəticə. Tutaq ki, $L$ normalı fəzadır. İxtiyari $x_0 \ne 0_L$ elementi üçün bütöv $L$ fəzasında təyin olunmuş elə $f$ məhdud xətti funksionalı var ki, $\|f\| = 1$ və $f(x_0) = \|x_0\|$.
İsbatı. Əvvəlcə $L_0 := \{ \alpha x_0 \mid \alpha \in \bbC \}$ xətti altfəzasında $f_0(\alpha x_0) := \alpha \|x_0\|$ xətti funksionalını təyin edək. Aydındır ki, $\|f_0\| = 1$. Han–Banax teoreminə görə $L$ fəzasında təyin olunmuş elə $f$ xətti funksionalı var ki, $\|f\| = \|f_0\| = 1$ və $f(x_0) = f_0(x_0) = \|x_0\|$.
$\square$