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 is contour independent
Statement
Assume the Axiom of Choice (The Axiom of Choice). Let be a unital complex Banach algebra, , and let be holomorphic on an open set containing . Then the value of Holomorphic functional calculus is independent of the admissible cycle used to compute it. Moreover, if is another open set containing and is holomorphic on with on a neighbourhood of , then with computed from .
Facts & Assumptions
Given: An assumed Axiom of Choice, a unital complex Banach algebra , an element with nonempty compact spectrum , an open , a holomorphic , and two admissible cycles in .
The definition chooses an admissible cycle and sets ; for every admissible cycle the displayed integral is defined because the integrand is continuous on its trace (Holomorphic functional calculus).
A cycle is null-homologous in an open set exactly when for every ; equivalently vanishes at every point outside (Null-homologous cycles and homologous cycles in an open set).
If is continuous and weakly holomorphic on an open and is a cycle with trace in that is null-homologous in , then (Banach-valued Cauchy integral vanishes).
For fixed the map is holomorphic on and the product of a scalar holomorphic function with it is weakly holomorphic: for every bounded linear functional on the map is holomorphic on (Resolvent is Banach-valued holomorphic, Spectrum and resolvent set in a Banach algebra).
For every compact contained in an open set there is a finite polygonal cycle with index on and index outside (Admissible cycle around a compact plane set).
Proof
Put , an open set containing both traces ; the difference is a cycle with trace in whose index at is .
The map is continuous on and weakly holomorphic there: for a bounded linear functional the composition is a product of the holomorphic scalar function and the holomorphic scalar function , hence holomorphic on the open subset of .
Germ independence: let be open and let be holomorphic on with on a neighbourhood of . Apply [L6] to the compact set and the open set : this gives an admissible cycle for both and with trace in , hence lying in , where .
For both indices equal , and for both equal , by admissibility; hence for every , that is, is null-homologous in .
By [L3] applied to and the cycle , null-homologous in by [step 2.1], one has ; by additivity of the chain integral this gives , hence does not depend on the admissible cycle.
On the trace of the cycle of [step 1.3] the two integrands coincide, , so the two integrals agree; by [step 3.1] applied to each function separately, .
Both assertions of the statement are proved: cycle independence by [step 3.1] and germ independence by [step 4.1].
Depends on
- Holomorphic functional calculus
- Banach-valued Cauchy integral vanishes
- The Axiom of Choice
- Null-homologous cycles and homologous cycles in an open set
- Complex chains, their traces, and cycles
- Admissible cycle around a compact plane set
- Resolvent is Banach-valued holomorphic
- Spectrum and resolvent set in a Banach algebra
- Banach algebra valued contour integral
Used by
Dependency tree · two levels
42 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
- Theo Bühler and Dietmar A. Salamon, Functional Analysis — Theorem 5.25(i), printed pp. 228–229 (standard reference, not scraped)
- Vahid Shirbisheh, Lectures on C-star Algebras, v2 — the contour-independence discussion after Definition 2.5.1, printed p. 47 (standard reference, not scraped)