Alphabeta Math
DefinitionDefinition: Literature-sourcedProof: Not applicablePipeline-generatedaudited 2026-09-22
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Holomorphic functional calculus

Definition

Assume the Axiom of Choice (The Axiom of Choice). Let A be a unital complex Banach algebra, let aA, and let f be a function holomorphic on an open set UC containing the spectrum σA(a) (Spectrum and resolvent set in a Banach algebra); the spectrum is a nonempty compact subset of the plane (Spectrum is nonempty compact and norm bounded). By Admissible cycle around a compact plane set applied to the compact set σA(a)U there is a finite polygonal complex cycle Γ with trace in UσA(a) such that

n(Γ,z)=1for zσA(a),n(Γ,z)=0for zU;

such a cycle is called admissible for (f,U) (or simply admissible). Define

f(a)  :=  12πiΓf(z)R(z,a)dz    A,

where R(z,a)=(z1a)1 is the resolvent and the integral is that of Banach algebra valued contour integral over the chain Γ (Complex chains, their traces, and cycles). The integrand zf(z)R(z,a) is continuous on the trace of Γ: f is holomorphic on U, and zR(z,a) is norm continuous on the resolvent set Resolvent is Banach-valued holomorphic, which contains Γ. So the integral exists, and f(a)A.

The construction describes the value attached to the germ of f near σA(a): two holomorphic functions f1 on U1 and f2 on U2 with the same germ at σA(a) — that is, agreeing on some neighbourhood of σA(a) — give the same f(a). The value is also independent of which admissible cycle is used; that is Holomorphic functional calculus is contour independent, and until it is proved the notation f(a) refers to the value computed from any one chosen admissible cycle.

Remarks

  • The hypothesis is nonempty and the cycle exists without choice. The spectrum of a is nonempty and compact, so the admissible cycle of Admissible cycle around a compact plane set always exists; the construction inside that lemma uses only finitely many grid cells.

  • Notation for operators. For a nonzero complex Banach space X and TB(X) the definition applies with A=B(X) and gives f(T)=12πiΓf(z)(z1T)1dzB(X), the Dunford integral of the resolvent. The spectrum is taken in B(X) (ex-bounded-operators-form-a-noncommutative-banach-algebra).

  • What is not part of the definition. The definition does not assert that ff(a) is multiplicative, that it preserves polynomials, or that σ(f(a))=f(σ(a)); those properties are proved from this definition in Holomorphic functional calculus homomorphism and Holomorphic spectral mapping and composition. In particular the contour independence of the value is a theorem, and the notation is provisional until then.

  • Wider or smaller domains of holomorphy. Only the germ at σA(a) matters: enlarging U beyond a neighbourhood of the spectrum does not change the value, and shrinking it is allowed as long as it still contains the spectrum and the cycle lies inside it. Both statements follow from Holomorphic functional calculus is contour independent.

  • Reading order. The example items named by ID above are homed on later pages of the plan, so they are named rather than hyperlinked: a body link to later material must be declared as a forward reference, and Step-5b closure removes every such declaration. Rehoming those items to an earlier page (an owner-only reading-order change) would make the citations backward and restore the links.

Depends on

Used by

Dependency tree · two levels

38 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources