Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-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 is contour independent

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let A be a unital complex Banach algebra, aA, and let f be holomorphic on an open set U containing σA(a). Then the value f(a) of Holomorphic functional calculus is independent of the admissible cycle used to compute it. Moreover, if VU is another open set containing σA(a) and g is holomorphic on V with g=f on a neighbourhood of σA(a), then f(a)=g(a) with g computed from V.

Facts & Assumptions

Given: An assumed Axiom of Choice, a unital complex Banach algebra A, an element aA with nonempty compact spectrum σA(a), an open UσA(a), a holomorphic f:UC, and two admissible cycles Γ1,Γ2 in UσA(a).

[L1]

The definition chooses an admissible cycle Γ0 and sets f(a)=12πiΓ0f(z)R(z,a)dz; for every admissible cycle the displayed integral is defined because the integrand is continuous on its trace (Holomorphic functional calculus).

[L2]

A cycle Γ is null-homologous in an open set Ω exactly when n(Γ,p)=0 for every pΩ; equivalently n(Γ,p) vanishes at every point outside Ω (Null-homologous cycles and homologous cycles in an open set).

[L3]

If F is continuous and weakly holomorphic on an open Ω and Γ is a cycle with trace in Ω that is null-homologous in Ω, then ΓFdz=0 (Banach-valued Cauchy integral vanishes).

[L4]

For fixed a the map zR(z,a) is holomorphic on ρA(a) and the product of a scalar holomorphic function with it is weakly holomorphic: for every bounded linear functional φ on A the map zφ(f(z)R(z,a)) is holomorphic on UρA(a) (Resolvent is Banach-valued holomorphic, Spectrum and resolvent set in a Banach algebra).

[L6]

For every compact K contained in an open set U there is a finite polygonal cycle with index 1 on K and index 0 outside U (Admissible cycle around a compact plane set).

Proof

technique · direct
1.1

Put Ω:=UσA(a), an open set containing both traces Γ1,Γ2; the difference Γ1Γ2 is a cycle with trace in Ω whose index at p is n(Γ1,p)n(Γ2,p).

L2L4algebra
1.2

The map F(z):=f(z)R(z,a) is continuous on Ω and weakly holomorphic there: for a bounded linear functional φ the composition φ(F(z))=f(z)φ(R(z,a)) is a product of the holomorphic scalar function f and the holomorphic scalar function φ(R(,a)), hence holomorphic on the open subset Ω of ρA(a).

L4algebra
1.3

Germ independence: let VσA(a) be open and let g be holomorphic on V with f=g on a neighbourhood W of σA(a). Apply [L6] to the compact set σA(a) and the open set UVW: this gives an admissible cycle for both (f,U) and (g,V) with trace in (UVW)σA(a), hence lying in W, where f=g.

L6algebra
2.1

For pσA(a) both indices equal 1, and for pU both equal 0, by admissibility; hence n(Γ1Γ2,p)=0 for every pUσA(a), that is, Γ1Γ2 is null-homologous in Ω:=UσA(a).

step 1.1L2algebra
3.1

By [L3] applied to F and the cycle Γ1Γ2, null-homologous in Ω by [step 2.1], one has Γ1Γ2Fdz=0; by additivity of the chain integral this gives Γ1f(z)R(z,a)dz=Γ2f(z)R(z,a)dz, hence f(a) does not depend on the admissible cycle.

step 1.2step 2.1L1
4.1

On the trace of the cycle of [step 1.3] the two integrands coincide, f(z)R(z,a)=g(z)R(z,a), so the two integrals agree; by [step 3.1] applied to each function separately, f(a)=g(a).

step 1.3step 3.1L1
5.1

Both assertions of the statement are proved: cycle independence by [step 3.1] and germ independence by [step 4.1].

step 3.1step 4.1

Depends on

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