FARMS001
Optimality of truncated SVD
SVD truncation attains the optimal rank-k error in spectral and Frobenius norms.
Source label: thm:best-rank-k-approximationAcceptedRead the mathematical statement & Lean
Formalization
Explorer.
Explore accepted mathematical statements, their assumptions and their Lean representations.
All 157 accepted formalizations from four mathematical sources, including three with source warnings explained on their pages.
002
Cumulative distribution function
The distribution function assigns the probability of a threshold event to each real threshold.
Source label: def:cumulative-distribution-functionAcceptedRead the mathematical statement & Lean
003
Expected Frobenius norm after column sampling
Uniform sampling with rescaling preserves the squared Frobenius norm in expectation.
Source label: lem:FNormExpAcceptedRead the mathematical statement & Lean
004
Frobenius norm and the trace identity
The Frobenius norm is the square root of the sum of squared matrix entries.
Source label: def:frobenius-normAcceptedRead the mathematical statement & Lean
005
Full singular value decomposition
A full SVD expresses a rectangular matrix through orthogonal bases and ordered singular values.
Source label: def:full-svdAcceptedRead the mathematical statement & Lean
006
Hoeffding inequality for bounded independent variables
A two-sided exponential bound controls the deviation of a sum from its expectation.
Source label: lem:hoefAcceptedRead the mathematical statement & Lean
007
Hadamard mixing of an orthonormal basis
Random sign mixing followed by a Hadamard transform spreads the row energy of an orthonormal basis.
Source label: lem:HUAcceptedRead the mathematical statement & Lean
008
Hadamard mixing of the leading right singular subspace
The leading k-dimensional subspace has uniformly bounded row energy after randomized Hadamard mixing.
Source label: lem:HUnewAcceptedRead the mathematical statement & Lean
009
Deterministic low-rank sampling inequality
Projection onto a sampled column space controls the loss of the leading rank-k component.
Source label: lem:mainlemma_generalAcceptedRead the mathematical statement & Lean
010
Pythagoras identity for matrices
Orthogonal matrix components have additive squared Frobenius norms.
Source label: l_pythAcceptedRead the mathematical statement & Lean
011
Entrywise expectation and variance of sampled multiplication
The source states unbiasedness and an entrywise variance bound for sampled matrix multiplication.
Source label: lem:multexpvarAccepted with source warningRead the mathematical statement & Lean
012
Axioms of a matrix norm
A matrix norm is characterized by definiteness, the triangle inequality and absolute homogeneity.
Source label: def:normAcceptedRead the mathematical statement & Lean
013
Concentration of a sampled second-moment matrix
An empirical second-moment matrix concentrates around its expectation in spectral norm.
Source label: lem:oliveiraAcceptedRead the mathematical statement & Lean
014
Orthonormal matrices preserve Euclidean length
Multiplication by a matrix with orthonormal columns preserves the Euclidean norm.
Source label: thm:orthonormal-isometryAcceptedRead the mathematical statement & Lean
015
Probability mass function
The mass at a real value is the probability that a random variable equals that value.
Source label: def:probability-mass-functionAcceptedRead the mathematical statement & Lean
016
Error decomposition for a sampled low-rank approximation
The approximation error splits into a sampled-subspace loss and the optimal rank-k tail.
Source label: l_aux2AcceptedRead the mathematical statement & Lean
017
Pythagoras identity and vector orthogonality
Orthogonality is equivalent to additivity of squared Euclidean norms.
Source label: thm:pythagorasAcceptedRead the mathematical statement & Lean
018
Best rank-k approximation within a sampled column space
Truncating the compressed matrix gives the best rank-k approximation within the selected column space.
Source label: lem:restateAcceptedRead the mathematical statement & Lean
019
Singular-value preservation under Hadamard row sampling
Uniform row sampling preserves the singular values of a mixed orthonormal basis with probability at least 0.95.
Source label: lem:sample_lem20pfAcceptedRead the mathematical statement & Lean
020
Control of the sketched least-squares cross term
The interaction between the sketched basis and the orthogonal residual is small with conditional probability at least 0.9.
Source label: lem:sample_lem40pfAcceptedRead the mathematical statement & Lean
021
Pseudoinverse stability of the sampled leading subspace
On the row-energy event, a sampled subspace's pseudoinverse is close to its transpose.
Source label: lem:sample_lem40pfn1AcceptedRead the mathematical statement & Lean
022
Tail error from pseudoinverse perturbation
The pseudoinverse correction contributes a controlled Frobenius error in the discarded singular subspace.
Source label: lem:sample_lem40pfn2AcceptedRead the mathematical statement & Lean
023
Tail interaction with the sampled leading subspace
A sampled cross term between retained and discarded singular directions is small with probability at least 0.95.
Source label: lem:sample_lem40pfn3AcceptedRead the mathematical statement & Lean
024
Relative-error guarantee for RandLowRank
A sufficient sample count gives a relative Frobenius-error guarantee with probability at least 0.85.
Source label: lem:sample_lem40pfn4AcceptedRead the mathematical statement & Lean
025
Sufficient sketch conditions for least squares
Two geometric sketch conditions control both residual error and solution error.
Source label: lem:suff_condAcceptedRead the mathematical statement & Lean
026
Relative solution error for sketched least squares
A lower bound on the projected right-hand side turns the sketch's error estimate into a relative solution bound.
Source label: lem:suff_cond2AcceptedRead the mathematical statement & Lean
027
Spectral accuracy of leverage-based row sampling
Sampling an orthonormal matrix with suitable row probabilities approximately preserves its Gram matrix.
Source label: thm:theorem7correctAcceptedRead the mathematical statement & Lean
028
Thin singular value decomposition
A thin SVD retains precisely the singular directions associated with nonzero singular values.
Source label: def:thin-svdAcceptedRead the mathematical statement & Lean
029
Gaussian a posteriori spectral-norm estimate
A small collection of Gaussian probes gives a probabilistic upper bound on a fixed matrix norm.
Source label: thm:aposterioriAcceptedRead the mathematical statement & Lean
030
Expected Frobenius error of Gaussian rangefinding
Gaussian rangefinding controls expected Frobenius error by the optimal singular-value tail.
Source label: thm:avg-frob-error-gaussAcceptedRead the mathematical statement & Lean
031
Expected spectral error of Gaussian rangefinding
The expected residual combines the next singular value with a Frobenius-tail contribution.
Source label: thm:avg-spec-error-gaussAcceptedRead the mathematical statement & Lean
032
Bidiagonal representation of a Gaussian matrix
A rectangular Gaussian matrix admits an orthogonally equivalent bidiagonal representation.
Source label: prop:bidiagAcceptedRead the mathematical statement & Lean
033
Moment bound for a chi-square variable
The source bounds the Lq moment of a chi-square variable by its degrees of freedom plus q.
Source label: lem:chisq-momentAcceptedRead the mathematical statement & Lean
034
Exact positive and negative chi-square moments
Gamma-function identities give positive and negative moments of a chi-square variable.
Source label: prop:chisq-moment-exactAcceptedRead the mathematical statement & Lean
035
Unitary change of coordinates for a projector
Orthogonal projection transforms naturally under a unitary change of coordinates.
Source label: prop:conj-projAcceptedRead the mathematical statement & Lean
036
Congruence preserves positive semidefinite order
Multiplying on both sides by a matrix and its adjoint preserves positive semidefiniteness and order.
Source label: prop:conjugationAcceptedRead the mathematical statement & Lean
037
Error bound for SVD via row extraction
The source bounds the spectral error of an SVD assembled through an interpolative decomposition.
Source label: lem:convert_IDAccepted with source warningRead the mathematical statement & Lean
038
Frobenius second moment of a Gaussian matrix product
The root mean square Frobenius norm of SGT factors into the Frobenius norms of S and T.
Source label: prop:gauss-frob-expectAcceptedRead the mathematical statement & Lean
039
Expected norms of a Gaussian pseudoinverse
Oversampling controls both the Frobenius second moment and the expected spectral norm of a Gaussian pseudoinverse.
Source label: prop:gauss-inv-expectAcceptedRead the mathematical statement & Lean
040
Two tail bounds for a Gaussian pseudoinverse
Polynomial tail estimates control large Frobenius and spectral norms of a Gaussian pseudoinverse.
Source label: prop:gauss-inv-tailsAcceptedRead the mathematical statement & Lean
041
Expected spectral norm of a Gaussian matrix product
The expected spectral norm of SGT is controlled by mixed spectral and Frobenius norms.
Source label: prop:gauss-spec-expectAcceptedRead the mathematical statement & Lean
042
Moment bound for an inverse chi-square variable
A restricted range of moments controls the reciprocal of a chi-square variable.
Source label: lem:inv-chisq-momentAcceptedRead the mathematical statement & Lean
043
Exact Frobenius second moment of a Gaussian pseudoinverse
The expected squared Frobenius norm has a closed form determined by the rectangular dimensions.
Source label: prop:inv-gauss-frob-expectAcceptedRead the mathematical statement & Lean
044
Tail of the squared Frobenius norm of a Gaussian pseudoinverse
A rectangular dimension gap controls the tail of the squared Frobenius norm.
Source label: thm:inv-gauss-frob-tailAcceptedRead the mathematical statement & Lean
045
Expected spectral norm of a rectangular Gaussian pseudoinverse
A positive rectangular dimension gap bounds the expected spectral norm of the pseudoinverse.
Source label: prop:inv-gauss-spec-expectAcceptedRead the mathematical statement & Lean
046
Spectral tail of a rectangular Gaussian pseudoinverse
The pseudoinverse spectral norm has a polynomial upper-tail bound governed by the dimension gap.
Source label: prop:inv-gauss-spec-tailAcceptedRead the mathematical statement & Lean
047
Expected spectral error of randomized SVD
Randomized SVD with power iteration approximates A with an expected error proportional to its next singular value.
Source label: thm:mainAcceptedRead the mathematical statement & Lean
048
Deterministic rangefinder error bound
A full-row-rank leading sample block yields a deterministic projection-error estimate.
Source label: thm:main-error-bdAcceptedRead the mathematical statement & Lean
049
Positive semidefinite inverse perturbation inequality
A positive semidefinite perturbation bounds the change from the identity to its shifted inverse.
Source label: prop:perturb-invAcceptedRead the mathematical statement & Lean
050
Expected spectral error after power iteration
Power iteration sharpens the expected spectral error of a Gaussian rangefinder.
Source label: cor:power-method-spec-gaussAcceptedRead the mathematical statement & Lean
051
Projection bound through matrix powers
A projected matrix norm is controlled by a powered matrix expression.
Source label: prop:proj-powerAcceptedRead the mathematical statement & Lean
052
Monotonicity under enlargement of a projection space
A larger projection space increases the captured norm and decreases the residual norm.
Source label: prop:proj-rangeAcceptedRead the mathematical statement & Lean
053
Frobenius and spectral estimates for a scaled Gaussian matrix
Fixed left and right factors give complementary Frobenius and spectral estimates for SGT.
Source label: prop:scaled-gaussAcceptedRead the mathematical statement & Lean
054
Spectral norm of a positive semidefinite block matrix
The diagonal block norms bound the norm of a positive semidefinite block matrix.
Source label: prop:spec-norm-sumAcceptedRead the mathematical statement & Lean
055
Approximation error of an SRFT rangefinder
A subsampled randomized Fourier transform yields simultaneous spectral and Frobenius residual bounds.
Source label: thm:SRFTAcceptedRead the mathematical statement & Lean
056
Singular values of an SRFT embedding
An SRFT preserves an orthonormal subspace's extreme singular values with high probability.
Source label: thm:SRFT-spec-bdAcceptedRead the mathematical statement & Lean
057
Frobenius tail bound for Gaussian rangefinding
Two deviation parameters control the Frobenius residual of a Gaussian rangefinder.
Source label: thm:tail-frob-error-gaussAcceptedRead the mathematical statement & Lean
058
Explicit spectral-error probabilities for Gaussian rangefinding
Two choices of tail parameters give explicit spectral-error bounds with exponentially small failure probabilities.
Source label: cor:tail-spec-error-gaussAcceptedRead the mathematical statement & Lean
059
Spectral tail bound for Gaussian rangefinding
A spectral residual bound separates the next singular value, the tail energy and a deviation term.
Source label: thm:tail-spec-error-gaussAcceptedRead the mathematical statement & Lean
060
Error after truncating a projected approximation
A best rank-k truncation of a projected matrix adds at most the next singular value to the projection error.
Source label: thm:truncationAcceptedRead the mathematical statement & Lean
061
Preconditioned conjugate gradients for a graph Laplacian
A sparse approximate Cholesky factor gives an iteration and arithmetic-cost bound for consistent Laplacian systems.
Source label: cor:laplacian-solverAcceptedRead the mathematical statement & Lean
062
Expectation and tail bounds for matrix sampling
Averages of bounded independent matrix samples approximate their mean in spectral norm.
Source label: thm:mtx-samplingAcceptedRead the mathematical statement & Lean
063
Residual inequality for Hermitian powers
Powering a Gram matrix controls the original projection residual.
Source label: lem:poweringAcceptedRead the mathematical statement & Lean
064
Expected eigenvalue error of randomized Krylov iteration
A Gaussian start gives gap-free and gap-dependent bounds for the leading eigenvalue estimate.
Source label: thm:rand-krylovAcceptedRead the mathematical statement & Lean
065
Expected spectral error of randomized Nyström approximation
The source relates Nyström approximation error to the eigenvalue tail of a positive semidefinite matrix.
Source label: Theorem rand-nysAccepted with source warningRead the mathematical statement & Lean
066
Expected eigenvalue error of randomized power iteration
A Gaussian start gives two expected relative-error estimates for the largest eigenvalue.
Source label: thm:rand-powerAcceptedRead the mathematical statement & Lean
067
Cost of randomized HBS construction
An HBS-compressible matrix admits a randomized construction with separate application, entry-access and arithmetic costs.
Source label: thm:randHBSAcceptedRead the mathematical statement & Lean
068
Deterministic spectral error of a rangefinder
The next singular value and a trailing-subspace interaction bound the rangefinder residual.
Source label: thm:rrf-deterministicAcceptedRead the mathematical statement & Lean
069
Expected error of a Gaussian rangefinder
A Gaussian test matrix controls spectral residual error through the next singular value and the singular-value tail.
Source label: thm:rrf-gaussAcceptedRead the mathematical statement & Lean
070
Monotonicity of rangefinder error in semidefinite order
Ordering the input Gram matrices orders the squared residual matrices for a fixed test matrix.
Source label: cor:rrf-monotoneAcceptedRead the mathematical statement & Lean
071
Gaussian power-rangefinder moment bound
A power rangefinder controls expected spectral error through a higher error moment.
Source label: cor:rrf-power-gaussAcceptedRead the mathematical statement & Lean
072
Rangefinder error as a Schur complement
The Gram matrix of a projection residual equals a generalized Schur complement.
Source label: prop:rrf-schurAcceptedRead the mathematical statement & Lean
073
Spectral error of an SRTT rangefinder
A randomized trigonometric embedding gives a residual bound with failure probability O(1/k).
Source label: thm:rrf-srttAcceptedRead the mathematical statement & Lean
074
Restricted singular values of Gaussian matrices
Gaussian width controls the distortion of a fixed subset of the unit sphere.
Source label: thm:rsv-gaussAcceptedRead the mathematical statement & Lean
075
Expected error of single-view matrix approximation
Independent Gaussian sketches support a single-view approximation with an expected squared Frobenius-error bound.
Source label: thm:singleviewAcceptedRead the mathematical statement & Lean
076
Exponential bounds for Gaussian trace estimation
Intrinsic dimension controls upper and lower deviations of a Gaussian trace estimator.
Source label: Theorem trace-est-expAcceptedRead the mathematical statement & Lean
077
Maximum principle for a one-dimensional elliptic operator
The sign of the elliptic operator controls the extrema of a function on the interval through its endpoint values.
Theorem 2.1 · printed p. 16AcceptedRead the mathematical statement & Lean
078
Supremum-norm stability in one dimension
An elliptic solution is controlled by its endpoint data and the size of its residual.
Theorem 2.2 · printed p. 17AcceptedRead the mathematical statement & Lean
079
Green-function representation on an interval
Two homogeneous boundary solutions determine a Green kernel for the inhomogeneous Dirichlet problem.
Theorem 2.3 · printed p. 18AcceptedRead the mathematical statement & Lean
080
Existence and stability of a one-dimensional weak solution
The weak Dirichlet problem has a unique solution and an energy bound in terms of the forcing.
Theorem 2.4 · printed p. 22AcceptedRead the mathematical statement & Lean
081
Dirichlet principle on an interval
The weak solution minimizes the quadratic energy, and any other minimizer agrees with it almost everywhere.
Theorem 2.5 · printed p. 22AcceptedRead the mathematical statement & Lean
082
Maximum principles on bounded domains
Elliptic inequalities bound interior extrema by boundary extrema, with a zero truncation when the reaction coefficient is nonnegative.
Theorem 3.1 · printed p. 26AcceptedRead the mathematical statement & Lean
083
Supremum-norm stability on a bounded domain
Boundary values and the elliptic residual bound the supremum norm throughout the domain.
Theorem 3.2 · printed p. 27AcceptedRead the mathematical statement & Lean
084
Poisson integral for a disc
The Poisson-kernel integral represents the harmonic extension of smooth periodic boundary data in the disc setting.
Theorem 3.3 · printed p. 28AcceptedRead the mathematical statement & Lean
085
A fundamental-solution convolution construction
The source formulates a solution construction by convolving a fundamental solution with compactly supported forcing.
Theorem 3.4 · printed p. 30AcceptedRead the mathematical statement & Lean
086
Fundamental solutions of the Laplacian
The logarithmic kernel in two dimensions and inverse-distance kernel in three dimensions are fundamental solutions of the negative Laplacian.
Theorem 3.5 · printed p. 31AcceptedRead the mathematical statement & Lean
087
Weak Dirichlet solvability on a bounded domain
Coercivity gives a unique weak Dirichlet solution with an energy estimate.
Theorem 3.6 · printed p. 33AcceptedRead the mathematical statement & Lean
088
Energy minimization for an elliptic boundary problem
The weak solution minimizes the elliptic energy over the zero-boundary Sobolev space.
Theorem 3.7 · printed p. 34AcceptedRead the mathematical statement & Lean
089
Weak Neumann solvability with positive reaction
The weak Neumann problem has a unique solution in the full first-order Sobolev space.
Theorem 3.8 · printed p. 36AcceptedRead the mathematical statement & Lean
090
A discrete maximum principle on an interval
A sign condition on a finite-difference operator controls grid extrema by endpoint values.
Lemma 4.1 · printed p. 44AcceptedRead the mathematical statement & Lean
091
Second-order error for an elliptic difference scheme
The one-dimensional finite-difference solution approximates a smooth elliptic solution with second-order accuracy in the grid maximum norm.
Theorem 4.1 · printed p. 45AcceptedRead the mathematical statement & Lean
092
Maximum-norm stability of a one-dimensional difference operator
A grid function is bounded by its endpoint values and discrete residual.
Lemma 4.2 · printed p. 45AcceptedRead the mathematical statement & Lean
093
Second-order convergence of the five-point Poisson scheme
The five-point approximation on the unit square has a second-order maximum-norm error bound.
Theorem 4.2 · printed p. 47AcceptedRead the mathematical statement & Lean
094
Boundary attainment for the discrete Poisson maximum principle
For the five-point Laplacian on a square grid, the sign of the discrete Laplacian forces a maximum or minimum to occur on the boundary.
Lemma 4.3 · printed p. 46AcceptedRead the mathematical statement & Lean
095
Boundary-adapted Poisson differences on a curved domain
The boundary-adapted difference scheme retains second-order maximum-norm accuracy on a smooth convex planar domain.
Theorem 4.3 · printed p. 49AcceptedRead the mathematical statement & Lean
096
Maximum-norm stability of the five-point Laplacian
The maximum size of a square-grid function is controlled by its boundary values and discrete Laplacian.
Lemma 4.4 · printed p. 47AcceptedRead the mathematical statement & Lean
097
Stability for a boundary-adapted difference scheme
Boundary data, near-boundary residuals, and interior Laplacian residuals together control a grid function on a convex domain.
Lemma 4.5 · printed p. 48AcceptedRead the mathematical statement & Lean
098
Coercivity and consistency of finite-element quadrature
The two specified quadrature rules preserve coercivity and admit second-order bounds for bilinear-form and load errors.
Lemma 5.1 · printed p. 69AcceptedRead the mathematical statement & Lean
099
Energy approximation by linear elements on an interval
The Galerkin solution is a best approximation in the energy norm and has a first-order derivative error bound.
Theorem 5.1 · printed p. 54AcceptedRead the mathematical statement & Lean
100
Second-order L2 error for interval finite elements
The piecewise-linear Galerkin solution has second-order error in the square-integrable norm.
Theorem 5.2 · printed p. 55AcceptedRead the mathematical statement & Lean
101
Energy error for triangular finite elements
Piecewise-linear Galerkin approximation is optimal in energy and converges at first order in the gradient seminorm.
Theorem 5.3 · printed p. 63AcceptedRead the mathematical statement & Lean
102
Second-order L2 error on convex polygonal domains
Linear finite elements yield a second-order square-integrable error bound for the elliptic problem.
Theorem 5.4 · printed p. 64AcceptedRead the mathematical statement & Lean
103
Ritz-projection approximation in L2 and H1
The Ritz projection has approximation estimates at first- and second-order Sobolev regularity.
Theorem 5.5 · printed p. 65AcceptedRead the mathematical statement & Lean
104
Residual-based a posteriori control of L2 error
Element residuals and jumps in normal flux give an a posteriori bound for the finite-element error.
Theorem 5.6 · printed p. 66AcceptedRead the mathematical statement & Lean
105
Finite-element error with numerical quadrature
The gradient error separates the usual interpolation term from additional quadrature terms.
Theorem 5.7 · printed p. 70AcceptedRead the mathematical statement & Lean
106
Best approximation by a finite orthonormal system
The finite Fourier expansion minimizes the distance to the span of an orthonormal family.
Lemma 6.1 · printed p. 82AcceptedRead the mathematical statement & Lean
107
Positivity and orthogonality of Dirichlet eigenpairs
Dirichlet Laplacian eigenvalues are real and positive, and eigenfunctions for distinct eigenvalues are orthogonal.
Theorem 6.1 · printed p. 79AcceptedRead the mathematical statement & Lean
108
Compactness of the H1 embedding into L2
A bounded set in the first-order Sobolev space is relatively compact in the square-integrable space.
Lemma 6.2 · printed p. 85AcceptedRead the mathematical statement & Lean
109
Attainment of the first Dirichlet Rayleigh quotient
The infimum of the Dirichlet Rayleigh quotient is attained by a normalized first eigenfunction.
Theorem 6.2 · printed p. 79AcceptedRead the mathematical statement & Lean
110
Divergence of the Dirichlet eigenvalue sequence
The ordered Dirichlet eigenvalues tend to infinity.
Theorem 6.3 · printed p. 81AcceptedRead the mathematical statement & Lean
111
Spectral characterization of the zero-boundary Sobolev space
Dirichlet eigenfunctions form a complete orthonormal basis, and their weighted coefficients characterize first-order zero-boundary regularity.
Theorem 6.4 · printed p. 83AcceptedRead the mathematical statement & Lean
112
Min–max characterization of Dirichlet eigenvalues
The nth Dirichlet eigenvalue is characterized by the smallest worst-case Rayleigh quotient over n-dimensional trial spaces.
Theorem 6.5 · printed p. 84AcceptedRead the mathematical statement & Lean
113
Second-order approximation of the first interval eigenvalue
The smallest eigenvalue of the one-dimensional difference operator approximates its continuous counterpart to second order.
Theorem 6.6 · printed p. 89AcceptedRead the mathematical statement & Lean
114
Finite-element eigenvalue bounds
For a fixed eigenvalue index, the conforming finite-element eigenvalue lies above the exact value and converges at second order.
Theorem 6.7 · printed p. 91AcceptedRead the mathematical statement & Lean
115
Approximation of the principal eigenfunction
The principal finite-element eigenfunction converges at second order in L2 and first order in the gradient norm.
Theorem 6.8 · printed p. 92AcceptedRead the mathematical statement & Lean
116
Heat-kernel solution for bounded continuous data
Convolution with the heat kernel solves the heat equation at positive times and approaches the initial value at each point.
Theorem 8.1 · printed p. 110AcceptedRead the mathematical statement & Lean
117
Supremum-norm contraction of the heat flow
Heat evolution does not increase the supremum norm or the distance between two bounded continuous initial conditions.
Theorem 8.2 · printed p. 112AcceptedRead the mathematical statement & Lean
118
Dirichlet heat expansion and smoothing
The Dirichlet eigenfunction series gives a classical heat solution at positive times, approaches L2 initial data, and satisfies smoothing bounds.
Theorem 8.3 · printed p. 117AcceptedRead the mathematical statement & Lean
119
Decay of the Dirichlet heat energy seminorm
Dirichlet heat evolution does not increase the first-order Sobolev seminorm.
Theorem 8.4 · printed p. 117AcceptedRead the mathematical statement & Lean
120
Energy estimates for the forced heat equation
The forced Dirichlet heat equation admits bounds for both solution energy and the time derivative.
Theorem 8.5 · printed p. 120AcceptedRead the mathematical statement & Lean
121
Parabolic maximum principle
A smooth heat subsolution attains its maximum on the initial or lateral boundary of the space–time cylinder.
Theorem 8.6 · printed p. 122AcceptedRead the mathematical statement & Lean
122
Supremum-norm estimate for a forced heat problem
Initial data, boundary data, and forcing control the solution throughout the space–time cylinder.
Theorem 8.7 · printed p. 123AcceptedRead the mathematical statement & Lean
123
Uniqueness of bounded whole-space heat solutions
Two heat solutions with the same initial data agree on a bounded time strip if both are bounded there.
Theorem 8.8 · printed p. 123AcceptedRead the mathematical statement & Lean
124
Maximum-norm error of explicit heat differences
The explicit whole-line heat scheme has second-order spatial accuracy when the time step satisfies the stability restriction.
Theorem 9.1 · printed p. 132AcceptedRead the mathematical statement & Lean
125
A necessary Fourier condition for maximum-norm stability
Maximum-norm stability of a finite-stencil scheme requires its Fourier symbol to have modulus at most one.
Theorem 9.2 · printed p. 132AcceptedRead the mathematical statement & Lean
126
Von Neumann criterion for discrete L2 stability
For a scalar finite-stencil scheme, the Fourier-symbol condition is equivalent to stability in the discrete square-integrable norm.
Theorem 9.3 · printed p. 134AcceptedRead the mathematical statement & Lean
127
Consistency and L2 convergence of heat difference schemes
An L2-stable heat scheme with order-r consistency has an order-r spatial error estimate.
Theorem 9.4 · printed p. 135AcceptedRead the mathematical statement & Lean
128
Explicit Dirichlet heat error on an interval
Forward Euler with centered spatial differences gives a second-order maximum-norm error bound under a CFL condition.
Theorem 9.5 · printed p. 139AcceptedRead the mathematical statement & Lean
129
Implicit Dirichlet heat error on an interval
Backward Euler with centered spatial differences has second-order spatial and first-order temporal error.
Theorem 9.6 · printed p. 141AcceptedRead the mathematical statement & Lean
130
L2 error of semidiscrete heat finite elements
The spatially discrete heat solution has an L2 error controlled by its initial error and a second-order approximation term.
Theorem 10.1 · printed p. 152AcceptedRead the mathematical statement & Lean
131
H1 error of semidiscrete heat finite elements
The gradient error of the semidiscrete heat approximation is first order in the spatial mesh width.
Theorem 10.2 · printed p. 154AcceptedRead the mathematical statement & Lean
132
Heat finite-element error for nonsmooth initial data
Parabolic smoothing yields a second-order spatial error estimate for square-integrable initial data at positive times.
Theorem 10.3 · printed p. 155AcceptedRead the mathematical statement & Lean
133
Higher-order semidiscrete heat approximation
A Ritz-projection approximation property transfers to a higher-order spatial error estimate for the heat equation.
Theorem 10.4 · printed p. 155AcceptedRead the mathematical statement & Lean
134
Backward Euler–Galerkin heat error
Fully discrete heat error separates second-order spatial approximation from first-order time stepping.
Theorem 10.5 · printed p. 156AcceptedRead the mathematical statement & Lean
135
Crank–Nicolson finite-element heat error
Crank–Nicolson with linear finite elements has second-order contributions in both space and time.
Theorem 10.6 · printed p. 159AcceptedRead the mathematical statement & Lean
136
Eigenfunction solution of the Dirichlet wave equation
The wave eigenfunction series converges and solves the Dirichlet initial-boundary problem.
Theorem 11.1 · printed p. 167AcceptedRead the mathematical statement & Lean
137
Energy conservation for the Dirichlet wave equation
The total kinetic and gradient energy of a smooth unforced Dirichlet wave solution is constant.
Theorem 11.2 · printed p. 167AcceptedRead the mathematical statement & Lean
138
Wave energy inside a backward cone
Energy in shrinking spatial balls along a backward characteristic cone cannot exceed its initial value.
Theorem 11.3 · printed p. 167AcceptedRead the mathematical statement & Lean
139
Energy stability for symmetric hyperbolic systems
The L2 norm of a symmetric hyperbolic solution is bounded by the initial data and a time-integrated forcing norm.
Theorem 11.5 · printed p. 178AcceptedRead the mathematical statement & Lean
140
Contractive symbols from positive matrix weights
A finite matrix-valued stencil has a contractive Fourier symbol when its weights are positive semidefinite and sum to the identity.
Lemma 12.1 · printed p. 194AcceptedRead the mathematical statement & Lean
141
First-order error of the upwind transport scheme
The upwind approximation to constant-speed transport has a first-order spatial error bound.
Theorem 12.1 · printed p. 186AcceptedRead the mathematical statement & Lean
142
L2 convergence of stable transport schemes
Order-r consistency and L2 stability imply an order-r error bound for a transport difference scheme.
Theorem 12.2 · printed p. 188AcceptedRead the mathematical statement & Lean
143
Energy conservation for semidiscrete wave finite elements
Spatial Galerkin discretization preserves the unforced wave energy exactly in continuous time.
Lemma 13.1 · printed p. 202AcceptedRead the mathematical statement & Lean
144
Semidiscrete wave error in displacement and velocity
Wave finite-element errors depend on the initial mismatch from Ritz projections and on spatial approximation of the exact solution.
Theorem 13.1 · printed p. 202AcceptedRead the mathematical statement & Lean
145
Discrete wave-energy conservation at half steps
The unforced fully discrete wave scheme preserves a discrete energy built from forward differences and half-step averages.
Lemma 13.2 · printed p. 204AcceptedRead the mathematical statement & Lean
146
Second-order time discretization of the wave equation
The fully discrete wave scheme has second-order midpoint L2 accuracy in displacement and velocity, with first-order spatial gradient accuracy.
Theorem 13.2 · printed p. 205AcceptedRead the mathematical statement & Lean
147
Semidiscrete finite elements for interval transport
A suitable discrete initial value gives a first-order L2 error estimate for the interval transport problem.
Theorem 13.3 · printed p. 206AcceptedRead the mathematical statement & Lean
148
Backward Euler finite elements for interval transport
The fully discrete transport estimate separates first-order spatial and temporal errors.
Theorem 13.4 · printed p. 207AcceptedRead the mathematical statement & Lean
149
Galerkin error for stationary transport with reaction
The Galerkin solution of a stationary transport-reaction problem has a first-order L2 error bound.
Theorem 13.5 · printed p. 209AcceptedRead the mathematical statement & Lean
150
Streamline-diffusion error for stationary transport
Streamline diffusion controls outflow error, bulk error, and the derivative of the error along the flow.
Theorem 13.6 · printed p. 211AcceptedRead the mathematical statement & Lean
151
Pointwise control by the interval H1 norm
The first-order Sobolev norm bounds every point value of a continuously differentiable function on the unit interval.
Lemma A.1 · printed p. 236AcceptedRead the mathematical statement & Lean
152
Riesz representation of bounded linear functionals
Every bounded linear functional on a Hilbert space has a unique representing vector of the same norm.
Theorem A.1 · printed p. 228AcceptedRead the mathematical statement & Lean
153
Equivalence of variational equations and energy minimization
A symmetric positive-definite variational problem is equivalent to minimizing its quadratic energy.
Theorem A.2 · printed p. 229AcceptedRead the mathematical statement & Lean
154
Lax–Milgram existence and energy bound
A bounded coercive bilinear form gives a unique variational solution and a norm bound.
Theorem A.3 · printed p. 230AcceptedRead the mathematical statement & Lean
155
Boundary trace from H1 to L2
Restriction to the boundary extends to a linear trace on the first-order Sobolev space with a norm bound.
Theorem A.4 · printed p. 236AcceptedRead the mathematical statement & Lean
156
Continuous representatives from Sobolev regularity
Sufficient Sobolev regularity supplies a continuous representative on the closed domain with a uniform pointwise bound.
Theorem A.5 · printed p. 237AcceptedRead the mathematical statement & Lean
157
Poincaré inequality for zero-boundary functions
The gradient norm controls the L2 norm of a zero-boundary Sobolev function.
Theorem A.6 · printed p. 238AcceptedRead the mathematical statement & Lean
No matching statements.
Try another term or clear the filters.
Acceptance concerns statement construction and source alignment. Definitions are distinguished from theorem statements; the displayed theorem proofs are omitted (sorry).