Completing the elementary inputs actually used

Prerequisite companion. The source is Jiří Lebl's freely accessible Basic Analysis, version 6.3, author edition. This is an attributed adaptation and extension under CC BY-SA 4.0. It fills particular omitted proofs in §§1.2, 2.1–2.4, 7.2–7.6 and 8.2. The complete human proofs already in the programme are retained through exact bindings; they are not replaced by a fresh treatment of those chapters. The one short reproduced route, the Archimedean argument, permits the needed proof to be carried separately from unrelated material on its source page.

The underlying definitions are those of an ordered field of real numbers with the least-upper-bound axiom, natural-number induction, finite sums, functions, sets and sequences. These are the declared axioms and definitions of the arguments, rather than additional theorems asserted without proof. No claim about constructing or uniquely characterizing that field is used here. For a nonempty set bounded below, its infimum exists by applying the supremum axiom to its negative: if $u=\sup(-A)$ , then $-u$ is a lower bound of $A$ , and every lower bound $b$ satisfies $-b\geq u$ , hence $b\leq-u$ .

P6. The short omissions in the compactness and contraction chain

P6.0. The Archimedean argument used by these proofs

This is the argument of Lebl's Theorem 1.2.4(i), adapted with its hypothesis explicit. The natural numbers are not bounded above in the ordered complete field. Otherwise $b=\sup\mathbb N$ would exist. Since $b-1<b$ , $b-1$ is not an upper bound, so some $m\in\mathbb N$ satisfies $m>b-1$ . Then $m+1\in\mathbb N$ and $m+1>b$ , a contradiction. Consequently, for $x>0$ and any $y$ , some $n$ satisfies $n>y/x$ , or $nx>y$ . In particular $1/n\to0$ : given $\varepsilon>0$ , choose $N>1/\varepsilon$ ; every $n\geq N$ satisfies $0<1/n<\varepsilon$ . $\square$

P6.1. Subsequence indices, metric limits and tails

If $n_{k+1}>n_k$ are positive integers, then $n_k\geq k$ . Indeed $n_1\geq1$ ; if $n_k\geq k$ , the integer inequality gives $n_{k+1}\geq n_k+1\geq k+1$ . Thus, if $x_n\to p$ in a metric space, every subsequence converges to $p$ : a bound $d(x_n,p)<\varepsilon$ for $n\geq N$ also holds at $n_k$ for $k\geq N$ . If a tail converges, take the larger of its threshold and its initial index to obtain the same bound for the original sequence. These statements complete the metric version left as Proposition 7.3.6.

For Proposition 7.3.5, if $d(x_n,p)\leq a_n\to0$ , then, for every $\varepsilon>0$ , eventually $d(x_n,p)\leq a_n<\varepsilon$ , so $x_n\to p$ . Conversely take $a_n=d(x_n,p)$ ; the definition of convergence says exactly that this nonnegative real sequence tends to zero. A convergent metric sequence is bounded (Proposition 7.3.4): eventually its distance from $p$ is less than 1, and the maximum of 1 and the finitely many earlier distances bounds every term. $\square$

P6.2. Decreasing limits and approximation to an extremum

For the decreasing half of Theorem 2.1.10, let $x_n$ decrease and be bounded below, and set $l=\inf\{x_n:n\geq1\}$ . Given $\varepsilon>0$ , $l+\varepsilon$ cannot be a lower bound, so there is an $N$ with $x_N<l+\varepsilon$ . Then $l\leq x_n\leq x_N<l+\varepsilon$ for every $n\geq N$ , proving $x_n\to l$ . The increasing proof is already written in the programme source.

If $S\ne\varnothing$ is bounded above and $s=\sup S$ , for every $\varepsilon>0$ there is an $a\in S$ with $s-\varepsilon<a\leq s$ : otherwise $s-\varepsilon$ would be an upper bound smaller than the least one. This proves Proposition 1.2.8. Choose $a_n\in S$ with $s-1/n<a_n\leq s$ , and put $u_n=\max(a_1,\ldots,a_n)$ . Each $u_n$ is an element of $S$ , the sequence is increasing, and $0\leq s-u_n<1/n$ . P6.0 implies $u_n\to s$ . For an infimum $t$ , choose $b_n\in S$ with $t\leq b_n<t+1/n$ , using the same greatest-lower-bound argument, and take the finite minima. This supplies both monotone sequences in Proposition 2.1.13, used by the extreme-value proof of Theorem 7.5.6. $\square$

P6.3. The omitted lower-limit steps in the real Cauchy proof

For a bounded sequence, choose $L\leq x_j\leq U$ for every $j$ . Each tail is nonempty, so its infimum $b_n$ and supremum $a_n$ satisfy $L\leq b_n\leq a_n\leq U$ . Passing to a smaller tail cannot decrease its infimum: any lower bound of the old tail is a lower bound of the new one. Hence $b_{n+1}\geq b_n$ . These are the omitted boundedness and monotonicity steps of Proposition 2.3.2.

