ExampleConstruction: AI-generatedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-26

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.

Cauchy estimates on a bidisc, computed and compared with the exact derivatives

Example

Let $f (z) = \exp (z_{0} + z_{1})$ on $C^{2}$ , let $a = 0$ , and let the polyradius be $(r, r)$ with $r > 0$ . Then the distinguished-boundary supremum is

$\sup_{Γ_{(r, r)} (0)} ∣ f ∣ = \exp (2 r),$

so the Cauchy estimate gives

$∣ \partial^{α} f (0) ∣ \leq α! \exp (2 r) r^{- ∣ α ∣} .$

For $α = (1, 1)$ the exact value is $∣ \partial^{α} f (0) ∣ = 1$ , whereas the bound is $\exp (2 r) / r^{2}$ , minimized at $r = 1$ with value $e^{2}$ .

Facts & Assumptions

Given: The function $f (z) = \exp (z_{0} + z_{1})$ , the centre $0 \in C^{2}$ , a real $r > 0$ , and the multi-index $α = (1, 1)$ .

[L1]

Cauchy estimates on a polydisc give $∣ \partial^{α} f (a) ∣ \leq α! M r^{- α}$ , where $M$ is the distinguished-boundary supremum and $r^{- α}$ is the product of the inverse powers of the radii (Cauchy estimates for mixed derivatives on a polydisc).

[L2]

The power-series expansion of $\exp (z_{0} + z_{1})$ is $\sum_{α} z^{α} / α!$ on every bidisc, and that series therefore defines a holomorphic function there (The power series of $\exp (z_{0} + z_{1})$ on every bidisc, An absolutely convergent multi-indexed power series is holomorphic and differentiates termwise).

[L3]

$∣ \exp (w) ∣ = \exp (Re w)$ for complex $w$ ( $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ ).

[L4]

For a convergent multivariable power series, the coefficient of $z^{α}$ is $\partial^{α} f (0) / α!$ (The coefficients of a convergent multi-indexed power series are its derivative coefficients, hence unique).

Verification

technique · direct

1.1

If $∣ ζ_{0} ∣ = ∣ ζ_{1} ∣ = r$ , then $∣ f (ζ) ∣ = ∣ \exp (ζ_{0} + ζ_{1}) ∣ = \exp (Re ζ_{0} + Re ζ_{1}) \leq \exp (∣ ζ_{0} ∣ + ∣ ζ_{1} ∣) = \exp (2 r)$ , with equality at $ζ_{0} = ζ_{1} = r$ . So $\sup_{Γ_{(r, r)} (0)} ∣ f ∣ = \exp (2 r)$ .

givenL3

2.1

Since [L2] makes $f$ holomorphic on every bidisc about $0$ , applying [L1] with the supremum of step 1.1 gives $∣ \partial^{α} f (0) ∣ \leq α! \exp (2 r) r^{- ∣ α ∣}$ for every multi-index $α$ .

step 1.1L1L2

3.1

By [L2], the coefficient of $z_{0} z_{1}$ is $1$ , so [L4] gives $\partial^{(1, 1)} f (0) = 1$ . Thus the estimate for $α = (1, 1)$ is $1 \leq \exp (2 r) / r^{2}$ .

step 2.1L2L4

4.1

The function $h (r) = \exp (2 r) / r^{2}$ satisfies $(\log h)^{'} = 2 - 2 / r$ , so its unique critical point on $(0, \infty)$ is $r = 1$ , where it takes the value $e^{2}$ ; hence this example's best bound is $1 \leq e^{2}$ .

step 3.1algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

57 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, v4.4, §1.2 (standard reference, not scraped)