Operator theory
The Lean Pool projects whose card's first MSC2020 code is in class 47, Operator theory: 7 articles, one per card.
TheoremContinuity and zero-class properties of abstract linear control systems#
Proves that every abstract linear control system with bounded L-infinity inputs between real or complex Banach spaces is zero-class, and hence has continuous input-response trajectories. No integral representation or reflexivity assumption is required. Includes finite-p continuity, a finite-p system with constant response norm, and a scalar zero-class system without integral representation or Orlicz-heart admissibility. Reusable infrastructure includes Phillips' lemma, strongly continuous semigroup bounds, half-line Lp concatenation and shifts, invariant Hahn-Banach extensions, and periodic invariant means.
Quoted from the card LeanPool/projects/abstract-linear-control.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 6 main results, each with its informal statement quoted from the card. The scan finds 6 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
AbstractLinearControl.ALCS.zero_class(theorem; a main declaration), declared in LeanPool/AbstractLinearControl/ZeroClass.lean, line 682: “For every abstract linear control system with L-infinity inputs between real or complex Banach spaces, the norms of its input-response operators tend to zero as time tends to zero from the right.” Its source, as the card gives it: “Theorem 1.5 of version 2, completed in Lean on 2026-10-03.”AbstractLinearControl.ALCS.continuousOn_Phi(theorem), declared in LeanPool/AbstractLinearControl/ContinuityLinfty.lean, line 65: “For every bounded input of such a system, its input-response trajectory is continuous on the nonnegative half-line.” Its source, as the card gives it: “Corollary 1.6.”AbstractLinearControl.ALCS.continuousOn_Phi_of_ne_top(theorem), declared in LeanPool/AbstractLinearControl/ContinuityFiniteP.lean, line 131: “For every abstract linear control system with finite exponent p at least one and complete state space, each Lp input has a continuous input-response trajectory on the nonnegative half-line.” Its source, as the card gives it: “Proposition 1.3.”AbstractLinearControl.exists_system_norm_Phi_eq_one(theorem), declared in LeanPool/AbstractLinearControl/Examples/FinitePNotZeroClass.lean, line 489: “For every finite exponent p at least one, there exist real Banach input and state spaces and an abstract linear control system whose input-response operator has norm one at every positive time.” Its source, as the card gives it: “Proposition 3.1.”AbstractLinearControl.ExoticMean.Counterexample.no_representation(theorem), declared in LeanPool/AbstractLinearControl/Examples/NoRepresentation.lean, line 496: “There exists a scalar abstract linear control system with identity semigroup and response norm equal to time, which has no integral representation and is not admissible for any of the formalized Young-function Orlicz hearts.” Its source, as the card gives it: “Proposition 3.3; formal Young functions include the paper's class.”AbstractLinearControl.Phillips.full(theorem), declared in LeanPool/AbstractLinearControl/Background/Phillips.lean, line 665: “For a pointwise null sequence of bounded linear functionals on real or complex bounded sequences, each sequence of atomic coefficients is absolutely summable, its sum of norms tends to zero, and its diagonal coefficient tends to zero.” Its source, as the card gives it: “Lemma 2.2.”
Project
- Authors: Frédéric Marbach, GPT-6 Pro, Claude Opus 5.5.
- Source: Continuity of solutions to abstract linear control systems, paper.
- Project repository: frederic-marbach/alcs, at commit bda56576.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 47D06, 93C25, 46E30.
- In Lean Pool: LeanPool/AbstractLinearControl, from the card LeanPool/projects/abstract-linear-control.yaml.
Sources
TheoremDavis–Kahan rotation of eigenvectors#
Formalizes the sin-Theta, tan-Theta, sin-two-Theta, and tan-two-Theta theorem families from Section 2 of Davis and Kahan (1970), for real or complex separable Hilbert spaces, including common-domain unbounded operators and symmetric-norm estimates. The tan-Theta endpoint requires Rayleigh–Ritz trial data with residual orthogonal to the trial subspace.
Quoted from the card LeanPool/projects/aiq-davis-kahan-1970-rotation-eigenvectgors-perturbation-formalization.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 5 main results, each with its informal statement quoted from the card. The scan finds 5 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
RotationOfEigenvectors.sinTheta_mem_and_bound(theorem; a main declaration), declared in LeanPool/DavisKahan/Solution.lean, line 383: “With finite symmetric residual norm, a spectral gap gives sine-angle ideal membership and controls its symmetric norm by the corresponding residual norm.”RotationOfEigenvectors.tanTheta(theorem), declared in LeanPool/DavisKahan/Solution.lean, line 416: “For Rayleigh–Ritz trial data with residual orthogonal to the trial subspace, a positive directed spectral gap between the trial compression and the unwanted reducing block gives the symmetric-norm tangent-angle residual estimate and tangent pole exclusion, assuming the residual has finite symmetric norm.”RotationOfEigenvectors.sinTwoTheta_directed_mem_and_bound(theorem), declared in LeanPool/DavisKahan/Solution.lean, line 461: “Under the printed oriented gap and common-domain self-adjointness hypotheses, finite symmetric residual norm gives directed sine-double-angle ideal membership, and twice the residual norm bounds the gap times its norm.”RotationOfEigenvectors.sinTwoTheta_ambient_mem_and_bound(theorem), declared in LeanPool/DavisKahan/Solution.lean, line 536: “Finite symmetric perturbation norm gives ambient sine-double-angle ideal membership and the whole-space gap bound under the theorem's reducing and perturbed-gap hypotheses.”RotationOfEigenvectors.tanTwoTheta(theorem), declared in LeanPool/DavisKahan/Solution.lean, line 603: “The residual tangent-double-angle estimate holds with the theorem’s source-facing block hypotheses.”
Project
- Authors: Jon Crall, Edward Wang.
- Project repository: aiq-kitware/aiq-davis-kahan-1970-rotation-eigenvectgors-perturbation-formalization, at commit 38e37da6.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 47A55, 47A15, 15A42.
- In Lean Pool: LeanPool/DavisKahan, from the card LeanPool/projects/aiq-davis-kahan-1970-rotation-eigenvectgors-perturbation-formalization.yaml.
Sources
Theoremlean-spectral-theory#
The spectral theorem for possibly unbounded self-adjoint operators on complex Hilbert spaces, formalized through the Cayley transform and real projection-valued measures. The selected spectral theorem constructs a PVM whose scalar measures give the exact finite-second-moment domain and first-moment quadratic form, with measurable-set uniqueness, and is proved equivalent to equality with the unbounded coordinate spectral integral. The selected Stone theorem proves both that strongly continuous one-parameter unitary groups have self-adjoint generators and that every self-adjoint operator generates such a group.
Quoted from the card LeanPool/projects/lean-spectral-theory.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 2 main results, each with its informal statement quoted from the card. The scan finds 2 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
PalomarSpectralStone.spectral_theorem_intrinsic(theorem; a main declaration), declared in LeanPool/SpectralTheory/SpectralStoneSolution.lean, line 85: “Every self-adjoint partial linear operator on a complex Hilbert space has a real projection-valued measure representing its domain and scalar moments, unique on Borel sets.”PalomarSpectralStone.stone_theorem_intrinsic(theorem), declared in LeanPool/SpectralTheory/SpectralStoneSolution.lean, line 137: “Every strongly continuous one-parameter unitary group has a self-adjoint generator, and every self-adjoint operator generates such a group.”
Project
- Authors: Ezzeri Esa.
- Project repository: savarin/lean-spectral-theory, at commit d19e279f.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 47A10, 47B15.
- In Lean Pool: LeanPool/SpectralTheory, from the card LeanPool/projects/lean-spectral-theory.yaml.
Sources
TheoremNemytskii operators on Lebesgue spaces#
Develops superposition operators induced by Caratheodory functions: measurability, Lp-to-Lq growth bounds and sequential continuity, Lipschitz estimates, monotonicity and coercivity, and Frechet remainder estimates. For Lebesgue measure on the real line and finite-dimensional real fibers, characterizes when every Lp input has an Lq output by the standard integrable-envelope growth condition, for 1 <= p,q < infinity. First-order remainder estimates on arbitrary measure spaces assume a Caratheodory derivative with the stated Holder-compatible growth. The integral-functional result bounds the integrated remainder and proves integrability of the linearized integrand; it does not assert integrability of the original integrand without its separate growth hypotheses. Caratheodory here requires strongly measurable sections and almost-everywhere continuity in the fiber variable.
Quoted from the card LeanPool/projects/nemytskii-lebesgue.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 4 main results, each with its informal statement quoted from the card. The scan finds 4 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
NemytskiiLebesgue.IsCaratheodory.memLp_nemytskii_volume_iff_growth(theorem; a main declaration), declared in LeanPool/NemytskiiLebesgue/ConverseImplication.lean, line 1052: “For f from R times R^m to R^k with strongly measurable sections and almost-everywhere continuous fibers, and 1 <= p,q < infinity, every Lp input gives an Lq output if and only if there exist an Lq real envelope a and a nonnegative constant C such that almost everywhere, simultaneously for every fiber vector xi, norm(f(x,xi)) <= abs(a(x)) + C * norm(xi)^(p/q).” Its source, as the card gives it: “Upstream NemytskiiLebesgue/ConverseImplication.lean.”NemytskiiLebesgue.IsCaratheodory.nemytskii_seqContinuous_of_memLp_of_growth_real(theorem), declared in LeanPool/NemytskiiLebesgue/Continuity.lean, line 433: “On any measure space, the same Caratheodory and growth assumptions imply that a sequence of Lp functions converging in Lp to an Lp function has superposition images converging in Lq, for finite exponents p,q at least one and finite-dimensional real fibers.” Its source, as the card gives it: “Upstream NemytskiiLebesgue/Continuity.lean.”NemytskiiLebesgue.IsCaratheodory.eLpNorm_frechet_remainder_le_ofReal_mul_eLpNorm(theorem), declared in LeanPool/NemytskiiLebesgue/Frechet.lean, line 430: “On a measure space, suppose f and its fiber derivative f' are Caratheodory, f' is the Frechet derivative at every fiber point almost everywhere, p,r >= 1 satisfy 1/q = 1/r + 1/p, and f' is bounded by b + C * norm(xi)^(p/r) with nonnegative b in Lr and C > 0. At each Lp function u, the Lq integral quantity (a quasi-norm when q < 1) of the first-order remainder is at most epsilon times the Lp norm of l whenever l is in Lp and its Lp norm is sufficiently small.” Its source, as the card gives it: “Upstream NemytskiiLebesgue/Frechet.lean; generalized in this port by removing an unused finite-measure assumption.”NemytskiiLebesgue.IsCaratheodory.integralFunctional_frechet_deriv(theorem), declared in LeanPool/NemytskiiLebesgue/IntegralFunctional.lean, line 193: “On a measure space with finite-dimensional real inputs, under Caratheodory assumptions on f and its fiber derivative f', conjugate exponents p,q, and derivative growth b + C*norm(xi)^(p-1) with nonnegative b in Lq and C > 0, the linearized integrand is integrable for every Lp perturbation. The norm of the integral of the first-order remainder is at most epsilon times the Lp norm of the perturbation when that norm is sufficiently small.” Its source, as the card gives it: “Upstream NemytskiiLebesgue/IntegralFunctional.lean; generalized in this port by removing an unused finite-measure assumption.”
Project
- Authors: Petr Girg, Petr Nečesal, Martin Dvořák, Jakub Psutka.
- Source: Nemytskii operators on Lebesgue spaces.
- Project repository: madvorak/nemytskii-lebesgue, at commit d276c27a.
- Provenance: mix, which in Lean Pool's terms means people and AI “both contributed substantially” to its Lean proofs. The card's note: “Upstream credits the four listed authors. Its README and available commit history contain no AI disclosure; this is evidence under the repository's human-provenance rubric, not proof of tool non-use. The imported version includes substantial AI-assisted Mathlib porting and proof refactoring by OpenAI Codex, so it is recorded as mixed.”
- License: Apache-2.0.
- MSC2020: 47H30, 46E30, 47J05.
- In Lean Pool: LeanPool/NemytskiiLebesgue, from the card LeanPool/projects/nemytskii-lebesgue.yaml.
Sources
TheoremPietsch s-numbers and the maximal difference theorem#
Formalizes the five classical s-number sequences, their comparison inequalities, the maximal difference theorem, compact-operator singular value decomposition, John ellipsoids, entropy numbers, and compactness characterizations.
Quoted from the card LeanPool/projects/lean-snumbers.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 3 main results, each with its informal statement quoted from the card. The scan finds 3 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
SNumbers.approximationNumber_le_e_mul_hilbertNumber(theorem; a main declaration), declared in LeanPool/SNumbers/SNumbers/MaxDifference.lean, line 900: “For a bounded operator, its nth approximation number is at most e times (n+1) times its nth Hilbert number.”SNumbers.allSNumbers_eq_on_HilbertSpace(theorem), declared in LeanPool/SNumbers/SNumbers/Uniqueness.lean, line 132: “Every s-number sequence agrees with the approximation numbers on operators between Hilbert spaces.”John.john_decomposition(theorem), declared in LeanPool/SNumbers/BasicResults/John.lean, line 852: “In John position, the identity decomposes into a positive weighted sum of rank-one operators from contact points.”
Project
- Authors: Mario Ullrich.
- Project repository: mario-ullrich/lean-snumbers, at commit d984f39b.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 47B06, 46B20.
- In Lean Pool: LeanPool/SNumbers, from the card LeanPool/projects/lean-snumbers.yaml.
Sources
TheoremSpectral theorem for compact self-adjoint operators#
Formalizes the spectral theorem for compact self-adjoint operators on a Hilbert space: such an operator admits a Hilbert basis of eigenvectors. The development passes from weak compactness of Hilbert closed balls and Rayleigh-quotient extrema to an eigenvector at the operator norm, finiteness of the point spectrum outside any neighbourhood of zero, finite-rank cutoff approximation, and finally the orthogonal decomposition into eigenspaces.
Quoted from the card LeanPool/projects/compact-spectral.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 5 main results, each with its informal statement quoted from the card. The scan finds 5 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
CompactSelfAdjoint.exists_hilbertBasis_hasEigenvector_of_isCompactOperator_of_isSelfAdjoint(theorem), declared in LeanPool/CompactSpectral/Analysis/InnerProductSpace/CompactSelfAdjoint/SpectralTheorem.lean, line 139: “A compact self-adjoint operator on a Hilbert space admits a Hilbert basis of eigenvectors.” Its source, as the card gives it: “A. W. Knapp, Advanced Real Analysis, Chapter II, Section 2, Theorem 2.3, doi:10.3792/euclid/9781429799911-2.”CompactSelfAdjoint.iSup_eigenspace_orthogonal_eq_bot_of_isCompactOperator_of_isSelfAdjoint(theorem), declared in LeanPool/CompactSpectral/Analysis/InnerProductSpace/CompactSelfAdjoint/SpectralTheorem.lean, line 45: “The eigenspaces of a compact self-adjoint operator span a dense subspace: the orthogonal complement of the supremum of all eigenspaces is trivial.” Its source, as the card gives it: “A. W. Knapp, Advanced Real Analysis, Chapter II, Section 2, Theorem 2.3, doi:10.3792/euclid/9781429799911-2.”CompactSelfAdjoint.exists_hasEigenvector_iSup_or_iInf_of_isCompactOperator(theorem; a main declaration), declared in LeanPool/CompactSpectral/Analysis/InnerProductSpace/RayleighCompact.lean, line 335: “A compact self-adjoint operator has an eigenvector whose eigenvalue realizes either the supremum or the infimum of its Rayleigh quotient.” Its source, as the card gives it: “A. W. Knapp, Advanced Real Analysis, Chapter II, Section 2, Theorem 2.2, doi:10.3792/euclid/9781429799911-2.”CompactSelfAdjoint.exists_unit_norm_eq_opNorm_of_isCompactOperator(theorem), declared in LeanPool/CompactSpectral/Analysis/InnerProductSpace/CompactSelfAdjoint/OpNormEigenvalue.lean, line 63: “A compact operator attains its operator norm on the unit sphere of the Hilbert space.” Its source, as the card gives it: “A. W. Knapp, Advanced Real Analysis, Chapter II, Section 1, compactness preliminaries for compact operators, doi:10.3792/euclid/9781429799911-2.”CompactSelfAdjoint.countable_set_hasEigenvalue_ne_zero_of_isCompactOperator_of_isSelfAdjoint(theorem), declared in LeanPool/CompactSpectral/Analysis/InnerProductSpace/CompactSelfAdjoint/SpectralFiniteness.lean, line 212: “The set of nonzero eigenvalues of a compact self-adjoint operator is countable.” Its source, as the card gives it: “A. W. Knapp, Advanced Real Analysis, Chapter II, Section 2, spectral theorem consequences, doi:10.3792/euclid/9781429799911-2.”
Project
- Authors: Adam Benenson.
- Source: Advanced Real Analysis by Anthony W. Knapp, doi:10.3792/euclid/9781429799911-2.
- Project repository: abenenson/compact-spectral.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 47A75, 47B07.
- In Lean Pool: LeanPool/CompactSpectral, from the card LeanPool/projects/compact-spectral.yaml.
Sources
TheoremUnitary dilation and the Crouzeix–Palencia bound#
Proves unitary power dilation for Hilbert-space contractions, von Neumann’s polynomial inequality, and the Crouzeix–Palencia polynomial spectral-set estimate for the closed numerical range.
Quoted from the card LeanPool/projects/lean-operator-theory.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 3 main results, each with its informal statement quoted from the card. The scan finds 3 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
PalomarCrouzeixPalencia.exists_unitary_power_dilation(theorem), declared in LeanPool/OperatorTheory/CrouzeixPalenciaSolution.lean, line 49: “Every contraction on a complex Hilbert space admits a unitary power dilation.”PalomarCrouzeixPalencia.vonNeumann_inequality(theorem), declared in LeanPool/OperatorTheory/CrouzeixPalenciaSolution.lean, line 58: “Polynomial evaluation on a contraction is bounded by the polynomial supremum on the closed unit disk.”PalomarCrouzeixPalencia.crouzeix_palencia(theorem; a main declaration), declared in LeanPool/OperatorTheory/CrouzeixPalenciaSolution.lean, line 64: “The closure of the numerical range is a polynomial spectral set with constant 1 + √2.”
Project
- Authors: Ezzeri Esa.
- Project repository: savarin/lean-operator-theory, at commit 6f90bb7e.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 47A12, 47A20, 47A25.
- In Lean Pool: LeanPool/OperatorTheory, from the card LeanPool/projects/lean-operator-theory.yaml.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.