The liminf half of Theorem 2.3.4 follows from its fully written limsup half with all signs justified as follows. The number $-b_n$ is the supremum of $\{-x_j:j\geq n\}$ , by the definition of an infimum. If $v_n\to v$ , then $-v_n\to-v$ because $|(-v_n)-(-v)|=|v_n-v|$ . Applying the proved limsup subsequence theorem to $-x_j$ therefore gives indices $m_k$ such that $-x_{m_k}\to-\lim b_n$ , hence $x_{m_k}\to\lim b_n=\liminf x_n$ . This completes the input used in the existing full proof of Theorem 2.4.5; that Cauchy proof is retained, including its comparison of the two subsequential limits.

The subtraction case omitted in Proposition 2.2.5 uses

|(x_n-y_n)-(x-y)|\leq|x_n-x|+|y_n-y|.

Choose both terms smaller than $\varepsilon/2$ . Its addition, product and reciprocal proofs are already complete in the source. $\square$

P6.4. Closed balls and closed complete subspaces

To complete Proposition 7.2.9, if $y\notin C(p,r)$ , then $\delta=d(p,y)-r>0$ . For $d(y,z)<\delta$ , the triangle inequality implies $d(p,z)\geq d(p,y)-d(y,z)>r$ . Thus a ball about every point of the complement stays in the complement, proving that $C(p,r)$ is closed. The proof that open balls are open is already in §7.2.

To complete Proposition 7.4.6, let $E$ be a closed subset of a complete metric space $X$ . A Cauchy sequence in $E$ is Cauchy in $X$ , since its distances are unchanged. It has a limit $p$ in $X$ . The already proved Proposition 7.3.12 says $p\in E$ . The same distance inequalities then prove convergence in $E$ . In particular a closed Euclidean ball is complete, using the complete coordinatewise proof for $\mathbb R^n$ in Proposition 7.4.4. $\square$

P6.5. The geometric bound inside the contraction proof

In Theorem 7.6.2 the contraction constant can be taken with $0\leq k<1$ : replacing any negative constant by zero only weakens the distance bound. For $0<k<1$ and a positive integer $q$ , expanding and cancelling finite sums gives

(1-k)\sum_{j=0}^{q-1}k^j=1-k^q, \qquad 0\leq\sum_{j=0}^{q-1}k^j\leq\frac1{1-k}.

Consequently the existing iteration estimate can use a finite sum directly:

d(x_m,x_n)\leq\frac{k^n}{1-k}d(x_1,x_0),\qquad m>n.

Proposition 2.2.11 has a complete proof that $k^n\to0$ , after the decreasing-limit step is supplied by P6.2. Given $\varepsilon>0$ , choose $N$ so that the right side at $n=N$ is smaller than $\varepsilon$ . It then stays smaller for every $n\geq N$ , independently of $m>n$ ; interchanging the indices covers $n>m$ , and equal indices have zero distance. This proves precisely the Cauchy claim used in the source. If $k=0$ , the image of the map is a single point, and the iteration is constant after its first step.

The limiting fixed-point step needs only the same Lipschitz estimate:

d(\varphi(x),x)\leq k\,d(x,x_n)+d(x_{n+1},x)\longrightarrow0.

Thus it does not require a separate unproved continuity theorem. The existence and uniqueness argument of the source remains unchanged. $\square$

P6.6. Closed-set operations used by the closure argument

Lebl's Proposition 7.2.8 leaves the closed-set version of the topology rules as an exercise. It follows from the proved open-set rules of Proposition 7.2.6 and the following identities, verified by membership:

X\setminus\bigcap_{\lambda}F_\lambda =\bigcup_{\lambda}(X\setminus F_\lambda),\qquad X\setminus\bigcup_{j=1}^m F_j =\bigcap_{j=1}^m(X\setminus F_j).

If the $F$ 's are closed, their complements are open by definition. The first right side is open by the union rule, and the second by the finite-intersection rule. Hence arbitrary intersections and finite unions of closed sets are closed. The empty set and the whole space are closed because their complements are open. These steps complete the input of the existing proofs that a closure is closed and that every ball about a point of the closure meets the set (Propositions 7.2.19 and 7.2.22).

The empty-set case in the compactness arguments is immediate from the definition: an empty family of members of any cover already covers the empty set. Proofs that begin by choosing a point apply to the nonempty case. This convention also removes an implicit nonemptiness step in Theorem 7.4.11.

That theorem also refers to Proposition 7.3.5. Here is the complete metric majorant argument. A sequence $x_n$ in a metric space converges to $p$ if and only if there are real numbers $a_n\to0$ with $d(x_n,p)\leq a_n$ for every $n$ . For the forward implication take $a_n=d(x_n,p)$ ; the real limit assertion is exactly the metric convergence definition. Conversely, given $\varepsilon>0$ , choose $N$ such that $|a_n|<\varepsilon$ for $n\geq N$ . Then $0\leq d(x_n,p)\leq a_n\leq|a_n|<\varepsilon$ , which is metric convergence. In the compactness proof $a_j=1/j$ tends to zero by the Archimedean argument P6.0. Thus that source cross-reference uses the full proof here, including both directions, rather than an unproved external result. $\square$

