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.
A locally bounded punctured slice has a holomorphic parameter extension
Statement
Let , let , let , and let be holomorphic. Assume that for some the restriction of to is bounded. Define
Then is holomorphic on , and for every fixed the one-variable slice extends holomorphically to with value at .
Facts & Assumptions
Given: A holomorphic function on , bounded on for some .
A punctured-disc holomorphic function extends across the centre exactly when it is bounded near that centre (Characterizations of removable singularities).
A contour integral of a jointly continuous integrand that is holomorphic in the parameter variable defines a holomorphic function of that parameter (A contour integral of a jointly continuous, parameter-holomorphic integrand is holomorphic).
The one-variable Cauchy integral formula recovers a holomorphic function on a disc from a circle inside it (Cauchy's integral formula on a circle compactly contained in a disc of holomorphy).
A separately holomorphic function that is locally bounded is jointly holomorphic (Locally bounded and separately holomorphic implies holomorphic).
Proof
Fix . The slice is holomorphic on the punctured disc and bounded on . Therefore [L1] gives a holomorphic extension to the full disc .
Fix one coordinate of and hold the others fixed. For the integrand is jointly continuous in that parameter and , and for fixed it is holomorphic in the chosen coordinate. So [L2] makes separately holomorphic on . The same circle formula gives local bounds on compact subsets of , so is locally bounded there.
Applying [L3] to the holomorphic function on the circle gives So is exactly the removable value of the slice at .
Step 2.1 identifies with the extension value at for every . Step 1.2 makes separately holomorphic and locally bounded, so [L4] upgrades it to a holomorphic function on .
Depends on
Used by
Dependency tree · two levels
40 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
- J. Lebl, Tasty Bits of Several Complex Variables, Theorem 1.6.1 (standard reference, not scraped)