Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 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 for mixed derivatives on a polydisc

Statement

Let m1, let aCm, let ρ be a polyradius and let f:Δρ(a)C be holomorphic. Let r be a polyradius with rk<ρk for every k<m, and put M=supΓr(a)f, the supremum over the distinguished boundary only. Then for every multi-index α

zαf(a)  α!Mk<mrkαk.

The bound uses no value of f outside Γr(a), which for m2 is a proper subset of the topological boundary of the closed polydisc.

Facts & Assumptions

Given: A holomorphic f on Δρ(a) and a polyradius r with rk<ρk; Cm is read through Complex m-space and its real coordinate dictionary.

[L1]

For f continuous and separately holomorphic on Δρ(a) and rk<ρk, the iterated-integral coefficients satisfy cαMk<mrkαk with M=supΓr(a)f, and f=αcα(za)α on Δr(a) (A continuous separately holomorphic function is the sum of an absolutely convergent power series with Cauchy-integral coefficients on every smaller polydisc).

[L2]

Every iterated complex partial derivative of a holomorphic function exists and is holomorphic (Holomorphic functions of several variables are smooth and their complex derivatives are holomorphic). For coefficient families satisfying the geometric polyradius bound, the power-series representation about a fixed centre is unique and its coefficients are cα=zαf(a)/α! (The coefficients of a convergent multi-indexed power series are its derivative coefficients, hence unique).

[L3]

A holomorphic function of several variables is continuous and separately holomorphic (A holomorphic function of several variables is continuous and separately holomorphic).

[L4]

If gK on the trace of a rectifiable contour γ, then γgdzKL(γ) (ML estimate: a contour integral is bounded by a supremum bound times path length), and the once-traversed circle of radius r>0 has length 2πr (Every circle has circumference 2 pi r and circumference-to-diameter ratio pi).

[L5]

For f holomorphic on D(a,R), 0<r<R and fK on the circle ζa=r, one has f(n)(a)n!K/rn (Cauchy's inequalities bound every derivative by a boundary bound on a compactly contained circle).

[L6]

Γr(a) is the set of points with zkak=rk for every k<m, and for m2 it is a proper subset of the topological boundary of Δr(a) (Balls, polydiscs and the distinguished boundary in Cm).

Proof

technique · direct
1.1

By [L3] the function f is continuous and separately holomorphic on Δρ(a), so [L1] applies with the given r and produces coefficients cα with cαMk<mrkαk, the constant M being the supremum of f on Γr(a) alone. That bound is what the m-fold application of the ML estimate of [L4] on the m circles of radius rk produces, one factor 2πrk cancelling each factor (2π)1, and it specialises at m=1 to the published one-variable inequality of [L5].

givenL1L3L4L5L6
2.1

By [L2] those same coefficients are cα=zαf(a)/α!, so multiplying the bound of step 1.1 by α! gives zαf(a)α!Mk<mrkαk, as claimed; α!0 by [L7] makes the division legitimate.

step 1.1L2L7
3.1

No value of f off Γr(a) entered: the constant M of step 1.1 is a supremum over that set, and by [L6] it is for m2 a proper subset of the topological boundary of the closed polydisc.

step 1.1step 2.1L6

Depends on

Used by

Dependency tree · two levels

82 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