Mizar Commentary on Walter Rudin's Principles of Mathematical Analysis/Functions of Several Variables

Linear Transformations

9.1 Definition
(a) Compare 1.36 Definitions (for vector spaces). Aside from that, REAL-NS n as a normed space is defined in REAL_NS1:def 4 and TOP-REAL n as a topological space is defined in EUCLID:def 8. (There is also REAL-US n (REAL_NS1:def 6).) Note that these are not a VectSp (compare NORMSTR (NORMSP_1), RLTopStruct (RLTOPSP1) and ModuleStr (VECTSP_1) in the second diagram here). RLSStruct (RLVECT_1) is incorporated into both NORMSTR and RLTopStruct and delivers most properties for both variants. RLS can be seen as a abbreviation of Real Linear Scalar. The RLSStruct variant of REAL n (EUCLID:def 1) would be RealVectSpace(Seg n) (FUNCSDOM:def 6 and FINSEQ_1:def 1). Note that there is CLSStruct (CLVECT_1) which will not be discussed here.
(b) A Linear_Combination of $R^{k}$ (RLVECT_2:def 3) is given as a function, sending the vectors to their associated scalars. Lin(S) (RLVECT_3:def 2) is the span of $S$. More generally, a Linear_Combination of a vector space is defined in VECTSP_6:def 1 and Lin(S) in VECTSP_7:def 2.
(c) Lineary independence is defined in RLVECT_3:def 1 or more generally in VECTSP_7:def 1.
(d) dim X is defined in RLVECT_5:def 2 or more generally in VECTSP_9:def 1. The remark is given by RLVECT_5:32 or VECTSP_9:29.
(e) The Basis of X is defined in RLVECT_3:def 3 or more generally in VECTSP_7 via VECTSP_7:def 3. No reference for the remark or the standard basis.

9.2 Theorem No reference.

Corollary is EUCLID_7:46 for RealVectSpace(Seg n), RLAFFIN3:4 for TOP-REAL n and EUCLID_7:51 for REAL-US n, else no reference.

9.3 Theorem
(a) No reference, but see RLVECT_5:29.
(b) is given by existence property of the definition of a basis (see RLVECT_3:def 3).
(c) is given by RLVECT_3:26 or RLVECT_5:2.

9.4 Definition
For VectSp $A$ is a linear-transformation (RANKNULL) if it is a additive (VECTSP_1:def 19), homogeneous (MOD_2:def 2) function.
For RealLinearSpace $A$ is a LinearOperator (LOPBAN_1) if it is a additive (VECTSP_1:def 19), homogeneous (LOPBAN_1:def 5) function.

9.5 Theorem No reference.

9.6 Definitions
(a) For RealLinearSpace $L(X,Y)$ is LinearOperators(X,Y) (LOPBAN_1:def 6), no reference fro VectSp. The addition of functions from $X$ to $Y$ is generally given by FuncAdd(X,Y) (LOPBAN_1:def 1, but also see FUNCT_3:def 7, FUNCOP_1:def 3 and the redefinition of the latter in FUNCSDOM to understand the definition; or look at LOPBAN_1:1). Skalar multiplication of functions is only given for RealLinearSpace by FuncExtMult(X,Y) (LOPBAN_1:def 2), else no reference.
(b) Composition was already defined RELAT_1:def 8. Additivity of the composition is clustered in GRCAT_1 (see also GRCAT_1:7). Homogeneity of the composition is only given for the one defined in MOD_2:def 2, given by MOD_2:2, else no reference. However, the combination for RealLinearSpace is given by LOPBAN_2:1.
(c) For a bounded operator $A$ between two RealNormSpace (NORMSP_1) $X$ and $Y$ the norm $||A||$ is given by BoundedLinearOperatorsNorm(X,Y).A (LOPBAN_1:def 13), before it is packed into R_NormSpace_of_BoundedLinearOperators (LOPBAN_1:def 14). The first inequality is given by LOPBAN_1:32, no reference for the second inequality. No reference for VectSp either.

9.7 Theorem (for VectSp) No reference.

9.7 Theorem (for RealNormSpace)
(a) The first part is given implicitly by LOPBAN_1:27, the second one is given by LOPBAN_8:3.
(b) First part is LOPBAN_1:37. The distance function is generally given by NORMSP_2:def 1 and the generated metric space by NORMSP_2:def 2.
(c) is LOPBAN_2:2.

9.8 Theorem No reference.

9.9 Matrices No reference.

Differentiation

9.10 Preliminaries
The new viewpoint on differentiation is the one Mizar starts with, see 5.1 Definition and FDIFF_1.

9.11 Definition
The notations are the same as for differentiation of real functions:
$f$ is differentiable at $x$ means f is_differentiable_in x (NDIFF_1:def 6), $f'(x)$ is diff(f,x) (NDIFF_1:def 7). $f$ is differentiable on $E$ means f is_differentiable_on E (NDIFF_1:def 8), $f'$ is f`|E (NDIFF_1:def 9). See also PDIFF_1:def 7/8.

9.12 Theorem is given by the uniqueness property of NDIFF_1:def 7.

9.13 Remark
(a) Basically given by NDIFF_1:47.
(b) Given by the types of NDIFF_1:def 7 and NDIFF_1:def 9.
(c) is NDIFF_1:44/45.
(d) Nothing to formalize.

9.14 Example No reference, but NDIFF_1:43 is similar.

9.15 Theorem is NDIFF_2:13.

9.16 Partial derivates
$(D_{j}f_{i})(x)$ is partdiff(f,x,j,i) (PDIFF_1:def 16). The use of e_j and u_i is avoided by using reproj(j,x) (PDIFF_1:def 5/6) and Proj(i,m) (PDIFF_1:def 4) respectively.

9.17 Theorem No reference.

9.18 Example No reference.

9.19 Theorem No reference.

Corollary No reference.

9.20 Definition No reference.

9.21 Theorem is PDIFF_8:20-22.

The Contraction Principle

9.22 Definition is ALI2:def 1 for MetrSpace and NFCONT_2:def 3 for NORMSTR.

9.23 Theorem is ALI2:1 for MetrSpace and NFCONT_2:14 for RealBanachSpace.

The Inverse Function Theorem

9.24 Theorem No reference.

9.25 Theorem No reference.

The Implicit Function Theorem

9.26 Notation

9.27 Theorem

9.28 Theorem

9.29 Example No reference.