Alphabeta MathArticle items · 04 — Complex spectral theorem: a normal endomorphism of a finite-dimensional complex inner product space has an orthonormal eigenbasis, and conversely
Presents 28 items from the article and its immediate prerequisites, covering published library prerequisites.
1 · Prerequisites
- Self-adjoint and normal endomorphisms of a finite-dimensional real or complex inner product space
- In an orthonormal basis, self-adjoint means conjugate-transpose symmetry and normal means commuting with the conjugate transpose
- The complex numbers are algebraically closed
- If the characteristic polynomial of an endomorphism splits, some orthonormal basis makes its matrix upper triangular
- A normal upper-triangular matrix is diagonal
- Riemann's criterion: a bounded f on [a,b] is Darboux integrable if and only if for every real ε > 0 there is a partition P with U(f,P) - L(f,P) < ε
- Heine-Cantor in ℝ: a continuous real function on a compact subset of ℝ is uniformly continuous
- Uniform continuity of f : A → ℝ: one δ serving every pair of points of A
- A subset of ℝ is compact if and only if it is closed and bounded
- Open cover, subcover, compact subset of ℝ (every open cover has a finite subcover), and sequentially compact subset
- Open subset of ℝ (every point has a neighbourhood inside it), closed subset (complement open), and clopen
- Continuity of f : A → ℝ at a point of A and on A: the ε-δ condition, its agreement with lim_x → c f(x) = f(c) at a limit point, and continuity at an isolated point
- A continuous real function on a compact subset of ℝ is bounded
- Partition of [a,b] as a finite strictly increasing list a = t₀ < t₁ < … < tₙ = b, its subintervals and their lengths, its mesh, refinement, and the common refinement of two partitions
- For bounded f on [a,b] and a partition P: the infimum mᵢ and supremum Mᵢ of f on the i-th subinterval, and the lower and upper Darboux sums L(f,P) = ∑ᵢ mᵢ Δᵢ and U(f,P) = ∑ᵢ Mᵢ Δᵢ
- The lower and upper Darboux integrals of a bounded f on [a,b] as sup_P L(f,P) and inf_P U(f,P), Darboux integrability as their equality, and the notation ∫ₐᵇ f
- Laws of finite sums and finite products
- Finite sums and finite products, by recursion
- For every ε > 0 in a complete ordered field there is a natural n ≥ 1 with 1/n < ε
- Every complete ordered field is Archimedean
- The canonical natural ι(n) = n · 1_F of a field
- Canonical naturals are positive and strictly increasing
- Intervals of ℝ: the nine order-convex forms, nondegeneracy, and length
- Lower bound, bounded below, bounded set
- Basic properties of the absolute value
- Complete ordered field (least-upper-bound property)
- Ordered field
- Order is preserved by adding a constant and by adding inequalities
- Sign rules for products and monotonicity of multiplication
- Reverse Fatou's lemma under an integrable majorant
- Integrable real and complex functions, and their integrals
- The Lebesgue integral is linear on L¹(μ)
- The modulus of an integral is bounded by the integral of the modulus
- Additivity of the nonnegative Lebesgue integral
- A nonnegative integral over a null set vanishes
- A nonnegative measurable function with finite integral is finite almost everywhere
- Monotonicity and nonnegative homogeneity of the nonnegative integral
- The exponential series converges absolutely for every real argument
- The exponential function is smooth and (exp)'=exp
- The exponential is positive and satisfies exp(-x)=1/exp(x)
- The mean value theorem, as the case g(x) = x of Cauchy's: for f continuous on [a,b] with a < b and differentiable on (a,b) there is c ∈ (a,b) with f(b) - f(a) = f'(c)(b-a)
- The sum of a real power series is continuous at every point strictly inside its interval of convergence
- The real exponential function and the number e by a power series
- A series of nonnegative terms converges iff its partial sums are bounded, and then the sum is their supremum
- Limits at +∞ and -∞, and infinite limits at a point
- Fourier transform acts continuously on Schwartz space
- Schwartz derivatives are integrable
- L1 Fourier inversion with an integrable transform
- The Axiom of Countable Choice (AC_ω)
- The derivative f'(c) = lim_x → c f(x) - f(c)/x - c of f : A → ℝ at a point c ∈ A that is a limit point of A, and differentiability on a set
- A function differentiable at c is continuous at c
- Tonelli's theorem for nonnegative measurable functions on a sigma-finite product
- The class L¹(μ) of integrable functions
- Integral over a measurable subset
- The indefinite integral of a nonnegative simple function is a measure
- Monotone convergence for the integral
- Measures on sigma-algebras
- Reflection through zero exchanges upper and lower bounds
- Greatest lower bound (infimum)
- Suprema and infima are unique
- Identities and inverses in a field are unique
- Field
- Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function
- f is continuous at c ∈ A if and only if f(xₖ) → f(c) for every sequence in A converging to c, the converse direction costing countable choice
- A nested sequence of nonempty closed bounded intervals has nonempty intersection, and the intersection is a single point exactly when the lengths tend to 0
- The recursion theorem
- For |r| < 1 the sequence rᵏ is null, and for |r| > 1 the sequence |r|ᵏ diverges to +∞
- Algebra of limits: sums, scalar multiples, products and quotients
- Limits preserve non-strict inequalities
- Limits and Cauchy sequences of reals
- Sequences of reals: bounded, eventually, frequently, tails, subsequences
- Integer powers aᵐ
- Laws of integer exponents
- Lebesgue measurable sets, the family L(ℝⁿ), and the restricted set function λₙ
- Assuming countable choice, Lebesgue outer measure is an outer measure that restricts to elementary volume
- Carathéodory's theorem: measurable sets form a sigma-algebra carrying a complete measure
- Assuming countable choice, every source-algebra set is measurable for the induced outer measure
- Assuming countable choice, a premeasure extends through its induced outer measure
- Every outer-null set is Carathéodory measurable
- Complete measure spaces
- Elementary sets: the finite unions of half-open boxes in ℝⁿ
- Lebesgue outer measure on ℝⁿ
- Elementary volume is a sigma-finite premeasure on the algebra of elementary sets
- The sum of the volumes of a disjoint box decomposition of an elementary set does not depend on the decomposition
- Half-open boxes in ℝⁿ and their volume
- The natural logarithm as the inverse of the exponential function
- Derivative of an inverse: if f is continuous and injective on a nondegenerate interval I and differentiable at c ∈ I with f'(c) ≠ 0, then the inverse g is differentiable at f(c) with g'(f(c)) = 1/f'(c); and if f'(c) = 0 then g is not differentiable at f(c)
- The first fundamental theorem: if f is integrable on [a,b] and continuous at c, then F'(c) = f(c); in particular a continuous f has F as a primitive
- The integral with oriented limits: ∫ₐᵃ f := 0 and ∫_bᵃ f := -∫ₐᵇ f
- A function continuous on an interval I whose derivative vanishes at every interior point of I is constant on I; consequently two such functions with the same derivative differ by a constant
- Nondecreasing, increasing (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of ℝ, with the dictionary to monotone sequences
- If f ≤ g on a punctured neighbourhood of c then lim f ≤ lim g, non-strictly
- The ε-δ limit lim_x → c f(x) = L of f : A → ℝ at a limit point c of A
- Interior, closure, boundary and exterior of a subset of ℝ
- Inverses of positives are positive, and reciprocation reverses order
- The ε-neighbourhood and the punctured ε-neighbourhood of a point of ℝ
- Limit point, isolated point, adherent point, derived set, and dense subset of ℝ
- For a<c<b: f is integrable on [a,b] if and only if it is integrable on [a,c] and on [c,b], and then ∫ₐᵇ f = ∫ₐᶜ f + ∫_cᵇ f; with the oriented form for arbitrary a,b,c
- If f ≤ g on [a,b] and both are integrable then ∫ₐᵇ f ≤ ∫ₐᵇ g; and m(b-a) ≤ ∫ₐᵇ f ≤ M(b-a)
- If m ≤ f ≤ M on [a,b] then m(b-a) ≤ L(f,P) ≤ ∫ₐᵇ f ≤ ∫ₐᵇ f ≤ U(f,P) ≤ M(b-a) for every partition P; in particular every constant function is integrable, with ∫ₐᵇ c = c(b-a)
- A function integrable on [a,b] is integrable on every closed subinterval
- Maximum and minimum of a set
- The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral
- Vector-valued functions f : A → ℝᵐ, their limits and continuity, with the dictionary to the metric notions
- The Euclidean inner product ⟨ x,y⟩ = ∑_k<n xₖ yₖ on ℝⁿ
- Cauchy-Schwarz |⟨ x,y⟩| ≤ ‖ x‖₂‖ y‖₂ with its equality case, the triangle inequality for ‖·‖₂, the parallelogram law and polarisation
- The p-norms ‖ x‖ₚ for rational p ≥ 1, and ‖ x‖_∞
- A norm on a real vector space, the induced metric, and the dictionary with the metric axioms
- Integrable functions on [a,b] form a set closed under sums and scalar multiples, and ∫ₐᵇ(λ f+μ g) = λ∫ₐᵇ f + μ∫ₐᵇ g
- If f,g are integrable on [a,b] then so are | f|, f², fg, max(f,g) and min(f,g), and |∫ₐᵇ f| ≤ ∫ₐᵇ| f|
- If f is integrable on [a,b] with values in [m,M] and φ is continuous on [m,M], then φ ∘ f is integrable
- Square roots exist: a unique √a ≥ 0 with (√a)² = a; the positives are {x² : x ≠ 0}
- Continuous inverse theorem: a continuous injective f on an interval I is a bijection onto the order-convex set f[I], and the inverse g : f[I] → I is continuous and strictly monotone in the same sense as f
- The principle of mathematical induction
- Squaring is monotone on the nonnegatives
- The principal inverse tangent arctan:ℝ→(-π/2,π/2)
- Tangent, cotangent, secant, and cosecant on their exact natural domains
- The derivatives of sine and cosine are cosine and minus sine
- Derivatives and fundamental periods of tangent, cotangent, secant, and cosecant
- Pythagorean and parity identities for all six trigonometric functions on their natural domains
- For |r| < 1, ∑_k ≥ 0 rᵏ = 1/(1-r), and for |r| ≥ 1 the series diverges
- Inside its radius a real power series may be integrated term by term on every closed subinterval
- The alternating series test: if (bₖ) is nonincreasing with bₖ → 0 then ∑ₖ (-1)ᵏ bₖ converges, the sum lies between any two consecutive partial sums, and the error after n terms is at most bₙ
- Abel's limit theorem: if a real series converges to s, then its power series tends to s as x↑1
- Cofunction, supplementary, quarter-turn, and reflection identities for the six trigonometric functions
- Density operator
- A non-negative operator is equivalently self-adjoint with nonnegative eigenvalues, a positive semidefinite matrix in an orthonormal basis, or an operator of the form S^*S
- The basis-independent trace of an endomorphism of a finite-dimensional vector space
- Ray-to-projector is well-defined and bijective
- Rank and nullity of a linear map with finite-dimensional domain
- Real and complex inner-product spaces and their induced length
- Finite-dimensional quantum channel
- Choi matrix with input factor first
- Finite Kraus representation
- Isometric Stinespring representation
- Partial trace over a finite tensor factor
- Trace preservation is Kraus normalization
- The Choi partial trace characterizes trace preservation
- Every finite-dimensional channel has a finite isometric dilation
- An isometry followed by partial trace is a channel
- Finite instruments and conditional states
- Trace is a linear functional on Mₙ(F)
- Completely positive maps
- Non-negative and positive operators
- Every finite-dimensional real or complex inner product space has an orthonormal basis
- The adjoint T^*:W→ V is characterised by ⟨ Tv,w⟩_W=⟨ v,T^*w⟩_V
- Real and complex inner product spaces, with the inner product linear in the first argument
- Quantum code as an isometric encoding and its code projector
- A unitary error-basis change gives orthogonal error ranges
- Agreement on pure states implies complete agreement
- Orthogonal error restrictions determine syndrome projections
- Adjoints satisfy (S+T)^*=S^*+T^*, (λ T)^*=λ̄ T^*, (ST)^*=T^*S^*, and T^**=T
- Every linear map between finite-dimensional inner product spaces has a unique adjoint
- An isometric quantum encoding gives an orthogonal code projector
- Exact recovery of an encoded quantum code
- Kraus operators in an identity-channel representation are scalar
- Complete positivity implies Choi positivity
- A positive Choi matrix yields finite Kraus operators
- Coordinate columns [v]_B and matrices [T]_B^C of linear maps relative to ordered bases
- Rectangular matrix multiplication and the identity matrix Iₙ, including zero-sized shapes
- The standard formulas ⟨ x,y⟩=∑_k<nxₖ yₖ on ℝⁿ and ∑_k<nxₖyₖ on ℂⁿ are inner products
- Ordered tensor registers, their inner product, and wire permutations
- Tensor products of finitely many linear maps
- The product basis is orthonormal and tensor dimensions multiply
- Tensor maps preserve composition, identities, and adjoints
- Finite POVMs and their outcome law
- A non-negative operator has a unique non-negative square root
- For A∈ M_m× n(F) and B∈ M_n× m(F), tr(AB)=tr(BA)
- Trace Distance
- Measurement Variation At Most Trace Distance
- Helstrom Binary Discrimination
- Linear map between vector spaces over the same field
- Trace Norm
- The singular values of a linear map as the eigenvalues of the positive square root of T^*T
- Every linear map between finite-dimensional real or complex inner product spaces admits a singular value decomposition
- The operator norm is zero on the zero domain and otherwise is max_‖ v‖=1‖ Tv‖
- Cauchy–Schwarz: |⟨ x,y⟩|≤‖x‖ ‖y‖, with equality exactly for dependent pairs
- Singular values are well defined because the positive square root of T^*T is unique
- Bessel's inequality for a finite orthonormal list and Parseval's identity for an orthonormal basis
- Conjugation is an involutive real-field automorphism, zz̄=|z|², and modulus is definite, multiplicative, and subadditive
2 · Logical flowchart
Arrows show item dependencies. A grouped prerequisite node points to items that use one or more of its members; their exact links are listed above.
3 · Items
TheoremLibrary prerequisite
Complex spectral theorem: a normal endomorphism of a finite-dimensional complex inner product space has an orthonormal eigenbasis, and conversely
TheoremLibrary prerequisite
A continuous function on [a,b] is Riemann integrable, by Heine-Cantor and Riemann's criterion
TheoremLibrary prerequisite
Dominated convergence
TheoremLibrary prerequisite
The exponential function is strictly increasing
TheoremLibrary prerequisite
The exponential tends to +∞ at +∞ and to 0 at -∞
TheoremLibrary prerequisite
Fourier inversion on Schwartz space
TheoremLibrary prerequisite
The second fundamental theorem: if G is differentiable on [a,b] with G' = f and f is integrable, then ∫ₐᵇ f = G(b)-G(a)
TheoremLibrary prerequisite
Fubini's theorem for L¹ functions on a sigma-finite product
TheoremLibrary prerequisite
The indefinite integral of a nonnegative measurable function is a measure
TheoremLibrary prerequisite
Every nonempty set bounded below has an infimum
TheoremLibrary prerequisite
Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on [a,b] takes every value between f(a) and f(b)
TheoremLibrary prerequisite
Assuming countable choice, L(ℝⁿ) is a sigma-algebra containing every elementary set and λₙ is a complete measure extending elementary volume
TheoremLibrary prerequisite
The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t
TheoremLibrary prerequisite
On an interval I, for f continuous on I and differentiable at every interior point: f' ≥ 0 throughout gives f nondecreasing, f' > 0 gives f increasing, f' ≤ 0 and f' < 0 give the two decreasing forms; conversely a nondecreasing f has f' ≥ 0 and a nonincreasing f has f' ≤ 0 wherever it is differentiable, and no strict converse is claimed
TheoremLibrary prerequisite
A continuous f ≥ 0 on [a,b] with ∫ₐᵇ f = 0 is identically 0
TheoremLibrary prerequisite
For a ≤ b and f : [a,b] → ℝᵐ integrable when a<b, ‖∫ₐᵇ f‖₂ ≤ ∫ₐᵇ ‖ f‖₂; for a<b, ‖ f‖₂ is integrable
TheoremLibrary prerequisite
Principal arctangent: derivative, integral, power series, and the Gregory–Leibniz series
TheoremLibrary prerequisite
Density operators have an orthogonal spectral ensemble
TheoremLibrary prerequisite
Finite channel, Kraus, Choi, and Stinespring equivalence
TheoremLibrary prerequisite
Positive-probability instrument branches are density operators
TheoremLibrary prerequisite
Instrument outcome weights normalize
TheoremLibrary prerequisite
An explicit syndrome recovery corrects a Knill–Laflamme error family
TheoremLibrary prerequisite
Exact recovery implies the Knill–Laflamme condition
TheoremLibrary prerequisite
Kraus and Choi characterizations of complete positivity
TheoremLibrary prerequisite
A finite Kraus sum is completely positive
TheoremLibrary prerequisite
POVM outcome weights are probabilities
TheoremLibrary prerequisite
Trace Distance Channel Contractivity
TheoremLibrary prerequisite