P7. Why permutation parity in the determinant is well defined

This completes the parity exercise preceding Lebl's determinant formula in §8.2.3. For indeterminates $t_1,\ldots,t_n$ , put

V(t)=\prod_{i<j}(t_j-t_i).

Interchanging two adjacent variables reverses their mutual factor and permutes all the other factors in pairs, so it multiplies $V$ by $-1$ . Interchanging positions $i<j$ can be performed by moving position $i$ to $j$ in $j-i$ adjacent steps and then moving the old position $j$ back to $i$ in $j-i-1$ steps. It therefore also changes $V$ by $-1$ .

Every permutation is a product of adjacent interchanges: move the entry 1 to the first position, then the entry 2 to the second without changing the first, and continue. Each step moves a specified entry through only finitely many positions; after $n$ stages the order is the identity. Thus a permutation $\sigma$ transforms $V(t)$ into $\epsilon_\sigma V(t)$ , where $\epsilon_\sigma\in\{1,-1\}$ . This sign is independent of the chosen decomposition, since evaluation at $(t_1,\ldots,t_n)=(1,\ldots,n)$ gives the fixed nonzero quotient

\epsilon_\sigma= \frac{\prod_{i<j}(\sigma(j)-\sigma(i))} {\prod_{i<j}(j-i)}.

Applying two permutations successively shows $\epsilon_{\sigma\tau}=\epsilon_\sigma\epsilon_\tau$ : both sides are the factor by which the same substitution changes $V$ . Any decomposition into $r$ arbitrary interchanges changes $V$ by $(-1)^r$ , so $(-1)^r=\epsilon_\sigma$ . Its parity is therefore intrinsic. These facts supply exactly the signs used in the programme determinant proofs and the cofactor calculation P2. For $n=1$ , the empty product is 1 and the same conclusions hold. $\square$

P8. Positive square roots without a smooth-inverse circularity

The existence argument generalizes the actually read square-root example in Lebl §1.2; the general root there is left as an exercise. Fix $r>0$ and let $A=\{x\geq0:x^2\leq r\}$ . This set is nonempty and bounded above by $r+1$ . It contains a positive point, for example $\min(r,1)/2$ . Therefore $s=\sup A>0$ exists.

If $s^2<r$ , choose

0<h\leq\min\left(1,\frac{r-s^2}{2(2s+1)}\right).

Then $(s+h)^2-s^2=h(2s+h)\leq(r-s^2)/2<r-s^2$ , so $s+h\in A$ , contradicting that $s$ is an upper bound. If $s^2>r$ , choose

0<h\leq\min\left(\frac s2,\frac{s^2-r}{4s}\right).

Then $s-h>0$ , and $(s-h)^2\geq s^2-2sh\geq(s^2+r)/2>r$ . Every nonnegative $x\geq s-h$ has $x^2>r$ , so $s-h$ is an upper bound for $A$ , contradicting minimality of $s$ . Hence $s^2=r$ . Positive squaring is strictly increasing, since $u^2-v^2=(u-v)(u+v)>0$ when $u>v\geq0$ ; this also proves uniqueness. Write this root as $\sqrt r$ , and set $\sqrt0=0$ . The same comparison proves monotonicity of the square root.

For $r>0$ and $t\geq0$ ,

|\sqrt t-\sqrt r|= \frac{|t-r|}{\sqrt t+\sqrt r}\leq\frac{|t-r|}{\sqrt r}.

This proves continuity at positive $r$ . At zero, $0\leq t<\varepsilon^2$ implies $\sqrt t<\varepsilon$ , proving one-sided continuity there. For $r+h>0$ and $h\ne0$ , rationalizing gives

\frac{\sqrt{r+h}-\sqrt r}{h} =\frac1{\sqrt{r+h}+\sqrt r}\longrightarrow\frac1{2\sqrt r}.

So the positive square root is $C^1$ on $(0,\infty)$ . If it is $C^k$ , the reciprocal calculation in P2 and the chain rule show that its displayed derivative is $C^k$ ; hence it is $C^{k+1}$ . Induction proves smoothness without invoking the inverse function theorem whose proof later uses these roots. The derivative step inherits the declared elementary product and chain rules; it does not close all of F0-CALC. $\square$

Remaining proof review

The exact existing programme files, anchors and these local completions form one dependency chain. Their mathematical arguments must be distinguished from the eligibility of whole source pages or whole-book downloads. The selected dimension and differential-calculus inputs, including P8's smoothness, are now bound in differential-proof-chain.json. The compact integral, fundamental theorem and Taylor inputs are bound separately in integration-proof-chain.json. Global integration, exponentials and multidimensional change of variables are not proved in this companion.