I realized that before the Square Root Lemma post, I should have included a short section. Here is this section.
The following Lemma is often being used in the construction of the square root of a self-adjoint positive operator. We will not use it, but, for completeness, we will state it here in full generality, for self-adjoint and mot necessarily positive operators.
Lemma. [Monotone convergence for bounded self-adjoint operators]
Let 
be a real or complex Hilbert space and let 
be a net of
bounded self-adjoint operators on such that
![\[ \iota_1\le \iota_2 \implies A_{\iota_1}\le A_{\iota_2}, \]](https://arkadiusz-jadczyk.eu/blog/wp-content/ql-cache/quicklatex.com-a6c4acf195c072bc40494094e7aac45a_l3.png "Rendered by QuickLaTeX.com")
with respect to the quadratic-form order 
for all 
.
Assume there exists a bounded self-adjoint operator 
with 
for all
. Then there is a bounded self-adjoint operator 
such that
![\[ (x,A_0x) = \sup_{\iota\in\mathcal I} (x,A_\iota x), \qquad x\in\mathcal H, \]](https://arkadiusz-jadczyk.eu/blog/wp-content/ql-cache/quicklatex.com-4ffddca4103d6d1200a184d49b4b6ac4_l3.png "Rendered by QuickLaTeX.com")
and 
in the strong operator topology. Equivalently: for every 
, for every 
, there is 
such that 
for all 
In particular, if 
for all 
, then 
is positive.
Proof.
The proof, covering both real and complex cases, can be found in [1, Proposition 13, Ch. V.46]
References.
[1] Bourbaki, n., ”Topological Vector Spaces Chapters 1–5”, Springer 2003.
There will be one more necessary addition: The Polar Decomposition. I am working on putting all this Hilbert space stuff in one big file, for reference.
