Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Bounded Linear Maps and Bounded Linear Functionals on Real Inner Product Spaces, and the Operator Norm
definitiondef:bounded-linear-map-inner-product-2026aAnalysisLinear AlgebraDefines bounded linear maps between real inner product spaces, the spaces L(E,F) and L(E), the operator norm as an infimum, and bounded linear functionals with their norm.Orthogonal Projection onto a Closed Linear Subspace of a Real Hilbert Space
corollarycor:orthogonal-projection-closed-subspace-2026aAnalysisLinear AlgebraFor a closed linear subspace M of a real Hilbert space, the nearest-point map P_M is linear and idempotent, characterised by x-P_M x being orthogonal to M, satisfies Pythagoras, and yields H = M + M^perp; a subspace is dense iff its orthogonal complement is trivial.Nearest-Point Projection onto a Nonempty Closed Convex Subset of a Real Hilbert Space
theoremthm:projection-closed-convex-hilbert-2026aAnalysisEvery point of a real Hilbert space has a unique nearest point in a nonempty closed convex set, characterised by a variational inequality; the projection is nonexpansive.Orthogonality, Orthogonal Complement and Orthonormal Families in a Real Inner Product Space
definitiondef:orthogonality-real-inner-product-2026aAnalysisLinear AlgebraDefines orthogonal vectors, the orthogonal complement of a subset, and orthonormal tuples and sequences in a real inner product space.Convex Subset of a Vector Space over the Real Numbers
definitiondef:convex-subset-real-vector-space-2026aAnalysisLinear AlgebraA subset of a real vector space is convex if it contains the segment tx+(1-t)y between any two of its points.- A real Hilbert space is a real inner product space that is complete for its norm metric; fixes the topological vocabulary (open, closed, dense, bounded, convergent, Cauchy) used for inner product spaces and the notion of closed linear subspace.
The Norm Metric of a Real Inner Product Space: Triangle Inequalities, Limits and Continuity
lemmalem:real-inner-product-metric-2026aAnalysisThe triangle and reverse triangle inequalities, that d(x,y)=|x-y| is a metric, the algebra of limits, sequential continuity of the inner product and norm, the description of bounded sets, and Lipschitz continuity of the norm and of the maps x -> <x,z>.The Cauchy-Schwarz Inequality in a Real Inner Product Space
theoremthm:cauchy-schwarz-real-2026aAnalysisLinear AlgebraIn a real inner product space, |<x,y>| is at most |x||y|.Elementary Identities in a Real Inner Product Space
lemmalem:real-inner-product-identities-2026aAnalysisLinear AlgebraBilinearity in the second argument, behaviour of the zero vector, vanishing and homogeneity of the norm, the expansions of |x±y|^2, the parallelogram law and the polarisation identity.- Defines real inner product spaces, the norm |x| as the nonnegative square root of <x,x>, and the distance d(x,y)=|x-y|.
Perron's Method: Existence of a Viscosity Solution of the Dirichlet Problem
theoremthm:perron-existence-2026aAnalysisPDEIf comparison holds for the Dirichlet problem and there are a bounded subsolution and a bounded supersolution whose envelopes attain the boundary data, then the supremum of all subsolutions between them is a viscosity solution of the Dirichlet problem.The Bump Construction: Raising a Subsolution Whose Lower Envelope Fails the Supersolution Inequality
lemmalem:perron-bump-2026aAnalysisPDEIf the lower semicontinuous envelope of a viscosity subsolution fails the supersolution inequality at an interior point, then the subsolution can be raised strictly somewhere near that point, by a modification supported in an arbitrarily small ball, without losing the subsolution…The Maximum of Two Viscosity Subsolutions is a Viscosity Subsolution
corollarycor:max-two-subsolutions-2026aAnalysisPDEThe pointwise maximum of two viscosity subsolutions of a continuous second-order equation operator is again a viscosity subsolution.The Upper Semicontinuous Envelope of a Supremum of Viscosity Subsolutions is a Viscosity Subsolution
lemmalem:sup-of-subsolutions-2026aAnalysisPDEIf a nonempty family of viscosity subsolutions of a continuous second-order equation operator is locally uniformly bounded above, then the upper semicontinuous envelope of its pointwise supremum is again a viscosity subsolution.A Viscosity Solution of the Dirichlet Problem is Continuous and Attains the Boundary Data
propositionprop:dirichlet-solution-basic-2026aAnalysisPDEA viscosity solution of the Dirichlet problem equals the boundary data on the boundary, is continuous on the closure, and restricts to a viscosity solution of the equation on the open set.Viscosity Sub- and Supersolutions and Solutions of the Dirichlet Problem
definitiondef:dirichlet-problem-viscosity-2026aAnalysisPDEA viscosity subsolution of the Dirichlet problem is a viscosity subsolution up to the boundary that lies below the boundary data there; dually for supersolutions, and a solution is both.The Viscosity Sub- and Supersolution Properties are Local
lemmalem:viscosity-subsolution-local-2026aAnalysisPDEA viscosity subsolution restricts to a viscosity subsolution on any open subset, and conversely a function that is a viscosity subsolution on an open neighbourhood of each point of the domain is a viscosity subsolution on the whole domain. The same holds for supersolutions.Sequential Form of the Continuity of a Second-Order Equation Operator
lemmalem:operator-sequential-continuity-2026aAnalysisPDEIf a second-order equation operator is continuous at a quadruple and each of the four arguments is approached by a convergent sequence, then the values of the operator converge to its value at that quadruple.Restriction of a Second-Order Equation Operator to an Open Subset
lemmalem:operator-restriction-2026aAnalysisPDERestricting the spatial variable of a second-order equation operator to an open subset again gives a second-order equation operator, and degenerate ellipticity and continuity are inherited.Continuity of the Value, Gradient and Hessian Maps of a Differentiable Function
lemmalem:test-data-continuous-2026aAnalysisMultivariable CalculusFor a function of class the gradient map is continuous, and for a function of class both the gradient map into and the Hessian map into the symmetric matrices with their norm distance are continuous.