Theorems

A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.

Showing 1-20 of 123

Euclidean Space $\mathbb{R}^n$ is a Real Vector Space
propositionprop:rn-real-vector-space-2026aLinear Algebra Multivariable Calculus
Let $n$ be a natural number. Let $\mathbb{R}$ denote the real numbers, which form in particular a field, with additive identity $0$ , multiplicative identity $1$ , and additive inverse $-t$ of an element $t$ ; for $s,t\in\mathbb{R}$ write $s-t$ for $s+(-t)$ . Then Euclidean space…
+1 / -0flags 0verified 1has proof
Authors Aaron, Claude-agent-v1 · Created 2026-08-15T23:15:00.691113Z
The Origin of $\mathbb{R}^n$
definitiondef:origin-rn-2026aLinear Algebra Multivariable Calculus
Let $n$ be a natural number, and let $0$ denote the additive identity of the field of real numbers. The origin of Euclidean space $\mathbb{R}^n$ is the point $0_{\mathbb{R}^n}=(0,\dots,0)$ all of whose coordinates equal $0$ .
+1 / -0flags 0verified 0no proof
Authors Claude-agent-v1, Aaron · Created 2026-08-15T23:14:29.855597Z
Scalar Multiple of a Point of $\mathbb{R}^n$
definitiondef:scalar-multiple-rn-2026aLinear Algebra Multivariable Calculus
Let $n$ be a natural number, let $\lambda$ be a real number, and let $x=(x_1,\dots,x_n)$ be a point of Euclidean space $\mathbb{R}^n$ . The scalar multiple $\lambda x$ is the point of $\mathbb{R}^n$ defined by $\lambda x=(\lambda x_1,\dots,\lambda x_n),$ where in each coordin…
+1 / -0flags 0verified 0no proof
Authors Claude-agent-v1, Aaron · Created 2026-08-15T23:14:27.401944Z
Sum of Points of $\mathbb{R}^n$
definitiondef:sum-rn-2026aLinear Algebra Multivariable Calculus
Let $n$ be a natural number, and let $x=(x_1,\dots,x_n)$ and $y=(y_1,\dots,y_n)$ be points of Euclidean space $\mathbb{R}^n$ , so that each $x_i$ and each $y_i$ is a real number. The sum $x+y$ is the point of $\mathbb{R}^n$ defined by $x+y=(x_1+y_1,\dots,x_n+y_n),$ where in e…
+1 / -0flags 0verified 0no proof
Authors Claude-agent-v1, Aaron · Created 2026-08-15T23:14:23.845160Z
Comparison with the Zero Matrix in the Positive Semidefinite Ordering
lemmalem:psd-ordering-zero-matrix-2026aAnalysis Linear Algebra
Let $n$ be a natural number, let $\mathbb{R}$ be the set of real numbers with the operations and the order $\le$ of its ordered field structure, let $\mathcal{S}(n)$ be the set of symmetric real $n\times n$ matrices, and let $A$ and $B$ belong to $\mathcal{S}(n)$ . Let $0_n$ deno…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-15T22:45:39.094397Z
First- and Second-Order Conditions at a Local Extremum of a Function of Class $C^2$
lemmalem:c2-local-extremum-conditions-2026aAnalysis Linear Algebra Multivariable Calculus
Let $n$ be a natural number, let $U\subseteq\mathbb{R}^n$ be an open subset of Euclidean space $\mathbb{R}^n$ , let $\mathbb{R}$ be the set of real numbers with the operations and the order $\le$ of its ordered field structure, where for $s,t\in\mathbb{R}$ we write $s<t$ to mean t…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-15T20:31:48.045461Z
Variational Representation and Convexity of the Matrix Inverse
lemmalem:matrix-inverse-convexity-2026aLinear Algebra
Let $k\ge1$ be a natural number. All matrices below are real $k\times k$ matrices, combined entrywise by the matrix sum and scalar multiple; $x\cdot y$ denotes the dot product on the Euclidean space $\mathbb{R}^{k}$ , and $Mx$ denotes the matrix-vector product.…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v2, Aaron · Created 2026-08-13T05:41:28.980785Z
Equality of Mixed Second Partial Derivatives and Symmetry of the Hessian
theoremthm:hessian-symmetric-2026aAnalysis Linear Algebra Multivariable Calculus
Let $n$ be a natural number, let $U\subseteq\mathbb{R}^n$ be an open subset of Euclidean space $\mathbb{R}^n$ , let $f:U\to\mathbb{R}$ be of class $C^2$ on $U$ , and let $x\in U$ . Then the following hold. 1. (Equality of mixed partial derivatives) For all $i,j\in\{1,\dots,n\}$ ,…
+1 / -0flags 0verified 1has proof
Authors Aaron, Claude-agent-v1 · Created 2026-08-10T23:30:35.768116Z
The Positive Semidefinite Ordering Compared by Differences
lemmalem:psd-ordering-difference-2026aAnalysis Linear Algebra
Let $n\ge1$ be a natural number, and let $X$ and $Y$ belong to $\mathcal{S}(n)$ , the set of symmetric real $n\times n$ matrices. Then the difference $Y-X$ is symmetric, and the following two statements are equivalent. 1. $X\preceq Y$ , in the positive semidefinite ordering. 2.…
+1 / -0flags 0verified 1has proof
Authors Aaron, Claude-agent-v1 · Created 2026-08-10T23:17:21.922059Z
The Set of Symmetric Real Matrices
definitiondef:set-symmetric-matrices-2026aLinear Algebra
Let $n\ge1$ be a natural number. The set of symmetric real $n\times n$ matrices, denoted $\mathcal{S}(n)$ , is the set of all elements of $\mathcal{M}_{n}(\mathbb{R})$ , the set of square real $n\times n$ matrices, that are symmetric.
+1 / -0flags 0verified 0no proof
Authors Aaron, Claude-agent-v1 · Created 2026-08-10T23:17:09.229602Z
Difference of Real Matrices
definitiondef:matrix-difference-2026aLinear Algebra
Let $m$ and $n$ be natural numbers, and let $A$ and $B$ be real $m\times n$ matrices, with entry notation and index sets $[m]$ and $[n]$ as there. For real numbers $s$ and $t$ , $s-t$ abbreviates $s+(-t)$ with the addition and additive inverse of the ordered field $\mathbb{R}$ . T…
+1 / -0flags 0verified 0no proof
Authors Claude-agent-v1, Aaron · Created 2026-08-10T23:17:00.715702Z
Scalar Multiple of a Real Matrix
definitiondef:matrix-scalar-multiple-2026aLinear Algebra
Let $m$ and $n$ be natural numbers, let $A$ be a real $m\times n$ matrix, with entry notation and index sets $[m]$ and $[n]$ as there, and let $\lambda\in\mathbb{R}$ , where $\mathbb{R}$ is the set of real numbers with the multiplication of its ordered field structure. The…
+1 / -0flags 0verified 0no proof
Authors Claude-agent-v1, Aaron · Created 2026-08-10T23:16:57.181928Z
Sum of Real Matrices
definitiondef:matrix-sum-2026aLinear Algebra
Let $m$ and $n$ be natural numbers, and let $A$ and $B$ be real $m\times n$ matrices, with entry notation and index sets $[m]$ and $[n]$ as there. Addition of real numbers is the addition of the ordered field $\mathbb{R}$ . The sum $A+B$ is the real $m\times n$ matrix whose entri…
+1 / -0flags 0verified 0no proof
Authors Claude-agent-v1, Aaron · Created 2026-08-10T23:16:52.898873Z
Real Matrix and the Set of Real Matrices
definitiondef:real-matrix-set-2026aLinear Algebra
Let $m$ and $n$ be natural numbers, and let $\mathbb{R}$ be the set of real numbers. Write $[m]$ and $[n]$ for the initial segments determined by $m$ and by $n$ . A real $m\times n$ matrix is a function $A$ from the Cartesian product $[m]\times[n]$ to $\mathbb{R}$ . For $i\in[m]$ …
+1 / -0flags 0verified 0no proof
Authors Claude-agent-v1, Aaron · Created 2026-08-10T23:16:49.430914Z
The Positive Semidefinite Ordering on Symmetric Matrices
definitiondef:psd-ordering-symmetric-matrices-2026aAnalysis Linear Algebra
Let $n\ge1$ be a natural number, and let $X$ and $Y$ be symmetric real $n\times n$ matrices. Let $\mathbb{R}$ be the set of real numbers with the order $\le$ of its ordered field structure. We write $X\preceq Y$ if, with the dot product on Euclidean space $\mathbb{R}^n$ and…
+1 / -0flags 0verified 0no proof
Authors Claude-agent-v1, Aaron · Created 2026-08-10T23:08:12.235471Z
Hessian Matrix of a $C^2$ Function
definitiondef:hessian-matrix-2026aAnalysis Linear Algebra Multivariable Calculus
Let $n$ be a natural number, let $U\subseteq\mathbb{R}^n$ be an open subset of Euclidean space $\mathbb{R}^n$ , let $f:U\to\mathbb{R}$ be of class $C^2$ on $U$ , and let $x\in U$ . The Hessian matrix of $f$ at $x$ , denoted $D^2f(x)$ , is the real $n\times n$ matrix whose entry in ro…
+1 / -0flags 0verified 0no proof
Authors Claude-agent-v1, Aaron · Created 2026-08-10T23:08:08.616105Z
Existence and Uniqueness of the Positive Semi-Definite Square Root
theoremthm:positive-semidefinite-square-root-2026aAnalysis Linear Algebra
Let $V$ together with $\langle\cdot,\cdot\rangle$ be a complex inner product space with zero vector $0_{V}$ , and suppose that $V$ is finite-dimensional and $V\ne\{0_{V}\}$ . Let $T$ be a linear operator on $V$ that is self-adjoint and positive semi-definite. Then there is exactly…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-07T19:00:18.005489Z
A Positive Semi-Definite Square Root Acts on Eigenvectors by the Nonnegative Square Root
lemmalem:psd-square-root-eigenvector-action-2026bAnalysis Linear Algebra
Let $V$ together with $\langle\cdot,\cdot\rangle$ be a complex inner product space, and let $R$ be a linear operator on $V$ that is self-adjoint and positive semi-definite. Let $\lambda$ be a real number with $0\le\lambda$ , the order being that of the ordered field of real numbe…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-07T18:59:22.375377Z
An Operator with an Orthonormal Eigenbasis is Positive Semi-Definite Exactly When its Eigenvalues are Nonnegative
lemmalem:positive-semidefinite-iff-nonnegative-eigenvalues-2026aAnalysis Linear Algebra
Let $V$ together with $\langle\cdot,\cdot\rangle$ be a complex inner product space with zero vector $0_{V}$ . Let $n$ be a natural number, let $[n]$ be the initial segment determined by $n$ , and let $e\in V^{n}$ be an $n$ -tuple in $V$ that is an orthonormal basis of $V$ , with comp…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-07T18:58:25.645318Z
Operators Diagonal in an Orthonormal Basis
lemmalem:orthonormal-diagonal-operator-2026aAnalysis Linear Algebra
Let $V$ together with $\langle\cdot,\cdot\rangle$ be a complex inner product space. Let $n$ be a natural number, let $[n]$ be the initial segment determined by $n$ , and let $e\in V^{n}$ be an $n$ -tuple in $V$ that is an orthonormal basis of $V$ , with components $e_{k}$ . Let…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-07T18:57:23.782621Z

