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 in the Wiener algebra
Statement
Assume the Axiom of Choice. Let and let be holomorphic on an open neighbourhood of . Then .
Facts & Assumptions
Given: The Axiom of Choice, , and holomorphic near the compact set .
A nowhere-zero member of has its reciprocal in (Wiener's lemma for absolutely convergent Fourier series).
is complete and closed under multiplication (The Wiener algebra is a unital commutative Banach algebra).
Cauchy's formula holds for null-homologous complex cycles (Cauchy's integral formula for a null-homologous cycle ↗).
Proof
Let be an open set on which is holomorphic and which contains . The compact-neighbourhood lemma A compact subset of an open Euclidean set has a compact Jordan neighborhood inside that open set gives a finite union of closed grid rectangles with . Orient the frontier edges of the constituent grid cells positively and cancel each internal edge against its reverse. The resulting polygonal chain is a cycle in , with for and for : summing the cell indices first proves this away from the grid lines, and local constancy of the cycle index extends it to every point off the frontier. Thus is null-homologous in . For , has no zero on , so by [L1].
The map is continuous into (the inverse identity follows from ). Hence its normalized chain integral is an element, as the finite sum of norm-limits of edgewise Riemann sums by [L2].
Evaluation at commutes with those norm-limits. Since step 1.1 gives and makes null-homologous in , [L3] applied to gives . Thus and belongs to .
Depends on
- The Wiener algebra is a unital commutative Banach algebra
- Wiener's lemma for absolutely convergent Fourier series
- A compact subset of an open Euclidean set has a compact Jordan neighborhood inside that open set
- Complex chains, their traces, and cycles
- Integration over a complex chain and the index of a chain
- Null-homologous cycles and homologous cycles in an open set
- The index of a cycle is locally constant off its trace and vanishes far from it
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
50 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
- Richard S. Laugesen, Harmonic Analysis Lecture Notes, Theorem 4.3 (standard reference, not scraped)