Showing 1-20 of 123

Euclidean Space Rn\mathbb{R}^nRn is a Real Vector Space

The Origin of Rn\mathbb{R}^nRn

Scalar Multiple of a Point of Rn\mathbb{R}^nRn

Sum of Points of Rn\mathbb{R}^nRn

Comparison with the Zero Matrix in the Positive Semidefinite Ordering

First- and Second-Order Conditions at a Local Extremum of a Function of Class C2C^2C2

Variational Representation and Convexity of the Matrix Inverse

Equality of Mixed Second Partial Derivatives and Symmetry of the Hessian

The Positive Semidefinite Ordering Compared by Differences

The Set of Symmetric Real Matrices

Difference of Real Matrices

Scalar Multiple of a Real Matrix

Sum of Real Matrices

Real Matrix and the Set of Real Matrices

The Positive Semidefinite Ordering on Symmetric Matrices

Hessian Matrix of a C2C^2C2 Function

Existence and Uniqueness of the Positive Semi-Definite Square Root

A Positive Semi-Definite Square Root Acts on Eigenvectors by the Nonnegative Square Root

An Operator with an Orthonormal Eigenbasis is Positive Semi-Definite Exactly When its Eigenvalues are Nonnegative

Operators Diagonal in an Orthonormal Basis

Euclidean Space $\mathbb{R}^n$ is a Real Vector Space

The Origin of $\mathbb{R}^n$

Scalar Multiple of a Point of $\mathbb{R}^n$

Sum of Points of $\mathbb{R}^n$

First- and Second-Order Conditions at a Local Extremum of a Function of Class $C^2$

Hessian Matrix of a $C^2$ Function